refactor(algebra/order/ring): turn sq_le_sq into an iff (#14511)

* `sq_le_sq` and `sq_lt_sq` are now `iff` lemmas;
* drop `abs_le_abs_of_sq_le_sq` and `abs_lt_abs_of_sq_lt_sq`.

src/algebra/group_power/order.lean

@@ -341,57 +341,46 @@ by simpa only [sq] using abs_mul_abs_self x
 theorem abs_sq (x : R) : |x ^ 2| = x ^ 2 :=
 by simpa only [sq] using abs_mul_self x
 
-theorem sq_lt_sq (h : |x| < |y|) : x ^ 2 < y ^ 2 :=
-by simpa only [sq_abs] using pow_lt_pow_of_lt_left h (abs_nonneg x) (1:ℕ).succ_pos
+theorem sq_lt_sq : x ^ 2 < y ^ 2 ↔ |x| < |y| :=
+by simpa only [sq_abs]
+  using (@strict_mono_on_pow R _ _ two_pos).lt_iff_lt (abs_nonneg x) (abs_nonneg y)
 
 theorem sq_lt_sq' (h1 : -y < x) (h2 : x < y) : x ^ 2 < y ^ 2 :=
-sq_lt_sq (lt_of_lt_of_le (abs_lt.2 ⟨h1, h2⟩) (le_abs_self _))
+sq_lt_sq.2 (lt_of_lt_of_le (abs_lt.2 ⟨h1, h2⟩) (le_abs_self _))
 
-theorem sq_le_sq (h : |x| ≤ |y|) : x ^ 2 ≤ y ^ 2 :=
-by simpa only [sq_abs] using pow_le_pow_of_le_left (abs_nonneg x) h 2
+theorem sq_le_sq : x ^ 2 ≤ y ^ 2 ↔ |x| ≤ |y| :=
+by simpa only [sq_abs]
+  using (@strict_mono_on_pow R _ _ two_pos).le_iff_le (abs_nonneg x) (abs_nonneg y)
 
 theorem sq_le_sq' (h1 : -y ≤ x) (h2 : x ≤ y) : x ^ 2 ≤ y ^ 2 :=
-sq_le_sq (le_trans (abs_le.mpr ⟨h1, h2⟩) (le_abs_self _))
-
-theorem abs_lt_abs_of_sq_lt_sq (h : x^2 < y^2) : |x| < |y| :=
-lt_of_pow_lt_pow 2 (abs_nonneg y) $ by rwa [← sq_abs x, ← sq_abs y] at h
+sq_le_sq.2 (le_trans (abs_le.mpr ⟨h1, h2⟩) (le_abs_self _))
 
 theorem abs_lt_of_sq_lt_sq (h : x^2 < y^2) (hy : 0 ≤ y) : |x| < y :=
-begin
-  rw [← abs_of_nonneg hy],
-  exact abs_lt_abs_of_sq_lt_sq h,
-end
+by rwa [← abs_of_nonneg hy, ← sq_lt_sq]
 
 theorem abs_lt_of_sq_lt_sq' (h : x^2 < y^2) (hy : 0 ≤ y) : -y < x ∧ x < y :=
 abs_lt.mp $ abs_lt_of_sq_lt_sq h hy
 
-theorem abs_le_abs_of_sq_le_sq (h : x^2 ≤ y^2) : |x| ≤ |y| :=
-le_of_pow_le_pow 2 (abs_nonneg y) (1:ℕ).succ_pos $ by rwa [← sq_abs x, ← sq_abs y] at h
-
 theorem abs_le_of_sq_le_sq (h : x^2 ≤ y^2) (hy : 0 ≤ y) : |x| ≤ y :=
-begin
-  rw [← abs_of_nonneg hy],
-  exact abs_le_abs_of_sq_le_sq h,
-end
+by rwa [← abs_of_nonneg hy, ← sq_le_sq]
 
 theorem abs_le_of_sq_le_sq' (h : x^2 ≤ y^2) (hy : 0 ≤ y) : -y ≤ x ∧ x ≤ y :=
 abs_le.mp $ abs_le_of_sq_le_sq h hy
 
 lemma sq_eq_sq_iff_abs_eq_abs (x y : R) : x^2 = y^2 ↔ |x| = |y| :=
-⟨λ h, (abs_le_abs_of_sq_le_sq h.le).antisymm (abs_le_abs_of_sq_le_sq h.ge),
- λ h, by rw [←sq_abs, h, sq_abs]⟩
+by simp only [le_antisymm_iff, sq_le_sq]
 
 @[simp] lemma sq_le_one_iff_abs_le_one (x : R) : x^2 ≤ 1 ↔ |x| ≤ 1 :=
-have t : x^2 ≤ 1^2 ↔ |x| ≤ |1| := ⟨abs_le_abs_of_sq_le_sq, sq_le_sq⟩, by simpa using t
+by simpa only [one_pow, abs_one] using @sq_le_sq _ _ x 1
 
 @[simp] lemma sq_lt_one_iff_abs_lt_one (x : R) : x^2 < 1 ↔ |x| < 1 :=
-have t : x^2 < 1^2 ↔ |x| < |1| := ⟨abs_lt_abs_of_sq_lt_sq, sq_lt_sq⟩, by simpa using t
+by simpa only [one_pow, abs_one] using @sq_lt_sq _ _ x 1
 
 @[simp] lemma one_le_sq_iff_one_le_abs (x : R) : 1 ≤ x^2 ↔ 1 ≤ |x| :=
-have t : 1^2 ≤ x^2 ↔ |1| ≤ |x| := ⟨abs_le_abs_of_sq_le_sq, sq_le_sq⟩, by simpa using t
+by simpa only [one_pow, abs_one] using @sq_le_sq _ _ 1 x
 
 @[simp] lemma one_lt_sq_iff_one_lt_abs (x : R) : 1 < x^2 ↔ 1 < |x| :=
-have t : 1^2 < x^2 ↔ |1| < |x| := ⟨abs_lt_abs_of_sq_lt_sq, sq_lt_sq⟩, by simpa using t
+by simpa only [one_pow, abs_one] using @sq_lt_sq _ _ 1 x
 
 lemma pow_four_le_pow_two_of_pow_two_le {x y : R} (h : x^2 ≤ y) : x^4 ≤ y^2 :=
 (pow_mul x 2 2).symm ▸ pow_le_pow_of_le_left (sq_nonneg x) h 2

src/analysis/inner_product_space/basic.lean

@@ -1935,9 +1935,8 @@ begin
     have : ∀ i, 0 ≤ ∥f i∥ ^ 2 := λ i : ι, sq_nonneg _,
     simp only [finset.abs_sum_of_nonneg' this],
     have : ∑ i in s₁ \ s₂, ∥f i∥ ^ 2 + ∑ i in s₂ \ s₁, ∥f i∥ ^ 2 < (sqrt ε) ^ 2,
-    { rw ← hV.norm_sq_diff_sum,
-      apply sq_lt_sq,
-      rw [_root_.abs_of_nonneg (sqrt_nonneg _), _root_.abs_of_nonneg (norm_nonneg _)],
+    { rw [← hV.norm_sq_diff_sum, sq_lt_sq,
+        _root_.abs_of_nonneg (sqrt_nonneg _), _root_.abs_of_nonneg (norm_nonneg _)],
       exact H s₁ hs₁ s₂ hs₂ },
     have hη := sq_sqrt (le_of_lt hε),
     linarith },

src/analysis/special_functions/bernstein.lean

@@ -162,6 +162,8 @@ The modulus of (uniform) continuity for `f`, chosen so `|f x - f y| < ε/2` when
 -/
 def δ (f : C(I, ℝ)) (ε : ℝ) (h : 0 < ε) : ℝ := f.modulus (ε/2) (half_pos h)
 
+lemma δ_pos {f : C(I, ℝ)} {ε : ℝ} {h : 0 < ε} : 0 < δ f ε h := f.modulus_pos
+
 /--
 The set of points `k` so `k/n` is within `δ` of `x`.
 -/
@@ -188,12 +190,8 @@ lemma le_of_mem_S_compl
   (1 : ℝ) ≤ (δ f ε h)^(-2 : ℤ) * (x - k/ₙ) ^ 2 :=
 begin
   simp only [finset.mem_compl, not_lt, set.mem_to_finset, set.mem_set_of_eq, S] at m,
-  field_simp,
-  erw [le_div_iff (pow_pos f.modulus_pos 2), one_mul],
-  apply sq_le_sq,
-  rw abs_eq_self.mpr (le_of_lt f.modulus_pos),
-  rw [dist_comm] at m,
-  exact m,
+  erw [zpow_neg, ← div_eq_inv_mul, one_le_div (pow_pos δ_pos 2), sq_le_sq, abs_of_pos δ_pos],
+  rwa [dist_comm] at m
 end
 
 end bernstein_approximation

src/number_theory/modular.lean

@@ -477,9 +477,8 @@ begin
   let c : ℝ := (c' : ℝ),
   suffices : 3 * c^2 < 4,
   { rw [← int.cast_pow, ← int.cast_three, ← int.cast_four, ← int.cast_mul, int.cast_lt] at this,
-    replace this : c'^2 ≤ 1^2, { linarith, },
-    rw ← abs_one,
-    exact abs_le_abs_of_sq_le_sq this, },
+    replace this : c' ^ 2 ≤ 1 ^ 2, { linarith, },
+    rwa [sq_le_sq, abs_one] at this },
   suffices : c ≠ 0 → 9 * c^4 < 16,
   { rcases eq_or_ne c 0 with hc | hc,
     { rw hc, norm_num, },