mathlib3

461865b2 - refactor(data/real): move `real.sqrt` to `data.real.sqrt`, more dependencies (#5359)

refactor(data/real): move `real.sqrt` to `data.real.sqrt`, more dependencies (#5359) * define `nnreal.sqrt`; * use general theory to prove that the inverse exists, and is an `order_iso`; * deduce continuity of `sqrt` from continuity of `order_iso`. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>