feat(data/real/sqrt): added some missing sqrt lemmas (#5933)

I noticed that some facts about `sqrt` and `abs` are missing, so I am adding them.

src/algebra/group_power/basic.lean

@@ -622,14 +622,27 @@ theorem pow_bit0_pos {a : R} (h : a ≠ 0) (n : ℕ) : 0 < a ^ bit0 n :=
 theorem pow_two_pos_of_ne_zero (a : R) (h : a ≠ 0) : 0 < a ^ 2 :=
 pow_bit0_pos h 1
 
-end linear_ordered_ring
+variables {x y : R}
 
-@[simp] lemma abs_sq_eq [linear_ordered_ring R] (a : R) : (abs a) ^ 2 = a ^ 2 :=
-begin
-  by_cases h : 0 ≤ a,
-  { simp [abs_of_nonneg h] },
-  { simp [abs_of_neg (not_le.mp h)] }
-end
+@[simp] theorem sqr_abs : abs x ^ 2 = x ^ 2 :=
+by simpa only [pow_two] using abs_mul_abs_self x
+
+theorem abs_sqr : abs (x ^ 2) = x ^ 2 :=
+by simpa only [pow_two] using abs_mul_self x
+
+theorem sqr_lt_sqr (h : abs x < y) : x ^ 2 < y ^ 2 :=
+by simpa only [sqr_abs] using pow_lt_pow_of_lt_left h (abs_nonneg x) (1:ℕ).succ_pos
+
+theorem sqr_lt_sqr' (h1 : -y < x) (h2 : x < y) : x ^ 2 < y ^ 2 :=
+sqr_lt_sqr (abs_lt.mpr ⟨h1, h2⟩)
+
+theorem sqr_le_sqr (h : abs x ≤ y) : x ^ 2 ≤ y ^ 2 :=
+by simpa only [sqr_abs] using pow_le_pow_of_le_left (abs_nonneg x) h 2
+
+theorem sqr_le_sqr' (h1 : -y ≤ x) (h2 : x ≤ y) : x ^ 2 ≤ y ^ 2 :=
+sqr_le_sqr (abs_le.mpr ⟨h1, h2⟩)
+
+end linear_ordered_ring
 
 @[simp] lemma eq_of_pow_two_eq_pow_two [linear_ordered_comm_ring R]
   {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) :

src/algebra/ordered_group.lean

@@ -642,11 +642,17 @@ lemma abs_pos_of_neg (h : a < 0) : 0 < abs a := abs_pos.2 h.ne
 lemma abs_sub (a b : α) : abs (a - b) = abs (b - a) :=
 by rw [← neg_sub, abs_neg]
 
-theorem abs_le' : abs a ≤ b ↔ a ≤ b ∧ -a ≤ b := max_le_iff
+lemma abs_le' : abs a ≤ b ↔ a ≤ b ∧ -a ≤ b := max_le_iff
 
-theorem abs_le : abs a ≤ b ↔ - b ≤ a ∧ a ≤ b :=
+lemma abs_le : abs a ≤ b ↔ - b ≤ a ∧ a ≤ b :=
 by rw [abs_le', and.comm, neg_le]
 
+lemma neg_le_of_abs_le (h : abs a ≤ b) : -b ≤ a := (abs_le.mp h).1
+
+lemma le_of_abs_le (h : abs a ≤ b) : a ≤ b := (abs_le.mp h).2
+
+lemma le_abs : a ≤ abs b ↔ a ≤ b ∨ a ≤ -b := le_max_iff
+
 lemma le_abs_self (a : α) : a ≤ abs a := le_max_left _ _
 
 lemma neg_le_abs_self (a : α) : -a ≤ abs a := le_max_right _ _
@@ -663,10 +669,14 @@ not_iff_not.1 $ ne_comm.trans $ (abs_nonneg a).lt_iff_ne.symm.trans abs_pos
 @[simp] lemma abs_nonpos_iff {a : α} : abs a ≤ 0 ↔ a = 0 :=
 (abs_nonneg a).le_iff_eq.trans abs_eq_zero
 
-lemma abs_lt {a b : α} : abs a < b ↔ - b < a ∧ a < b :=
+lemma abs_lt : abs a < b ↔ - b < a ∧ a < b :=
 max_lt_iff.trans $ and.comm.trans $ by rw [neg_lt]
 
-lemma lt_abs {a b : α} : a < abs b ↔ a < b ∨ a < -b := lt_max_iff
+lemma neg_lt_of_abs_lt (h : abs a < b) : -b < a := (abs_lt.mp h).1
+
+lemma lt_of_abs_lt (h : abs a < b) : a < b := (abs_lt.mp h).2
+
+lemma lt_abs : a < abs b ↔ a < b ∨ a < -b := lt_max_iff
 
 lemma max_sub_min_eq_abs' (a b : α) : max a b - min a b = abs (a - b) :=
 begin

src/data/real/sqrt.lean

@@ -167,35 +167,45 @@ by simp [sqrt, nnreal.of_real_le_of_real_iff, *]
 @[simp] theorem sqrt_lt (hx : 0 ≤ x) : sqrt x < sqrt y ↔ x < y :=
 lt_iff_lt_of_le_iff_le (sqrt_le hx)
 
-lemma sqrt_le_sqrt (h : x ≤ y) : sqrt x ≤ sqrt y :=
+theorem sqrt_le_sqrt (h : x ≤ y) : sqrt x ≤ sqrt y :=
 by simp [sqrt, nnreal.of_real_le_of_real h]
 
-lemma sqrt_le_left (hy : 0 ≤ y) : sqrt x ≤ y ↔ x ≤ y ^ 2 :=
+theorem sqrt_le_left (hy : 0 ≤ y) : sqrt x ≤ y ↔ x ≤ y ^ 2 :=
 by rw [sqrt, ← nnreal.le_of_real_iff_coe_le hy, nnreal.sqrt_le_iff, ← nnreal.of_real_mul hy,
   nnreal.of_real_le_of_real_iff (mul_self_nonneg y), pow_two]
 
-lemma sqrt_le_iff : sqrt x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2 :=
+theorem sqrt_le_iff : sqrt x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2 :=
 begin
   rw [← and_iff_right_of_imp (λ h, (sqrt_nonneg x).trans h), and.congr_right_iff],
   exact sqrt_le_left
 end
 
 /- note: if you want to conclude `x ≤ sqrt y`, then use `le_sqrt_of_sqr_le`.
    if you have `x > 0`, consider using `le_sqrt'` -/
-lemma le_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
+theorem le_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
 by rw [mul_self_le_mul_self_iff hx (sqrt_nonneg _), pow_two, mul_self_sqrt hy]
 
-lemma le_sqrt' (hx : 0 < x) : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
+theorem le_sqrt' (hx : 0 < x) : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
 by { rw [sqrt, ← nnreal.coe_mk x hx.le, nnreal.coe_le_coe, nnreal.le_sqrt_iff,
   nnreal.le_of_real_iff_coe_le', pow_two, nnreal.coe_mul], exact mul_pos hx hx }
 
-lemma le_sqrt_of_sqr_le (h : x ^ 2 ≤ y) : x ≤ sqrt y :=
+theorem abs_le_sqrt (h : x^2 ≤ y) : abs x ≤ sqrt y :=
+by rw ← sqrt_sqr_eq_abs; exact sqrt_le_sqrt h
+
+theorem sqr_le (h : 0 ≤ y) : x^2 ≤ y ↔ -sqrt y ≤ x ∧ x ≤ sqrt y :=
 begin
-  cases lt_or_ge 0 x with hx hx,
-  { rwa [le_sqrt' hx] },
-  { exact le_trans hx (sqrt_nonneg y) }
+  split,
+  { simpa only [abs_le] using abs_le_sqrt },
+  { rw [← abs_le, ← sqr_abs],
+    exact (le_sqrt (abs_nonneg x) h).mp },
 end
 
+theorem neg_sqrt_le_of_sqr_le (h : x^2 ≤ y) : -sqrt y ≤ x :=
+((sqr_le ((pow_two_nonneg x).trans h)).mp h).1
+
+theorem le_sqrt_of_sqr_le (h : x^2 ≤ y) : x ≤ sqrt y :=
+((sqr_le ((pow_two_nonneg x).trans h)).mp h).2
+
 @[simp] theorem sqrt_inj (hx : 0 ≤ x) (hy : 0 ≤ y) : sqrt x = sqrt y ↔ x = y :=
 by simp [le_antisymm_iff, hx, hy]
 
@@ -205,6 +215,12 @@ by simpa using sqrt_inj h (le_refl _)
 theorem sqrt_eq_zero' : sqrt x = 0 ↔ x ≤ 0 :=
 by rw [sqrt, nnreal.coe_eq_zero, nnreal.sqrt_eq_zero, nnreal.of_real_eq_zero]
 
+theorem sqrt_ne_zero (h : 0 ≤ x) : sqrt x ≠ 0 ↔ x ≠ 0 :=
+by rw [not_iff_not, sqrt_eq_zero h]
+
+theorem sqrt_ne_zero' : sqrt x ≠ 0 ↔ 0 < x :=
+by rw [← not_le, not_iff_not, sqrt_eq_zero']
+
 @[simp] theorem sqrt_pos : 0 < sqrt x ↔ 0 < x :=
 lt_iff_lt_of_le_iff_le (iff.trans
   (by simp [le_antisymm_iff, sqrt_nonneg]) sqrt_eq_zero')
@@ -221,6 +237,28 @@ by rw [sqrt, nnreal.of_real_inv, nnreal.sqrt_inv, nnreal.coe_inv, sqrt]
 @[simp] theorem sqrt_div (hx : 0 ≤ x) (y : ℝ) : sqrt (x / y) = sqrt x / sqrt y :=
 by rw [division_def, sqrt_mul hx, sqrt_inv, division_def]
 
+@[simp] theorem div_sqrt : x / sqrt x = sqrt x :=
+begin
+  cases le_or_lt x 0,
+  { rw [sqrt_eq_zero'.mpr h, div_zero] },
+  { rw [div_eq_iff (sqrt_ne_zero'.mpr h), mul_self_sqrt h.le] },
+end
+
+theorem lt_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x < sqrt y ↔ x ^ 2 < y :=
+by rw [mul_self_lt_mul_self_iff hx (sqrt_nonneg y), pow_two, mul_self_sqrt hy]
+
+theorem sqr_lt : x^2 < y ↔ -sqrt y < x ∧ x < sqrt y :=
+begin
+  split,
+  { simpa only [← sqrt_lt (pow_two_nonneg x), sqrt_sqr_eq_abs] using abs_lt.mp },
+  { rw [← abs_lt, ← sqr_abs],
+    exact λ h, (lt_sqrt (abs_nonneg x) (sqrt_pos.mp (lt_of_le_of_lt (abs_nonneg x) h)).le).mp h },
+end
+
+theorem neg_sqrt_lt_of_sqr_lt (h : x^2 < y) : -sqrt y < x := (sqr_lt.mp h).1
+
+theorem lt_sqrt_of_sqr_lt (h : x^2 < y) : x < sqrt y := (sqr_lt.mp h).2
+
 end real
 
 open real

src/geometry/manifold/instances/sphere.lean

@@ -173,7 +173,7 @@ begin
   { have hvy' : ⟪a • v, y⟫_ℝ = 0 := by simp [inner_smul_left, hvy],
     convert norm_add_square_eq_norm_square_add_norm_square_of_inner_eq_zero _ _ hvy' using 2,
     { simp [← split] },
-    { simp [norm_smul, hv, real.norm_eq_abs, ← pow_two, abs_sq_eq] },
+    { simp [norm_smul, hv, real.norm_eq_abs, ← pow_two, sqr_abs] },
     { exact pow_two _ } },
   -- two facts which will be helpful for clearing denominators in the main calculation
   have ha : 1 - a ≠ 0,
@@ -198,7 +198,7 @@ begin
   convert congr_arg2 has_add.add (congr_arg (λ t, t • (y:E)) h₁) (congr_arg (λ t, t • v) h₂)
     using 1,
   { simp [inner_add_right, inner_smul_right, hvy, real_inner_self_eq_norm_square, hv, mul_smul,
-      mul_pow, real.norm_eq_abs, abs_sq_eq, norm_smul] },
+      mul_pow, real.norm_eq_abs, sqr_abs, norm_smul] },
   { simp [split, add_comm] }
 end