chore: remove redundant field from Lean.Grind.IntModule (#8879)

src/Init/Grind/Module/Basic.lean

@@ -23,7 +23,6 @@ class NatModule (M : Type u) extends Zero M, Add M, HMul Nat M M where
   add_hmul : ∀ n m : Nat, ∀ a : M, (n + m) * a = n * a + m * a
   hmul_zero : ∀ n : Nat, n * (0 : M) = 0
   hmul_add : ∀ n : Nat, ∀ a b : M, n * (a + b) = n * a + n * b
-  mul_hmul : ∀ n m : Nat, ∀ a : M, (n * m) * a = n * (m * a)
 
 attribute [instance 100] NatModule.toZero NatModule.toAdd NatModule.toHMul
 
@@ -36,7 +35,6 @@ class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M w
   add_hmul : ∀ n m : Int, ∀ a : M, (n + m) * a = n * a + m * a
   hmul_zero : ∀ n : Int, n * (0 : M) = 0
   hmul_add : ∀ n : Int, ∀ a b : M, n * (a + b) = n * a + n * b
-  mul_hmul : ∀ n m : Int, ∀ a : M, (n * m) * a = n * (m * a)
   neg_add_cancel : ∀ a : M, -a + a = 0
   sub_eq_add_neg : ∀ a b : M, a - b = a + -b
 
@@ -47,6 +45,12 @@ variable {M : Type u} [NatModule M]
 theorem zero_add (a : M) : 0 + a = a := by
   rw [add_comm, add_zero]
 
+theorem mul_hmul (n m : Nat) (a : M) : (n * m) * a = n * (m * a) := by
+  induction n with
+  | zero => simp [zero_hmul]
+  | succ n ih =>
+    rw [Nat.add_one_mul, add_hmul, ih, add_hmul, one_hmul]
+
 end NatModule
 
 namespace IntModule
@@ -58,8 +62,7 @@ instance toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
     hMul a x := (a : Int) * x
     hmul_zero := by simp [IntModule.hmul_zero]
     add_hmul := by simp [IntModule.add_hmul]
-    hmul_add := by simp [IntModule.hmul_add]
-    mul_hmul := by simp [IntModule.mul_hmul] }
+    hmul_add := by simp [IntModule.hmul_add] }
 
 variable {M : Type u} [IntModule M]
 
@@ -136,6 +139,19 @@ theorem hmul_sub (k : Int) (a b : M) : k * (a - b) = k * a - k * b := by
 theorem sub_hmul (k₁ k₂ : Int) (a : M) : (k₁ - k₂) * a = k₁ * a - k₂ * a := by
   rw [Int.sub_eq_add_neg, add_hmul, neg_hmul, ← sub_eq_add_neg]
 
+private theorem nat_mul_hmul (n : Nat) (m : Int) (a : M) :
+    ((n : Int) * m) * a = (n : Int) * (m * a) := by
+  induction n with
+  | zero => simp [zero_hmul]
+  | succ n ih =>
+    rw [Int.natCast_add, Int.add_mul, add_hmul, Int.natCast_one,
+      Int.one_mul, add_hmul, one_hmul, ih]
+
+theorem mul_hmul (n m : Int) (a : M) : (n * m) * a = n * (m * a) := by
+  match n with
+  | (n : Nat) => exact nat_mul_hmul n m a
+  | -(n + 1 : Nat) => rw [Int.neg_mul, neg_hmul, nat_mul_hmul, neg_hmul]
+
 end IntModule
 
 /--

src/Init/Grind/Ring/Basic.lean

@@ -127,7 +127,6 @@ instance : NatModule α where
   add_hmul := by simp [natCast_add, right_distrib]
   hmul_zero := by simp [mul_zero]
   hmul_add := by simp [left_distrib]
-  mul_hmul := by simp [natCast_mul, mul_assoc]
 
 theorem hmul_eq_natCast_mul {α} [Semiring α] {k : Nat} {a : α} : HMul.hMul (α := Nat) k a = (k : α) * a := rfl
 
@@ -294,7 +293,6 @@ instance : IntModule α where
   add_hmul := by simp [intCast_add, right_distrib]
   hmul_zero := by simp [mul_zero]
   hmul_add := by simp [left_distrib]
-  mul_hmul := by simp [intCast_mul, mul_assoc]
   neg_add_cancel := by simp [neg_add_cancel]
   sub_eq_add_neg := by simp [sub_eq_add_neg]