feat: minor refactors for speedups/easier unification (#8884)

I think these are all positive or neutral in isolation, and they avoid breakages from a more interesting PR (providing a `@[csimp]` lemma for `npowRec`).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Counterexamples/Monic_nonRegular.lean

@@ -56,19 +56,22 @@ instance : Mul N₃ where
   | _, 0 => 0
   | _, _ => more
 
-instance : CommSemiring N₃ where
-  add_assoc := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
-  zero_add  := by rintro ⟨⟩ <;> rfl
-  add_zero  := by rintro ⟨⟩ <;> rfl
-  add_comm  := by rintro ⟨⟩ ⟨⟩ <;> rfl
-  left_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
-  right_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
+instance : CommMonoid N₃ where
   mul_assoc := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
-  mul_comm := by rintro ⟨⟩ ⟨⟩ <;> rfl
-  zero_mul := by rintro ⟨⟩ <;> rfl
-  mul_zero := by rintro ⟨⟩ <;> rfl
   one_mul := by rintro ⟨⟩ <;> rfl
   mul_one := by rintro ⟨⟩ <;> rfl
+  mul_comm := by rintro ⟨⟩ ⟨⟩ <;> rfl
+
+instance : CommSemiring N₃ :=
+  { (inferInstance : CommMonoid N₃) with
+    add_assoc := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
+    zero_add  := by rintro ⟨⟩ <;> rfl
+    add_zero  := by rintro ⟨⟩ <;> rfl
+    add_comm  := by rintro ⟨⟩ ⟨⟩ <;> rfl
+    left_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
+    right_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
+    zero_mul := by rintro ⟨⟩ <;> rfl
+    mul_zero := by rintro ⟨⟩ <;> rfl }
 
 theorem X_add_two_mul_X_add_two : (X + C 2 : N₃[X]) * (X + C 2) = (X + C 2) * (X + C 3) := by
   simp only [mul_add, add_mul, X_mul, add_assoc]

Mathlib/Algebra/Module/LocalizedModule.lean

@@ -237,11 +237,9 @@ theorem mk_neg {M : Type*} [AddCommGroup M] [Module R M] {m : M} {s : S} : mk (-
   rfl
 #align localized_module.mk_neg LocalizedModule.mk_neg
 
-set_option maxHeartbeats 500000 in
 instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} :
-    Semiring (LocalizedModule S A) :=
-  { show (AddCommMonoid (LocalizedModule S A)) by infer_instance with
-    mul := fun m₁ m₂ =>
+    Monoid (LocalizedModule S A) :=
+  { mul := fun m₁ m₂ =>
       liftOn₂ m₁ m₂ (fun x₁ x₂ => LocalizedModule.mk (x₁.1 * x₂.1) (x₁.2 * x₂.2))
         (by
           rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨b₁, t₁⟩ ⟨b₂, t₂⟩ ⟨u₁, e₁⟩ ⟨u₂, e₂⟩
@@ -254,6 +252,23 @@ instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} :
           all_goals
             rw [smul_smul, mul_mul_mul_comm, ← smul_eq_mul, ← smul_eq_mul A, smul_smul_smul_comm,
               mul_smul, mul_smul])
+    one := mk 1 (1 : S)
+    one_mul := by
+      rintro ⟨a, s⟩
+      exact mk_eq.mpr ⟨1, by simp only [one_mul, one_smul]⟩
+    mul_one := by
+      rintro ⟨a, s⟩
+      exact mk_eq.mpr ⟨1, by simp only [mul_one, one_smul]⟩
+    mul_assoc := by
+      rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
+      apply mk_eq.mpr _
+      use 1
+      simp only [one_mul, smul_smul, ← mul_assoc, mul_right_comm] }
+
+instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} :
+    Semiring (LocalizedModule S A) :=
+  { show (AddCommMonoid (LocalizedModule S A)) by infer_instance,
+    show (Monoid (LocalizedModule S A)) by infer_instance with
     left_distrib := by
       rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
       apply mk_eq.mpr _
@@ -271,19 +286,7 @@ instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} :
       exact mk_eq.mpr ⟨1, by simp only [zero_mul, smul_zero]⟩
     mul_zero := by
       rintro ⟨a, s⟩
-      exact mk_eq.mpr ⟨1, by simp only [mul_zero, smul_zero]⟩
-    mul_assoc := by
-      rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
-      apply mk_eq.mpr _
-      use 1
-      simp only [one_mul, smul_smul, ← mul_assoc, mul_right_comm]
-    one := mk 1 (1 : S)
-    one_mul := by
-      rintro ⟨a, s⟩
-      exact mk_eq.mpr ⟨1, by simp only [one_mul, one_smul]⟩
-    mul_one := by
-      rintro ⟨a, s⟩
-      exact mk_eq.mpr ⟨1, by simp only [mul_one, one_smul]⟩ }
+      exact mk_eq.mpr ⟨1, by simp only [mul_zero, smul_zero]⟩ }
 
 instance {A : Type*} [CommSemiring A] [Algebra R A] {S : Submonoid R} :
     CommSemiring (LocalizedModule S A) :=

Mathlib/Data/Num/Lemmas.lean

@@ -1428,19 +1428,22 @@ instance linearOrder : LinearOrder ZNum where
   decidableLT := ZNum.decidableLT
 #align znum.linear_order ZNum.linearOrder
 
-instance addCommGroup : AddCommGroup ZNum where
+instance addMonoid : AddMonoid ZNum where
   add := (· + ·)
   add_assoc := by transfer
   zero := 0
   zero_add := zero_add
   add_zero := add_zero
-  add_comm := by transfer
-  neg := Neg.neg
-  add_left_neg := by transfer
+
+instance addCommGroup : AddCommGroup ZNum :=
+  { ZNum.addMonoid with
+    add_comm := by transfer
+    neg := Neg.neg
+    add_left_neg := by transfer }
 #align znum.add_comm_group ZNum.addCommGroup
 
 instance addMonoidWithOne : AddMonoidWithOne ZNum :=
-  { ZNum.addCommGroup with
+  { ZNum.addMonoid with
     one := 1
     natCast := fun n => ZNum.ofInt' n
     natCast_zero := show (Num.ofNat' 0).toZNum = 0 by rw [Num.ofNat'_zero]; rfl

Mathlib/GroupTheory/Perm/Basic.lean

@@ -714,8 +714,8 @@ lemma BijOn.perm_pow : BijOn f s s → ∀ n : ℕ, BijOn (f ^ n) s s := by
 #align set.bij_on.perm_pow Set.BijOn.perm_pow
 
 lemma BijOn.perm_zpow (hf : BijOn f s s) : ∀ n : ℤ, BijOn (f ^ n) s s
-  | (Int.ofNat _) => hf.perm_pow _
-  | (Int.negSucc _) => (hf.perm_pow _).perm_inv
+  | (Int.ofNat n) => hf.perm_pow n
+  | (Int.negSucc n) => (hf.perm_pow (n + 1)).perm_inv
 #align set.bij_on.perm_zpow Set.BijOn.perm_zpow
 
 end Set