From ec61182178f58e9de85abbaa2cfb0dc9d224919a Mon Sep 17 00:00:00 2001
From: Bhavik Mehta <bhavikmehta8@gmail.com>
Date: Tue, 1 Feb 2022 18:24:10 +0000
Subject: [PATCH] feat(algebra/group_power): relate square equality and
 absolute value equality (#11683)

---
 src/algebra/group_power/order.lean          | 26 +++++++++++++++++++--
 src/analysis/inner_product_space/basic.lean |  2 +-
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/algebra/group_power/order.lean b/src/algebra/group_power/order.lean
index 3e61a970e6c7c..75ff4b4333d2f 100644
--- a/src/algebra/group_power/order.lean
+++ b/src/algebra/group_power/order.lean
@@ -320,11 +320,11 @@ 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 :=
+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' (h1 : -y < x) (h2 : x < y) : x ^ 2 < y ^ 2 :=
-sq_lt_sq (abs_lt.mpr ⟨h1, h2⟩)
+sq_lt_sq (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
@@ -356,6 +356,28 @@ end
 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]⟩
+
+@[simp] lemma sq_eq_one_iff (x : R) : x^2 = 1 ↔ x = 1 ∨ x = -1 :=
+by rw [←abs_eq_abs, ←sq_eq_sq_iff_abs_eq_abs, one_pow]
+
+lemma sq_ne_one_iff (x : R) : x^2 ≠ 1 ↔ x ≠ 1 ∧ x ≠ -1 :=
+(not_iff_not.2 (sq_eq_one_iff _)).trans not_or_distrib
+
+@[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
+
+@[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
+
+@[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
+
+@[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
+
 end linear_ordered_ring
 
 section linear_ordered_comm_ring
diff --git a/src/analysis/inner_product_space/basic.lean b/src/analysis/inner_product_space/basic.lean
index 631385064d334..1edce8dd21f07 100644
--- a/src/analysis/inner_product_space/basic.lean
+++ b/src/analysis/inner_product_space/basic.lean
@@ -1865,7 +1865,7 @@ begin
     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 (norm_nonneg _),
+      rw [_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 },