mathlib

796efae2 - feat(data/real/sqrt): `nnreal.coe_sqrt` and `nnreal.sqrt_eq_rpow` (#9025)

feat(data/real/sqrt): `nnreal.coe_sqrt` and `nnreal.sqrt_eq_rpow` (#9025) Also rename a few lemmas: * `nnreal.mul_sqrt_self` -> `nnreal.mul_self_sqrt` to follow `real.mul_self_sqrt` * `real.sqrt_le` -> `real.sqrt_le_sqrt_iff` * `real.sqrt_lt` -> `real.sqrt_lt_sqrt_iff` and provide a few more for commodity: * `nnreal.sqrt_sq` * `nnreal.sq_sqrt` * `real.sqrt_lt_sqrt` * `real.sqrt_lt_sqrt_iff_of_pos` * `nnreal.sqrt_le_sqrt_iff` * `nnreal.sqrt_lt_sqrt_iff` Closes #8016