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

Author: YaelDillies

archive/imo/imo2008_q3.lean

@@ -77,17 +77,15 @@ begin
 
   have hreal₅ : k₀ > 4,
   { calc k₀ ≥ sqrt(p₀ - 4) : hreal₄
-    ...     > sqrt(4 ^ 2)  : (sqrt_lt (by linarith)).mpr (by linarith [hreal₂])
-    ...     = 4            : sqrt_sq (by linarith) },
+    ...     > sqrt(4 ^ 2)  : sqrt_lt_sqrt (by norm_num) (by linarith [hreal₂])
+    ...     = 4            : sqrt_sq zero_lt_four.le },
 
   have hreal₆ : p₀ > 2 * n₀ + sqrt(2 * n),
   { calc p₀ = 2 * n₀ + k₀                    : hreal₁
-    ...     ≥ 2 * n₀ + sqrt(p₀ - 4)          : by linarith [hreal₄]
+    ...     ≥ 2 * n₀ + sqrt(p₀ - 4)          : add_le_add_left hreal₄ _
     ...     = 2 * n₀ + sqrt(2 * n₀ + k₀ - 4) : by rw hreal₁
-    ...     > 2 * n₀ + sqrt(2 * n₀)     : by { refine add_lt_add_left _ (2 * n₀),
-                                               refine (sqrt_lt _).mpr _,
-                                               refine mul_nonneg zero_le_two (nat.cast_nonneg n),
-                                               linarith [hreal₅] } },
+    ...     > 2 * n₀ + sqrt(2 * n₀) : add_lt_add_left
+        (sqrt_lt_sqrt (mul_nonneg zero_le_two n.cast_nonneg) $ by linarith [hreal₅]) (2 * n₀) },
 
   exact ⟨n, hnat₁, hreal₆⟩,
 end

src/analysis/special_functions/arsinh.lean

@@ -42,8 +42,8 @@ end
 
 private lemma b_lt_sqrt_b_one_add_sq (b : ℝ) : b < sqrt (1 + b ^ 2) :=
 calc  b
-    ≤ sqrt (b ^ 2)     : le_sqrt_of_sq_le $ le_refl _
-... < sqrt (1 + b ^ 2) : (sqrt_lt (sq_nonneg _)).2 (lt_one_add _)
+    ≤ sqrt (b ^ 2)     : le_sqrt_of_sq_le le_rfl
+... < sqrt (1 + b ^ 2) : sqrt_lt_sqrt (sq_nonneg _) (lt_one_add _)
 
 private lemma add_sqrt_one_add_sq_pos (b : ℝ) : 0 < b + sqrt (1 + b ^ 2) :=
 by { rw [← neg_neg b, ← sub_eq_neg_add, sub_pos, sq, neg_mul_neg, ← sq],

src/analysis/special_functions/pow.lean

@@ -923,14 +923,14 @@ times_cont_diff_at.has_strict_deriv_at'
 
 section sqrt
 
-lemma sqrt_eq_rpow : sqrt = λx:ℝ, x ^ (1/(2:ℝ)) :=
+lemma sqrt_eq_rpow (x : ℝ) : sqrt x = x ^ (1/(2:ℝ)) :=
 begin
-  funext, by_cases h : 0 ≤ x,
-  { rw [← mul_self_inj_of_nonneg, mul_self_sqrt h, ← sq, ← rpow_nat_cast, ← rpow_mul h],
-    norm_num, exact sqrt_nonneg _, exact rpow_nonneg_of_nonneg h _ },
-  { replace h : x < 0 := lt_of_not_ge h,
-    have : 1 / (2:ℝ) * π = π / (2:ℝ), ring,
-    rw [sqrt_eq_zero_of_nonpos (le_of_lt h), rpow_def_of_neg h, this, cos_pi_div_two, mul_zero] }
+  obtain h | h := le_or_lt 0 x,
+  { rw [← mul_self_inj_of_nonneg (sqrt_nonneg _) (rpow_nonneg_of_nonneg h _), mul_self_sqrt h,
+      ← sq, ← rpow_nat_cast, ← rpow_mul h],
+    norm_num },
+  { have : 1 / (2:ℝ) * π = π / (2:ℝ), ring,
+    rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero] }
 end
 
 end sqrt
@@ -1251,6 +1251,13 @@ nnreal.eq $ real.inv_rpow x.2 y
 lemma div_rpow (x y : ℝ≥0) (z : ℝ) : (x / y) ^ z = x ^ z / y ^ z :=
 nnreal.eq $ real.div_rpow x.2 y.2 z
 
+lemma sqrt_eq_rpow (x : ℝ≥0) : sqrt x = x ^ (1/(2:ℝ)) :=
+begin
+  refine nnreal.eq _,
+  push_cast,
+  exact real.sqrt_eq_rpow x.1,
+end
+
 @[simp, norm_cast] lemma rpow_nat_cast (x : ℝ≥0) (n : ℕ) : x ^ (n : ℝ) = x ^ n :=
 nnreal.eq $ by simpa only [coe_rpow, coe_pow] using real.rpow_nat_cast x n
 

src/analysis/special_functions/trigonometric.lean

@@ -1393,8 +1393,8 @@ lemma sqrt_two_add_series_lt_two : ∀(n : ℕ), sqrt_two_add_series 0 n < 2
 | 0     := by norm_num
 | (n+1) :=
   begin
-    refine lt_of_lt_of_le _ (le_of_eq $ sqrt_sq $ le_of_lt zero_lt_two),
-    rw [sqrt_two_add_series, sqrt_lt, ← lt_sub_iff_add_lt'],
+    refine lt_of_lt_of_le _ (sqrt_sq zero_lt_two.le).le,
+    rw [sqrt_two_add_series, sqrt_lt_sqrt_iff, ← lt_sub_iff_add_lt'],
     { refine (sqrt_two_add_series_lt_two n).trans_le _, norm_num },
     { exact add_nonneg zero_le_two (sqrt_two_add_series_zero_nonneg n) }
   end

src/data/real/sqrt.lean

@@ -45,6 +45,12 @@ order_iso.symm $ strict_mono.order_iso_of_surjective (λ x, x * x)
   (continuous_id.mul continuous_id).surjective tendsto_mul_self_at_top $
     by simp [order_bot.at_bot_eq]
 
+lemma sqrt_le_sqrt_iff : sqrt x ≤ sqrt y ↔ x ≤ y :=
+sqrt.le_iff_le
+
+lemma sqrt_lt_sqrt_iff : sqrt x < sqrt y ↔ x < y :=
+sqrt.lt_iff_lt
+
 lemma sqrt_eq_iff_sq_eq : sqrt x = y ↔ y * y = x :=
 sqrt.to_equiv.apply_eq_iff_eq_symm_apply.trans eq_comm
 
@@ -61,13 +67,19 @@ sqrt_eq_iff_sq_eq.trans $ by rw [eq_comm, zero_mul]
 
 @[simp] lemma sqrt_one : sqrt 1 = 1 := sqrt_eq_iff_sq_eq.2 $ mul_one 1
 
-@[simp] lemma mul_sqrt_self (x : ℝ≥0) : sqrt x * sqrt x = x :=
+@[simp] lemma mul_self_sqrt (x : ℝ≥0) : sqrt x * sqrt x = x :=
 sqrt.symm_apply_apply x
 
 @[simp] lemma sqrt_mul_self (x : ℝ≥0) : sqrt (x * x) = x := sqrt.apply_symm_apply x
 
+@[simp] lemma sq_sqrt (x : ℝ≥0) : (sqrt x)^2 = x :=
+by rw [sq, mul_self_sqrt x]
+
+@[simp] lemma sqrt_sq (x : ℝ≥0) : sqrt (x^2) = x :=
+by rw [sq, sqrt_mul_self x]
+
 lemma sqrt_mul (x y : ℝ≥0) : sqrt (x * y) = sqrt x * sqrt y :=
-by rw [sqrt_eq_iff_sq_eq, mul_mul_mul_comm, mul_sqrt_self, mul_sqrt_self]
+by rw [sqrt_eq_iff_sq_eq, mul_mul_mul_comm, mul_self_sqrt, mul_self_sqrt]
 
 /-- `nnreal.sqrt` as a `monoid_with_zero_hom`. -/
 noncomputable def sqrt_hom : monoid_with_zero_hom ℝ≥0 ℝ≥0 := ⟨sqrt, sqrt_zero, sqrt_one, sqrt_mul⟩
@@ -122,6 +134,9 @@ nnreal.sqrt (real.to_nnreal x)
 
 variables {x y : ℝ}
 
+@[simp, norm_cast] lemma coe_sqrt {x : ℝ≥0} : (nnreal.sqrt x : ℝ) = real.sqrt x :=
+by rw [real.sqrt, real.to_nnreal_coe]
+
 @[continuity]
 lemma continuous_sqrt : continuous sqrt :=
 nnreal.continuous_coe.comp $ nnreal.sqrt.continuous.comp nnreal.continuous_of_real
@@ -132,7 +147,7 @@ by simp [sqrt, real.to_nnreal_eq_zero.2 h]
 theorem sqrt_nonneg (x : ℝ) : 0 ≤ sqrt x := nnreal.coe_nonneg _
 
 @[simp] theorem mul_self_sqrt (h : 0 ≤ x) : sqrt x * sqrt x = x :=
-by simp [sqrt, ← nnreal.coe_mul, real.coe_to_nnreal _ h]
+by rw [sqrt, ← nnreal.coe_mul, nnreal.mul_self_sqrt, real.coe_to_nnreal _ h]
 
 @[simp] theorem sqrt_mul_self (h : 0 ≤ x) : sqrt (x * x) = x :=
 (mul_self_inj_of_nonneg (sqrt_nonneg _) h).1 (mul_self_sqrt (mul_self_nonneg _))
@@ -141,7 +156,7 @@ theorem sqrt_eq_iff_mul_self_eq (hx : 0 ≤ x) (hy : 0 ≤ y) :
   sqrt x = y ↔ y * y = x :=
 ⟨λ h, by rw [← h, mul_self_sqrt hx], λ h, by rw [← h, sqrt_mul_self hy]⟩
 
-@[simp] theorem sq_sqrt (h : 0 ≤ x) : sqrt x ^ 2 = x :=
+@[simp] theorem sq_sqrt (h : 0 ≤ x) : (sqrt x)^2 = x :=
 by rw [sq, mul_self_sqrt h]
 
 @[simp] theorem sqrt_sq (h : 0 ≤ x) : sqrt (x ^ 2) = x :=
@@ -161,14 +176,20 @@ by rw [sq, sqrt_mul_self_eq_abs]
 
 @[simp] theorem sqrt_one : sqrt 1 = 1 := by simp [sqrt]
 
-@[simp] theorem sqrt_le (hy : 0 ≤ y) : sqrt x ≤ sqrt y ↔ x ≤ y :=
-by simp [sqrt, real.to_nnreal_le_to_nnreal_iff, *]
+@[simp] theorem sqrt_le_sqrt_iff (hy : 0 ≤ y) : sqrt x ≤ sqrt y ↔ x ≤ y :=
+by rw [sqrt, sqrt, nnreal.coe_le_coe, nnreal.sqrt_le_sqrt_iff, real.to_nnreal_le_to_nnreal_iff hy]
+
+@[simp] theorem sqrt_lt_sqrt_iff (hx : 0 ≤ x) : sqrt x < sqrt y ↔ x < y :=
+lt_iff_lt_of_le_iff_le (sqrt_le_sqrt_iff hx)
 
-@[simp] theorem sqrt_lt (hx : 0 ≤ x) : sqrt x < sqrt y ↔ x < y :=
-lt_iff_lt_of_le_iff_le (sqrt_le hx)
+theorem sqrt_lt_sqrt_iff_of_pos (hy : 0 < y) : sqrt x < sqrt y ↔ x < y :=
+by rw [sqrt, sqrt, nnreal.coe_lt_coe, nnreal.sqrt_lt_sqrt_iff, to_nnreal_lt_to_nnreal_iff hy]
 
 theorem sqrt_le_sqrt (h : x ≤ y) : sqrt x ≤ sqrt y :=
-by simp [sqrt, real.to_nnreal_le_to_nnreal h]
+by { rw [sqrt, sqrt, nnreal.coe_le_coe, nnreal.sqrt_le_sqrt_iff], exact to_nnreal_le_to_nnreal h }
+
+theorem sqrt_lt_sqrt (hx : 0 ≤ x) (h : x < y) : sqrt x < sqrt y :=
+(sqrt_lt_sqrt_iff hx).2 h
 
 theorem sqrt_le_left (hy : 0 ≤ y) : sqrt x ≤ y ↔ x ≤ y ^ 2 :=
 by rw [sqrt, ← real.le_to_nnreal_iff_coe_le hy, nnreal.sqrt_le_iff, ← real.to_nnreal_mul hy,
@@ -250,7 +271,7 @@ by rw [mul_self_lt_mul_self_iff hx (sqrt_nonneg y), sq, mul_self_sqrt hy]
 theorem sq_lt : x^2 < y ↔ -sqrt y < x ∧ x < sqrt y :=
 begin
   split,
-  { simpa only [← sqrt_lt (sq_nonneg x), sqrt_sq_eq_abs] using abs_lt.mp },
+  { simpa only [← sqrt_lt_sqrt_iff (sq_nonneg x), sqrt_sq_eq_abs] using abs_lt.mp },
   { rw [← abs_lt, ← sq_abs],
     exact λ h, (lt_sqrt (abs_nonneg x) (sqrt_pos.mp (lt_of_le_of_lt (abs_nonneg x) h)).le).mp h },
 end