[Merged by Bors] - feat(Parity): add lemmas about x ^ n = ±y ^ n

Mathlib/Data/Nat/Parity.lean

@@ -336,13 +336,44 @@ end Involutive
 
 end Function
 
-variable {R : Type*} [Monoid R] [HasDistribNeg R] {n : ℕ}
-
-theorem neg_one_pow_eq_one_iff_even (h : (-1 : R) ≠ 1) : (-1 : R) ^ n = 1 ↔ Even n :=
+theorem neg_one_pow_eq_one_iff_even {R : Type*} [Monoid R] [HasDistribNeg R] {n : ℕ}
+    (h : (-1 : R) ≠ 1) : (-1 : R) ^ n = 1 ↔ Even n :=
   ⟨fun h' => of_not_not fun hn => h <| (Odd.neg_one_pow <| odd_iff_not_even.mpr hn).symm.trans h',
     Even.neg_one_pow⟩
 #align neg_one_pow_eq_one_iff_even neg_one_pow_eq_one_iff_even
 
+section LinearOrderedRing
+
+variable {R : Type*} [LinearOrderedRing R] {a b : R} {n : ℕ}
+
+theorem pow_eq_pow_iff_of_ne_zero (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n :=
+  match n.even_xor_odd with
+  | .inl hne => by simp only [*, and_true, ← abs_eq_abs,
+    ← pow_left_inj (abs_nonneg a) (abs_nonneg b) hn, hne.1.pow_abs]
+  | .inr hn => by simp [hn, (hn.1.strictMono_pow (R := R)).injective.eq_iff]
+
+theorem pow_eq_pow_iff_cases : a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n := by
+  rcases eq_or_ne n 0 with rfl | hn <;> simp [pow_eq_pow_iff_of_ne_zero, *]
+
+theorem pow_eq_one_iff_of_ne_zero (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n := by
+  simp [← pow_eq_pow_iff_of_ne_zero hn]
+
+theorem pow_eq_one_iff_cases : a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n := by
+  simp [← pow_eq_pow_iff_cases]
+
+theorem pow_eq_neg_pow_iff (hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n :=
+  match n.even_or_odd with
+  | .inl he =>
+    suffices a ^ n > -b ^ n by simpa [he] using this.ne'
+    lt_of_lt_of_le (by simp [he.pow_pos hb]) (he.pow_nonneg _)
+  | .inr ho => by
+    simp only [ho, and_true, ← ho.neg_pow, (ho.strictMono_pow (R := R)).injective.eq_iff]
+
+theorem pow_eq_neg_one_iff : a ^ n = -1 ↔ a = -1 ∧ Odd n := by
+  simpa using pow_eq_neg_pow_iff (R := R) one_ne_zero
+
+end LinearOrderedRing
+
 /-- If `a` is even, then `n` is odd iff `n % a` is odd. -/
 theorem Odd.mod_even_iff {n a : ℕ} (ha : Even a) : Odd (n % a) ↔ Odd n :=
   ((even_sub' <| mod_le n a).mp <|

Mathlib/GroupTheory/SpecificGroups/Alternating.lean

@@ -73,8 +73,7 @@ theorem mem_alternatingGroup {f : Perm α} : f ∈ alternatingGroup α ↔ sign
 
 theorem prod_list_swap_mem_alternatingGroup_iff_even_length {l : List (Perm α)}
     (hl : ∀ g ∈ l, IsSwap g) : l.prod ∈ alternatingGroup α ↔ Even l.length := by
-  rw [mem_alternatingGroup, sign_prod_list_swap hl, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
-    Units.coe_neg_one, neg_one_pow_eq_one_iff_even]
+  rw [mem_alternatingGroup, sign_prod_list_swap hl, neg_one_pow_eq_one_iff_even]
   decide
 #align equiv.perm.prod_list_swap_mem_alternating_group_iff_even_length Equiv.Perm.prod_list_swap_mem_alternatingGroup_iff_even_length
 
@@ -284,8 +283,7 @@ theorem isConj_swap_mul_swap_of_cycleType_two {g : Perm (Fin 5)} (ha : g ∈ alt
     le_of_mul_le_mul_right (le_trans h (by simp only [card_fin]; ring_nf; decide)) (by simp)
   rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha
   norm_num at ha
-  rw [pow_add, pow_mul, Int.units_pow_two, one_mul, Units.ext_iff, Units.val_one,
-    Units.val_pow_eq_pow_val, Units.coe_neg_one, neg_one_pow_eq_one_iff_even _] at ha
+  rw [pow_add, pow_mul, Int.units_pow_two, one_mul, neg_one_pow_eq_one_iff_even] at ha
   swap; · decide
   rw [isConj_iff_cycleType_eq, h2]
   interval_cases h_1 : Multiset.card g.cycleType