chore: Move Commute results earlier (#9440)

These lemmas aren't really proved any faster using units, and I will soon need them not to be proved using units.

Part of #9411

Mathlib/Algebra/Group/Commute/Basic.lean

@@ -58,4 +58,38 @@ protected theorem div_div_div_comm (hbc : Commute b c) (hbd : Commute b⁻¹ d)
 
 end DivisionMonoid
 
+section Group
+variable [Group G] {a b : G}
+
+@[to_additive (attr := simp)]
+lemma inv_left_iff : Commute a⁻¹ b ↔ Commute a b := SemiconjBy.inv_symm_left_iff
+#align commute.inv_left_iff Commute.inv_left_iff
+#align add_commute.neg_left_iff AddCommute.neg_left_iff
+
+@[to_additive] alias ⟨_, inv_left⟩ := inv_left_iff
+#align commute.inv_left Commute.inv_left
+#align add_commute.neg_left AddCommute.neg_left
+
+@[to_additive (attr := simp)]
+lemma inv_right_iff : Commute a b⁻¹ ↔ Commute a b := SemiconjBy.inv_right_iff
+#align commute.inv_right_iff Commute.inv_right_iff
+#align add_commute.neg_right_iff AddCommute.neg_right_iff
+
+@[to_additive] alias ⟨_, inv_right⟩ := inv_right_iff
+#align commute.inv_right Commute.inv_right
+#align add_commute.neg_right AddCommute.neg_right
+
+@[to_additive]
+protected lemma inv_mul_cancel (h : Commute a b) : a⁻¹ * b * a = b := by
+  rw [h.inv_left.eq, inv_mul_cancel_right]
+#align commute.inv_mul_cancel Commute.inv_mul_cancel
+#align add_commute.neg_add_cancel AddCommute.neg_add_cancel
+
+@[to_additive]
+lemma inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b := by
+  rw [← mul_assoc, h.inv_mul_cancel]
+#align commute.inv_mul_cancel_assoc Commute.inv_mul_cancel_assoc
+#align add_commute.neg_add_cancel_assoc AddCommute.neg_add_cancel_assoc
+
+end Group
 end Commute

Mathlib/Algebra/Group/Commute/Units.lean

@@ -99,65 +99,4 @@ theorem _root_.isUnit_mul_self_iff : IsUnit (a * a) ↔ IsUnit a :=
 #align is_add_unit_add_self_iff isAddUnit_add_self_iff
 
 end Monoid
-
-section Group
-
-variable [Group G] {a b : G}
-
-@[to_additive]
-theorem inv_right : Commute a b → Commute a b⁻¹ :=
-  SemiconjBy.inv_right
-#align commute.inv_right Commute.inv_right
-#align add_commute.neg_right AddCommute.neg_right
-
-@[to_additive (attr := simp)]
-theorem inv_right_iff : Commute a b⁻¹ ↔ Commute a b :=
-  SemiconjBy.inv_right_iff
-#align commute.inv_right_iff Commute.inv_right_iff
-#align add_commute.neg_right_iff AddCommute.neg_right_iff
-
-@[to_additive]
-theorem inv_left : Commute a b → Commute a⁻¹ b :=
-  SemiconjBy.inv_symm_left
-#align commute.inv_left Commute.inv_left
-#align add_commute.neg_left AddCommute.neg_left
-
-@[to_additive (attr := simp)]
-theorem inv_left_iff : Commute a⁻¹ b ↔ Commute a b :=
-  SemiconjBy.inv_symm_left_iff
-#align commute.inv_left_iff Commute.inv_left_iff
-#align add_commute.neg_left_iff AddCommute.neg_left_iff
-
-@[to_additive]
-protected theorem inv_mul_cancel (h : Commute a b) : a⁻¹ * b * a = b := by
-  rw [h.inv_left.eq, inv_mul_cancel_right]
-#align commute.inv_mul_cancel Commute.inv_mul_cancel
-#align add_commute.neg_add_cancel AddCommute.neg_add_cancel
-
-@[to_additive]
-theorem inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b := by
-  rw [← mul_assoc, h.inv_mul_cancel]
-#align commute.inv_mul_cancel_assoc Commute.inv_mul_cancel_assoc
-#align add_commute.neg_add_cancel_assoc AddCommute.neg_add_cancel_assoc
-
-end Group
-
 end Commute
-
-section CommGroup
-
-variable [CommGroup G] (a b : G)
-
-@[to_additive (attr := simp)]
-theorem inv_mul_cancel_comm : a⁻¹ * b * a = b :=
-  (Commute.all a b).inv_mul_cancel
-#align inv_mul_cancel_comm inv_mul_cancel_comm
-#align neg_add_cancel_comm neg_add_cancel_comm
-
-@[to_additive (attr := simp)]
-theorem inv_mul_cancel_comm_assoc : a⁻¹ * (b * a) = b :=
-  (Commute.all a b).inv_mul_cancel_assoc
-#align inv_mul_cancel_comm_assoc inv_mul_cancel_comm_assoc
-#align neg_add_cancel_comm_assoc neg_add_cancel_comm_assoc
-
-end CommGroup

Mathlib/Algebra/Group/Defs.lean

@@ -998,6 +998,10 @@ theorem zpow_ofNat (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
 #align zpow_of_nat zpow_ofNat
 #align of_nat_zsmul ofNat_zsmul
 
+@[to_additive (attr := simp, norm_cast) coe_nat_zsmul]
+lemma zpow_coe_nat (a : G) (n : ℕ) : a ^ (Nat.cast n : ℤ) = a ^ n := zpow_ofNat ..
+#align coe_nat_zsmul coe_nat_zsmul
+
 theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹ := by
   rw [← zpow_ofNat]
   exact DivInvMonoid.zpow_neg' n a
@@ -1263,6 +1267,16 @@ instance (priority := 100) CommGroup.toCancelCommMonoid : CancelCommMonoid G :=
 instance (priority := 100) CommGroup.toDivisionCommMonoid : DivisionCommMonoid G :=
   { ‹CommGroup G›, Group.toDivisionMonoid with }
 
+@[to_additive (attr := simp)] lemma inv_mul_cancel_comm (a b : G) : a⁻¹ * b * a = b := by
+  rw [mul_comm, mul_inv_cancel_left]
+#align inv_mul_cancel_comm inv_mul_cancel_comm
+#align neg_add_cancel_comm neg_add_cancel_comm
+
+@[to_additive (attr := simp)] lemma inv_mul_cancel_comm_assoc (a b : G) : a⁻¹ * (b * a) = b := by
+  rw [mul_comm, mul_inv_cancel_right]
+#align inv_mul_cancel_comm_assoc inv_mul_cancel_comm_assoc
+#align neg_add_cancel_comm_assoc neg_add_cancel_comm_assoc
+
 end CommGroup
 
 /-! We initialize all projections for `@[simps]` here, so that we don't have to do it in later

Mathlib/Algebra/Group/Semiconj/Basic.lean

@@ -9,29 +9,47 @@ import Mathlib.Algebra.Group.Basic
 #align_import algebra.group.semiconj from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
 
 /-!
-# Lemmas about semiconjugate elements of a semigroup
+# Lemmas about semiconjugate elements of a group
 
 -/
 
 namespace SemiconjBy
+variable {G : Type*}
 
 section DivisionMonoid
-
-variable {G : Type*} [DivisionMonoid G] {a x y : G}
+variable [DivisionMonoid G] {a x y : G}
 
 @[to_additive (attr := simp)]
-theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x :=
-  inv_involutive.injective.eq_iff.symm.trans <| by
-    rw [mul_inv_rev, mul_inv_rev, inv_inv, inv_inv, inv_inv, eq_comm, SemiconjBy]
+theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x := by
+  simp_rw [SemiconjBy, ← mul_inv_rev, inv_inj, eq_comm]
 #align semiconj_by.inv_inv_symm_iff SemiconjBy.inv_inv_symm_iff
 #align add_semiconj_by.neg_neg_symm_iff AddSemiconjBy.neg_neg_symm_iff
 
-@[to_additive]
-theorem inv_inv_symm : SemiconjBy a x y → SemiconjBy a⁻¹ y⁻¹ x⁻¹ :=
-  inv_inv_symm_iff.2
+@[to_additive] alias ⟨_, inv_inv_symm⟩ := inv_inv_symm_iff
 #align semiconj_by.inv_inv_symm SemiconjBy.inv_inv_symm
 #align add_semiconj_by.neg_neg_symm AddSemiconjBy.neg_neg_symm
 
 end DivisionMonoid
 
+section Group
+variable [Group G] {a x y : G}
+
+@[to_additive (attr := simp)] lemma inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y := by
+  simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]
+#align semiconj_by.inv_symm_left_iff SemiconjBy.inv_symm_left_iff
+#align add_semiconj_by.neg_symm_left_iff AddSemiconjBy.neg_symm_left_iff
+
+@[to_additive] alias ⟨_, inv_symm_left⟩ := inv_symm_left_iff
+#align semiconj_by.inv_symm_left SemiconjBy.inv_symm_left
+#align add_semiconj_by.neg_symm_left AddSemiconjBy.neg_symm_left
+
+@[to_additive (attr := simp)] lemma inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y := by
+  rw [← inv_symm_left_iff, inv_inv_symm_iff]
+#align add_semiconj_by.neg_right_iff AddSemiconjBy.neg_right_iff
+
+@[to_additive] alias ⟨_, inv_right⟩ := inv_right_iff
+#align semiconj_by.inv_right SemiconjBy.inv_right
+#align add_semiconj_by.neg_right AddSemiconjBy.neg_right
+
+end Group
 end SemiconjBy

Mathlib/Algebra/Group/Semiconj/Units.lean

@@ -88,38 +88,6 @@ theorem units_val_iff {a x y : Mˣ} : SemiconjBy (a : M) x y ↔ SemiconjBy a x
 #align add_semiconj_by.add_units_coe_iff AddSemiconjBy.addUnits_val_iff
 
 end Monoid
-
-section Group
-
-variable [Group G] {a x y : G}
-
-@[to_additive (attr := simp)]
-theorem inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y :=
-  @units_inv_right_iff G _ a ⟨x, x⁻¹, mul_inv_self x, inv_mul_self x⟩
-    ⟨y, y⁻¹, mul_inv_self y, inv_mul_self y⟩
-#align semiconj_by.inv_right_iff SemiconjBy.inv_right_iff
-#align add_semiconj_by.neg_right_iff AddSemiconjBy.neg_right_iff
-
-@[to_additive]
-theorem inv_right : SemiconjBy a x y → SemiconjBy a x⁻¹ y⁻¹ :=
-  inv_right_iff.2
-#align semiconj_by.inv_right SemiconjBy.inv_right
-#align add_semiconj_by.neg_right AddSemiconjBy.neg_right
-
-@[to_additive (attr := simp)]
-theorem inv_symm_left_iff : SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y :=
-  @units_inv_symm_left_iff G _ ⟨a, a⁻¹, mul_inv_self a, inv_mul_self a⟩ _ _
-#align semiconj_by.inv_symm_left_iff SemiconjBy.inv_symm_left_iff
-#align add_semiconj_by.neg_symm_left_iff AddSemiconjBy.neg_symm_left_iff
-
-@[to_additive]
-theorem inv_symm_left : SemiconjBy a x y → SemiconjBy a⁻¹ y x :=
-  inv_symm_left_iff.2
-#align semiconj_by.inv_symm_left SemiconjBy.inv_symm_left
-#align add_semiconj_by.neg_symm_left AddSemiconjBy.neg_symm_left
-
-end Group
-
 end SemiconjBy
 
 /-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/

Mathlib/Algebra/GroupPower/Basic.lean

@@ -3,9 +3,9 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
-import Mathlib.Algebra.Group.Commute.Units
+import Mathlib.Algebra.Group.Commute.Basic
 import Mathlib.Algebra.GroupWithZero.Defs
-import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Common
 
 #align_import algebra.group_power.basic from "leanprover-community/mathlib"@"9b2660e1b25419042c8da10bf411aa3c67f14383"
 

Mathlib/Data/Int/Basic.lean

@@ -88,11 +88,6 @@ lemma natAbs_cast (n : ℕ) : natAbs ↑n = n := rfl
 @[norm_cast]
 protected lemma coe_nat_sub {n m : ℕ} : n ≤ m → (↑(m - n) : ℤ) = ↑m - ↑n := ofNat_sub
 
-@[to_additive (attr := simp, norm_cast) coe_nat_zsmul]
-theorem _root_.zpow_coe_nat [DivInvMonoid G] (a : G) (n : ℕ) : a ^ (Nat.cast n : ℤ) = a ^ n :=
-  zpow_ofNat ..
-#align coe_nat_zsmul coe_nat_zsmul
-
 /-! ### Extra instances to short-circuit type class resolution
 
 These also prevent non-computable instances like `Int.normedCommRing` being used to construct