fix tests

src/Init/Data/BitVec/Basic.lean

@@ -35,7 +35,12 @@ protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) : BitVec n :=
 
 section Nat
 
-instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
+/--
+`NatCast` instance for `BitVec`.
+-/
+-- As this is a lossy conversion, it should be removed as a global instance.
+instance instNatCast : NatCast (BitVec w) where
+  natCast x := BitVec.ofNat w x
 
 /-- Theorem for normalizing the bitvector literal representation. -/
 -- TODO: This needs more usage data to assess which direction the simp should go.

src/Init/Grind/Module/Basic.lean

@@ -20,6 +20,24 @@ class AddRightCancel (M : Type u) [Add M] where
   /-- Addition is right-cancellative. -/
   add_right_cancel : ∀ a b c : M, a + c = b + c → a = b
 
+class AddCommMonoid (M : Type u) extends Zero M, Add M where
+  /-- Zero is the right identity for addition. -/
+  add_zero : ∀ a : M, a + 0 = a
+  /-- Addition is commutative. -/
+  add_comm : ∀ a b : M, a + b = b + a
+  /-- Addition is associative. -/
+  add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
+
+attribute [instance 100] AddCommMonoid.toZero AddCommMonoid.toAdd
+
+class AddCommGroup (M : Type u) extends AddCommMonoid M, Neg M, Sub M where
+  /-- Negation is the left inverse of addition. -/
+  neg_add_cancel : ∀ a : M, -a + a = 0
+  /-- Subtraction is addition of the negative. -/
+  sub_eq_add_neg : ∀ a b : M, a - b = a + -b
+
+attribute [instance 100] AddCommGroup.toAddCommMonoid AddCommGroup.toNeg AddCommGroup.toSub
+
 /--
 A module over the natural numbers, i.e. a type with zero, addition, and scalar multiplication by natural numbers,
 satisfying appropriate compatibilities.
@@ -28,25 +46,21 @@ Equivalently, an additive commutative monoid.
 
 Use `IntModule` if the type has negation.
 -/
-class NatModule (M : Type u) extends Zero M, Add M, HMul Nat M M where
-  /-- Zero is the right identity for addition. -/
-  add_zero : ∀ a : M, a + 0 = a
-  /-- Addition is commutative. -/
-  add_comm : ∀ a b : M, a + b = b + a
-  /-- Addition is associative. -/
-  add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
+class NatModule (M : Type u) extends AddCommMonoid M where
+  /-- Scalar multiplication by natural numbers. -/
+  [nsmul : HMul Nat M M]
   /-- Scalar multiplication by zero is zero. -/
-  zero_hmul : ∀ a : M, 0 * a = 0
+  zero_nsmul : ∀ a : M, 0 * a = 0
   /-- Scalar multiplication by one is the identity. -/
-  one_hmul : ∀ a : M, 1 * a = a
+  one_nsmul : ∀ a : M, 1 * a = a
   /-- Scalar multiplication is distributive over addition in the natural numbers. -/
-  add_hmul : ∀ n m : Nat, ∀ a : M, (n + m) * a = n * a + m * a
+  add_nsmul : ∀ n m : Nat, ∀ a : M, (n + m) * a = n * a + m * a
   /-- Scalar multiplication of zero is zero. -/
-  hmul_zero : ∀ n : Nat, n * (0 : M) = 0
+  nsmul_zero : ∀ n : Nat, n * (0 : M) = 0
   /-- Scalar multiplication is distributive over addition in the module. -/
-  hmul_add : ∀ n : Nat, ∀ a b : M, n * (a + b) = n * a + n * b
+  nsmul_add : ∀ n : Nat, ∀ a b : M, n * (a + b) = n * a + n * b
 
-attribute [instance 100] NatModule.toZero NatModule.toAdd NatModule.toHMul
+attribute [instance 100] NatModule.toAddCommMonoid NatModule.nsmul
 
 /--
 A module over the integers, i.e. a type with zero, addition, negation, subtraction, and scalar multiplication by integers,
@@ -54,83 +68,54 @@ satisfying appropriate compatibilities.
 
 Equivalently, an additive commutative group.
 -/
-class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M where
+class IntModule (M : Type u) extends AddCommGroup M where
   /-- Scalar multiplication by natural numbers. -/
-  [hmulNat : HMul Nat M M]
+  [nsmul : HMul Nat M M]
   /-- Scalar multiplication by integers. -/
-  [hmulInt : HMul Int M M]
-  /-- Zero is the right identity for addition. -/
-  add_zero : ∀ a : M, a + 0 = a
-  /-- Addition is commutative. -/
-  add_comm : ∀ a b : M, a + b = b + a
-  /-- Addition is associative. -/
-  add_assoc : ∀ a b c : M, a + b + c = a + (b + c)
+  [zsmul : HMul Int M M]
   /-- Scalar multiplication by zero is zero. -/
-  zero_hmul : ∀ a : M, (0 : Int) * a = 0
+  zero_zsmul : ∀ a : M, (0 : Int) * a = 0
   /-- Scalar multiplication by one is the identity. -/
-  one_hmul : ∀ a : M, (1 : Int) * a = a
+  one_zsmul : ∀ a : M, (1 : Int) * a = a
   /-- Scalar multiplication is distributive over addition in the integers. -/
-  add_hmul : ∀ n m : Int, ∀ a : M, (n + m) * a = n * a + m * a
+  add_zsmul : ∀ n m : Int, ∀ a : M, (n + m) * a = n * a + m * a
   /-- Scalar multiplication of zero is zero. -/
-  hmul_zero : ∀ n : Int, n * (0 : M) = 0
-  /-- Scalar multiplication is distributive over addition in the module. -/
-  hmul_add : ∀ n : Int, ∀ a b : M, n * (a + b) = n * a + n * b
-  /-- Negation is the left inverse of addition. -/
-  neg_add_cancel : ∀ a : M, -a + a = 0
-  /-- Subtraction is addition of the negative. -/
-  sub_eq_add_neg : ∀ a b : M, a - b = a + -b
+  zsmul_zero : ∀ n : Int, n * (0 : M) = 0
+  /-- Scalar multiplication by integers is distributive over addition in the module. -/
+  zsmul_add : ∀ n : Int, ∀ a b : M, n * (a + b) = n * a + n * b
   /-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers. -/
-  hmul_nat : ∀ n : Nat, ∀ a : M, (n : Int) * a = n * a
+  zsmul_natCast_eq_nsmul : ∀ n : Nat, ∀ a : M, (n : Int) * a = n * a
 
-namespace NatModule
+attribute [instance 100] IntModule.toAddCommGroup IntModule.zsmul
 
-variable {M : Type u} [NatModule M]
+instance (priority := 100) IntModule.toNatModule [I : IntModule M] : NatModule M :=
+  { I with
+    zero_nsmul a := by rw [← zsmul_natCast_eq_nsmul, Int.natCast_zero, zero_zsmul]
+    one_nsmul a := by rw [← zsmul_natCast_eq_nsmul, Int.natCast_one, one_zsmul]
+    add_nsmul n m a := by rw [← zsmul_natCast_eq_nsmul, Int.natCast_add, add_zsmul, zsmul_natCast_eq_nsmul, zsmul_natCast_eq_nsmul]
+    nsmul_zero n := by rw [← zsmul_natCast_eq_nsmul, zsmul_zero]
+    nsmul_add n a b := by rw [← zsmul_natCast_eq_nsmul, zsmul_add, zsmul_natCast_eq_nsmul, zsmul_natCast_eq_nsmul] }
+
+namespace AddCommMonoid
+
+variable {M : Type u} [AddCommMonoid 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]
-
-instance (priority := 100) (M : Type u) [NatModule M] : SMul Nat M where
-  smul a x := a * x
-
-end NatModule
-
-namespace IntModule
-
-attribute [instance 100] IntModule.toZero IntModule.toAdd IntModule.toNeg IntModule.toSub
-  IntModule.hmulNat IntModule.hmulInt
-
-instance toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
-  { i with
-    hMul := i.hmulNat.hMul
-    zero_hmul := by simp [← hmul_nat, zero_hmul]
-    one_hmul := by simp [← hmul_nat, one_hmul]
-    hmul_zero := by simp [← hmul_nat, hmul_zero]
-    add_hmul := by simp [← hmul_nat, add_hmul]
-    hmul_add := by simp [← hmul_nat, hmul_add] }
-
-instance (priority := 100) (M : Type u) [IntModule M] : SMul Nat M where
-  smul a x := a * x
-
-instance (priority := 100) (M : Type u) [IntModule M] : SMul Int M where
-  smul a x := a * x
-
-variable {M : Type u} [IntModule M]
-
-theorem zero_add (a : M) : 0 + a = a := by
-  rw [add_comm, add_zero]
-
-theorem add_neg_cancel (a : M) : a + -a = 0 := by
-  rw [add_comm, neg_add_cancel]
-
 theorem add_left_comm (a b c : M) : a + (b + c) = b + (a + c) := by
   rw [← add_assoc, ← add_assoc, add_comm a]
 
+end AddCommMonoid
+
+namespace AddCommGroup
+
+variable {M : Type u} [AddCommGroup M]
+open AddCommMonoid
+
+theorem add_neg_cancel (a : M) : a + -a = 0 := by
+  rw [add_comm, neg_add_cancel]
+
 theorem add_left_inj {a b : M} (c : M) : a + c = b + c ↔ a = b :=
   ⟨fun h => by simpa [add_assoc, add_neg_cancel, add_zero] using (congrArg (· + -c) h),
    fun g => congrArg (· + c) g⟩
@@ -175,35 +160,65 @@ theorem add_sub_cancel {a b : M} : a + b - b = a := by
 theorem sub_add_cancel {a b : M} : a - b + b = a := by
   rw [sub_eq_add_neg, add_assoc, neg_add_cancel, add_zero]
 
-theorem neg_hmul (n : Int) (a : M) : (-n) * a = - (n * a) := by
+theorem neg_eq_iff (a b : M) : -a = b ↔ a = -b := by
+  constructor
+  · intro h
+    rw [← neg_neg a, h]
+  · intro h
+    rw [← neg_neg b, h]
+
+end AddCommGroup
+
+namespace NatModule
+
+variable {M : Type u} [NatModule M]
+
+theorem mul_nsmul (n m : Nat) (a : M) : (n * m) * a = n * (m * a) := by
+  induction n with
+  | zero => simp [zero_nsmul]
+  | succ n ih =>
+    rw [Nat.add_one_mul, add_nsmul, ih, add_nsmul, one_nsmul]
+
+instance (priority := 100) (M : Type u) [NatModule M] : SMul Nat M where
+  smul a x := a * x
+
+end NatModule
+
+namespace IntModule
+
+open NatModule AddCommGroup
+
+instance (priority := 100) (M : Type u) [IntModule M] : SMul Int M where
+  smul a x := a * x
+
+variable {M : Type u} [IntModule M]
+
+theorem neg_zsmul (n : Int) (a : M) : (-n) * a = - (n * a) := by
   apply (add_left_inj (n * a)).mp
-  rw [← add_hmul, Int.add_left_neg, zero_hmul, neg_add_cancel]
+  rw [← add_zsmul, Int.add_left_neg, zero_zsmul, neg_add_cancel]
 
-theorem hmul_neg (n : Int) (a : M) : n * (-a) = - (n * a) := by
+theorem zsmul_neg (n : Int) (a : M) : n * (-a) = - (n * a) := by
   apply (add_left_inj (n * a)).mp
-  rw [← hmul_add, neg_add_cancel, neg_add_cancel, hmul_zero]
+  rw [← zsmul_add, neg_add_cancel, neg_add_cancel, zsmul_zero]
 
-theorem hmul_sub (k : Int) (a b : M) : k * (a - b) = k * a - k * b := by
-  rw [sub_eq_add_neg, hmul_add, hmul_neg, ← sub_eq_add_neg]
+theorem zsmul_sub (k : Int) (a b : M) : k * (a - b) = k * a - k * b := by
+  rw [sub_eq_add_neg, zsmul_add, zsmul_neg, ← sub_eq_add_neg]
 
-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]
+theorem sub_zsmul (k₁ k₂ : Int) (a : M) : (k₁ - k₂) * a = k₁ * a - k₂ * a := by
+  rw [Int.sub_eq_add_neg, add_zsmul, neg_zsmul, ← sub_eq_add_neg]
 
-theorem nat_zero_hmul (a : M) : (0 : Nat) * a = 0 := by
-  rw [← hmul_nat, Int.natCast_zero, zero_hmul]
-
-private theorem nat_mul_hmul (n : Nat) (m : Int) (a : M) :
+private theorem mul_zsmul_aux (n : Nat) (m : Int) (a : M) :
     ((n : Int) * m) * a = (n : Int) * (m * a) := by
   induction n with
-  | zero => simp [zero_hmul]
+  | zero => simp [zero_zsmul]
   | succ n ih =>
-    rw [Int.natCast_add, Int.add_mul, add_hmul, Int.natCast_one,
-      Int.one_mul, add_hmul, one_hmul, ih]
+    rw [Int.natCast_add, Int.add_mul, add_zsmul, Int.natCast_one,
+      Int.one_mul, add_zsmul, one_zsmul, ih]
 
-theorem mul_hmul (n m : Int) (a : M) : (n * m) * a = n * (m * a) := by
+theorem mul_zsmul (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]
+  | (n : Nat) => exact mul_zsmul_aux n m a
+  | -(n + 1 : Nat) => rw [Int.neg_mul, neg_zsmul, mul_zsmul_aux, neg_zsmul]
 
 end IntModule
 
@@ -225,31 +240,35 @@ export NoNatZeroDivisors (no_nat_zero_divisors)
 namespace NoNatZeroDivisors
 
 /-- Alternative constructor for `NoNatZeroDivisors` when we have an `IntModule`. -/
-def mk' {α} [IntModule α] (eq_zero_of_mul_eq_zero : ∀ (k : Nat) (a : α), k ≠ 0 → k * a = 0 → a = 0) : NoNatZeroDivisors α where
+def mk' {α} [IntModule α]
+    (eq_zero_of_mul_eq_zero : ∀ (k : Nat) (a : α), k ≠ 0 → k * a = 0 → a = 0) :
+    NoNatZeroDivisors α where
   no_nat_zero_divisors k a b h₁ h₂ := by
-    rw [← IntModule.sub_eq_zero_iff, ← IntModule.hmul_nat, ← IntModule.hmul_nat, ← IntModule.hmul_sub, IntModule.hmul_nat] at h₂
-    rw [← IntModule.sub_eq_zero_iff]
+    rw [← AddCommGroup.sub_eq_zero_iff, ← IntModule.zsmul_natCast_eq_nsmul,
+      ← IntModule.zsmul_natCast_eq_nsmul, ← IntModule.zsmul_sub,
+      IntModule.zsmul_natCast_eq_nsmul] at h₂
+    rw [← AddCommGroup.sub_eq_zero_iff]
     apply eq_zero_of_mul_eq_zero k (a - b) h₁ h₂
 
 theorem eq_zero_of_mul_eq_zero {α : Type u} [NatModule α] [NoNatZeroDivisors α] {k : Nat} {a : α}
     : k ≠ 0 → k * a = 0 → a = 0 := by
   intro h₁ h₂
   replace h₁ : k ≠ 0 := by intro h; simp [h] at h₁
-  exact no_nat_zero_divisors k a 0 h₁ (by rwa [NatModule.hmul_zero])
+  exact no_nat_zero_divisors k a 0 h₁ (by rwa [NatModule.nsmul_zero])
 
 end NoNatZeroDivisors
 
-instance [ToInt α (IntInterval.co lo hi)] [IntModule α] [ToInt.Zero α (IntInterval.co lo hi)] [ToInt.Add α (IntInterval.co lo hi)] : ToInt.Neg α (IntInterval.co lo hi) where
+instance [ToInt α (IntInterval.co lo hi)] [AddCommGroup α] [ToInt.Zero α (IntInterval.co lo hi)] [ToInt.Add α (IntInterval.co lo hi)] : ToInt.Neg α (IntInterval.co lo hi) where
   toInt_neg x := by
     have := (ToInt.Add.toInt_add (-x) x).symm
-    rw [IntModule.neg_add_cancel, ToInt.Zero.toInt_zero, ← ToInt.Zero.wrap_zero (α := α)] at this
+    rw [AddCommGroup.neg_add_cancel, ToInt.Zero.toInt_zero, ← ToInt.Zero.wrap_zero (α := α)] at this
     rw [IntInterval.wrap_eq_wrap_iff] at this
     simp at this
     rw [← ToInt.wrap_toInt]
     rw [IntInterval.wrap_eq_wrap_iff]
     simpa
 
-instance [ToInt α (IntInterval.co lo hi)] [IntModule α] [ToInt.Add α (IntInterval.co lo hi)] [ToInt.Neg α (IntInterval.co lo hi)] : ToInt.Sub α (IntInterval.co lo hi) :=
-  ToInt.Sub.of_sub_eq_add_neg IntModule.sub_eq_add_neg (by simp)
+instance [ToInt α (IntInterval.co lo hi)] [AddCommGroup α] [ToInt.Add α (IntInterval.co lo hi)] [ToInt.Neg α (IntInterval.co lo hi)] : ToInt.Sub α (IntInterval.co lo hi) :=
+  ToInt.Sub.of_sub_eq_add_neg AddCommGroup.sub_eq_add_neg (by simp)
 
 end Lean.Grind

src/Init/Grind/Module/Envelope.lean

@@ -19,9 +19,9 @@ variable [NatModule α]
 
 -- Helper instance for `ac_rfl`
 local instance : Std.Associative (· + · : α → α → α) where
-  assoc := NatModule.add_assoc
+  assoc := AddCommMonoid.add_assoc
 local instance : Std.Commutative (· + · : α → α → α) where
-  comm := NatModule.add_comm
+  comm := AddCommMonoid.add_comm
 
 @[local simp] private theorem exists_true : ∃ (_ : α), True := ⟨0, trivial⟩
 
@@ -33,10 +33,10 @@ def Q := Quot (r α)
 variable {α}
 
 theorem r_rfl (a : α × α) : r α a a := by
-  cases a; refine ⟨0, ?_⟩; simp [NatModule.add_zero]; ac_rfl
+  cases a; refine ⟨0, ?_⟩; simp [AddCommMonoid.add_zero]; ac_rfl
 
 theorem r_sym {a b : α × α} : r α a b → r α b a := by
-  cases a; cases b; simp [r]; intro h w; refine ⟨h, ?_⟩; simp [w, NatModule.add_comm]
+  cases a; cases b; simp [r]; intro h w; refine ⟨h, ?_⟩; simp [w, AddCommMonoid.add_comm]
 
 theorem r_trans {a b c : α × α} : r α a b → r α b c → r α a c := by
   cases a; cases b; cases c;
@@ -63,20 +63,20 @@ def Q.liftOn₂ (q₁ q₂ : Q α)
   induction q₂ using Quot.ind
   apply h; assumption; apply r_rfl
 
-attribute [local simp] Q.mk Q.liftOn₂ NatModule.add_zero
+attribute [local simp] Q.mk Q.liftOn₂ AddCommMonoid.add_zero
 
 def Q.ind {β : Q α → Prop} (mk : ∀ (a : α × α), β (Q.mk a)) (q : Q α) : β q :=
   Quot.ind mk q
 
-@[local simp] def hmulNat (n : Nat) (q : Q α) : (Q α) :=
+@[local simp] def nsmul (n : Nat) (q : Q α) : (Q α) :=
   q.liftOn (fun (a, b) => Q.mk (n * a, n * b))
     (by intro (a₁, b₁) (a₂, b₂)
         simp; intro k h; apply Quot.sound; simp
         refine ⟨n * k, ?_⟩
         replace h := congrArg (fun x : α => n * x) h
-        simpa [NatModule.hmul_add] using h)
+        simpa [NatModule.nsmul_add] using h)
 
-@[local simp] def hmulInt (n : Int) (q : Q α) : (Q α) :=
+@[local simp] def zsmul (n : Int) (q : Q α) : (Q α) :=
   q.liftOn (fun (a, b) => if n < 0 then Q.mk (n.natAbs * b, n.natAbs * a) else Q.mk (n.natAbs * a, n.natAbs * b))
     (by intro (a₁, b₁) (a₂, b₂)
         simp; intro k h;
@@ -84,11 +84,11 @@ def Q.ind {β : Q α → Prop} (mk : ∀ (a : α × α), β (Q.mk a)) (q : Q α)
         · apply Quot.sound; simp
           refine ⟨n.natAbs * k, ?_⟩
           replace h := congrArg (fun x : α => n.natAbs * x) h
-          simpa [NatModule.hmul_add] using h.symm
+          simpa [NatModule.nsmul_add] using h.symm
         · apply Quot.sound; simp
           refine ⟨n.natAbs * k, ?_⟩
           replace h := congrArg (fun x : α => n.natAbs * x) h
-          simpa [NatModule.hmul_add] using h)
+          simpa [NatModule.nsmul_add] using h)
 
 @[local simp] def sub (q₁ q₂ : Q α) : Q α :=
   Q.liftOn₂ q₁ q₂ (fun (a, b) (c, d) => Q.mk (a + d, c + b))
@@ -115,8 +115,8 @@ def Q.ind {β : Q α → Prop} (mk : ∀ (a : α × α), β (Q.mk a)) (q : Q α)
         exact ⟨k, h.symm⟩)
 
 attribute [local simp]
-  Quot.liftOn NatModule.add_zero NatModule.zero_add NatModule.one_hmul NatModule.zero_hmul NatModule.hmul_zero
-  NatModule.hmul_add NatModule.add_hmul
+  Quot.liftOn AddCommMonoid.add_zero AddCommMonoid.zero_add NatModule.one_nsmul NatModule.zero_nsmul NatModule.nsmul_zero
+  NatModule.nsmul_add NatModule.add_nsmul
 
 @[local simp] def zero : Q α :=
   Q.mk (0, 0)
@@ -150,18 +150,18 @@ theorem sub_eq_add_neg (a b : Q α) : sub a b = add a (neg b) := by
   next a b =>
   cases a; cases b; simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; ac_rfl
 
-theorem one_hmul (a : Q α) : hmulInt 1 a = a := by
+theorem one_zsmul (a : Q α) : zsmul 1 a = a := by
   induction a using Quot.ind
   next a => cases a; simp
 
-theorem zero_hmul (a : Q α) : hmulInt 0 a = zero := by
+theorem zero_zsmul (a : Q α) : zsmul 0 a = zero := by
   induction a using Quot.ind
   next a => cases a; simp
 
-theorem hmul_zero (a : Int) : hmulInt a (zero : Q α) = zero := by
+theorem zsmul_zero (a : Int) : zsmul a (zero : Q α) = zero := by
   simp
 
-theorem hmul_add (a : Int) (b c : Q α) : hmulInt a (add b c) = add (hmulInt a b) (hmulInt a c) := by
+theorem zsmul_add (a : Int) (b c : Q α) : zsmul a (add b c) = add (zsmul a b) (zsmul a c) := by
   induction b using Q.ind
   induction c using Q.ind
   next b c =>
@@ -172,7 +172,7 @@ theorem hmul_add (a : Int) (b c : Q α) : hmulInt a (add b c) = add (hmulInt a b
     simp
     ac_rfl
 
-theorem add_hmul (a b : Int) (c : Q α) : hmulInt (a + b) c = add (hmulInt a c) (hmulInt b c) := by
+theorem add_zsmul (a b : Int) (c : Q α) : zsmul (a + b) c = add (zsmul a c) (zsmul b c) := by
   induction c using Q.ind
   next c =>
   rcases c with ⟨c₁, c₂⟩; simp
@@ -183,7 +183,7 @@ theorem add_hmul (a b : Int) (c : Q α) : hmulInt (a + b) c = add (hmulInt a c)
       rw [if_pos (by omega)]
       apply Quot.sound
       refine ⟨0, ?_⟩
-      rw [Int.natAbs_add_of_nonpos (by omega) (by omega), NatModule.add_hmul, NatModule.add_hmul]
+      rw [Int.natAbs_add_of_nonpos (by omega) (by omega), NatModule.add_nsmul, NatModule.add_nsmul]
       ac_rfl
     · split
       · apply Quot.sound
@@ -213,23 +213,23 @@ theorem add_hmul (a b : Int) (c : Q α) : hmulInt (a + b) c = add (hmulInt a c)
       rw [if_neg (by omega)]
       apply Quot.sound
       refine ⟨0, ?_⟩
-      rw [Int.natAbs_add_of_nonneg (by omega) (by omega), NatModule.add_hmul, NatModule.add_hmul]
+      rw [Int.natAbs_add_of_nonneg (by omega) (by omega), NatModule.add_nsmul, NatModule.add_nsmul]
       ac_rfl
 
-theorem hmul_nat (n : Nat) (a : Q α) : hmulInt (n : Int) a = hmulNat n a := by
+theorem zsmul_natCast_eq_nsmul (n : Nat) (a : Q α) : zsmul (n : Int) a = nsmul n a := by
   induction a using Q.ind
   next a =>
   rcases a with ⟨a₁, a₂⟩; simp; omega
 
 def ofNatModule : IntModule (Q α) := {
-  hmulNat := ⟨hmulNat⟩,
-  hmulInt := ⟨hmulInt⟩,
+  nsmul := ⟨nsmul⟩,
+  zsmul := ⟨zsmul⟩,
   zero,
   add, sub, neg,
   add_comm, add_assoc, add_zero,
   neg_add_cancel, sub_eq_add_neg,
-  one_hmul, zero_hmul, hmul_zero, hmul_add, add_hmul,
-  hmul_nat
+  one_zsmul, zero_zsmul, zsmul_zero, zsmul_add, add_zsmul,
+  zsmul_natCast_eq_nsmul
 }
 
 attribute [instance] ofNatModule
@@ -257,7 +257,7 @@ private def rel (h : Equivalence (r α)) (q₁ q₂ : Q α) : Prop :=
 
 private theorem rel_rfl (h : Equivalence (r α)) (q : Q α) : rel h q q := by
   induction q using Quot.ind
-  simp [rel, NatModule.add_comm]
+  simp [rel, AddCommMonoid.add_comm]
 
 private theorem helper (h : Equivalence (r α)) (q₁ q₂ : Q α) : q₁ = q₂ → rel h q₁ q₂ := by
   intro h; subst q₁; apply rel_rfl h
@@ -287,7 +287,7 @@ instance [NatModule α] [AddRightCancel α] [NoNatZeroDivisors α] : NoNatZeroDi
     simp [r] at h₂
     rcases h₂ with ⟨k', h₂⟩
     replace h₂ := AddRightCancel.add_right_cancel _ _ _ h₂
-    simp [← NatModule.hmul_add] at h₂
+    simp [← NatModule.nsmul_add] at h₂
     replace h₂ := NoNatZeroDivisors.no_nat_zero_divisors k (a₁ + b₂) (a₂ + b₁) h₁ h₂
     apply Quot.sound; simp [r]; exists 0; simp [h₂]
 
@@ -318,7 +318,7 @@ instance [Preorder α] [OrderedAdd α] : Preorder (OfNatModule.Q α) where
     rcases a with ⟨a₁, a₂⟩
     change Q.mk _ ≤ Q.mk _
     simp only [mk_le_mk]
-    simp [NatModule.add_comm]; exact Preorder.le_refl (a₁ + a₂)
+    simp [AddCommMonoid.add_comm]; exact Preorder.le_refl (a₁ + a₂)
   le_trans {a b c} h₁ h₂ := by
     induction a using Q.ind
     induction b using Q.ind
@@ -337,12 +337,12 @@ attribute [-simp] Q.mk
 
 @[local simp] private theorem mk_lt_mk [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α}  :
     Q.mk (a₁, a₂) < Q.mk (b₁, b₂) ↔ a₁ + b₂ < a₂ + b₁ := by
-  simp [Preorder.lt_iff_le_not_le, NatModule.add_comm]
+  simp [Preorder.lt_iff_le_not_le, AddCommMonoid.add_comm]
 
 @[local simp] private theorem mk_pos [Preorder α] [OrderedAdd α] {a₁ a₂ : α} :
     0 < Q.mk (a₁, a₂) ↔ a₂ < a₁ := by
   change Q.mk (0,0) < _ ↔ _
-  simp [mk_lt_mk, NatModule.zero_add]
+  simp [mk_lt_mk, AddCommMonoid.zero_add]
 
 @[local simp]
 theorem toQ_le [Preorder α] [OrderedAdd α] {a b : α} : toQ a ≤ toQ b ↔ a ≤ b := by

src/Init/Grind/Ordered/Linarith.lean

@@ -20,9 +20,9 @@ Support for the linear arithmetic module for `IntModule` in `grind`
 
 namespace Lean.Grind.Linarith
 abbrev Var := Nat
-open IntModule
+open AddCommMonoid AddCommGroup NatModule IntModule
 
-attribute [local simp] add_zero zero_add zero_hmul nat_zero_hmul hmul_zero one_hmul
+attribute [local simp] add_zero zero_add zero_zsmul zero_nsmul zsmul_zero one_zsmul
 
 inductive Expr where
   | zero
@@ -75,10 +75,10 @@ where
 
 -- Helper instance for `ac_rfl`
 local instance {α} [IntModule α] : Std.Associative (· + · : α → α → α) where
-  assoc := IntModule.add_assoc
+  assoc := AddCommMonoid.add_assoc
 -- Helper instance for `ac_rfl`
 local instance {α} [IntModule α] : Std.Commutative (· + · : α → α → α) where
-  comm := IntModule.add_comm
+  comm := AddCommMonoid.add_comm
 
 theorem Poly.denote'_go_eq_denote {α} [IntModule α] (ctx : Context α) (p : Poly) (r : α) : denote'.go ctx r p = p.denote ctx + r := by
   induction r, p using denote'.go.induct ctx <;> simp [denote'.go, denote]
@@ -176,7 +176,7 @@ def Poly.mul (p : Poly) (k : Int) : Poly :=
   next => simp [*, denote]
   next =>
     induction p <;> simp [mul', denote, *]
-    rw [mul_hmul, hmul_add]
+    rw [mul_zsmul, zsmul_add]
 
 theorem Poly.denote_insert {α} [IntModule α] (ctx : Context α) (k : Int) (v : Var) (p : Poly) :
     (p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx := by
@@ -184,8 +184,8 @@ theorem Poly.denote_insert {α} [IntModule α] (ctx : Context α) (k : Int) (v :
   next => ac_rfl
   next h₁ h₂ h₃ =>
     simp at h₃; simp at h₂; subst h₂
-    rw [add_comm, ← add_assoc, ← add_hmul, h₃, zero_hmul, zero_add]
-  next h _ => simp at h; subst h; rw [add_hmul]; ac_rfl
+    rw [add_comm, ← add_assoc, ← add_zsmul, h₃, zero_zsmul, zero_add]
+  next h _ => simp at h; subst h; rw [add_zsmul]; ac_rfl
   next ih => rw [ih]; ac_rfl
 
 attribute [local simp] Poly.denote_insert
@@ -205,8 +205,8 @@ theorem Poly.denote_combine' {α} [IntModule α] (ctx : Context α) (fuel : Nat)
     simp_all +zetaDelta [denote]
   next h _ =>
     rw [Int.add_comm] at h
-    rw [add_left_comm, add_assoc, ← add_assoc, ← add_hmul, h, zero_hmul, zero_add]
-  next => rw [add_hmul]; ac_rfl
+    rw [add_left_comm, add_assoc, ← add_assoc, ← add_zsmul, h, zero_zsmul, zero_add]
+  next => rw [add_zsmul]; ac_rfl
   all_goals ac_rfl
 
 theorem Poly.denote_combine {α} [IntModule α] (ctx : Context α) (p₁ p₂ : Poly) : (p₁.combine p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
@@ -216,14 +216,14 @@ attribute [local simp] Poly.denote_combine
 
 theorem Expr.denote_toPoly'_go {α} [IntModule α] {k p} (ctx : Context α) (e : Expr)
     : (toPoly'.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
-  induction k, e using Expr.toPoly'.go.induct generalizing p <;> simp [toPoly'.go, denote, Poly.denote, *, hmul_add]
+  induction k, e using Expr.toPoly'.go.induct generalizing p <;> simp [toPoly'.go, denote, Poly.denote, *, zsmul_add]
   next => ac_rfl
-  next => rw [sub_eq_add_neg, neg_hmul, hmul_add, hmul_neg]; ac_rfl
+  next => rw [sub_eq_add_neg, neg_zsmul, zsmul_add, zsmul_neg]; ac_rfl
   next h => simp at h; subst h; simp
-  next ih => simp at ih; rw [ih, mul_hmul, IntModule.hmul_nat]
+  next ih => simp at ih; rw [ih, mul_zsmul, zsmul_natCast_eq_nsmul]
   next ih => simp at ih; simp [ih]
-  next ih => simp at ih; rw [ih, mul_hmul]
-  next => rw [hmul_neg, neg_hmul]
+  next ih => simp at ih; rw [ih, mul_zsmul]
+  next => rw [zsmul_neg, neg_zsmul]
 
 theorem Expr.denote_norm {α} [IntModule α] (ctx : Context α) (e : Expr) : e.norm.denote ctx = e.denote ctx := by
   simp [norm, toPoly', Expr.denote_toPoly'_go, Poly.denote]
@@ -280,8 +280,8 @@ def le_le_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
 theorem le_le_combine {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
     : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
   simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp
-  replace h₁ := hmul_int_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
-  replace h₂ := hmul_int_nonpos (coe_natAbs_nonneg p₁.leadCoeff) h₂
+  replace h₁ := zsmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
+  replace h₂ := zsmul_nonpos (coe_natAbs_nonneg p₁.leadCoeff) h₂
   exact le_add_le h₁ h₂
 
 def le_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
@@ -292,8 +292,8 @@ def le_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
 theorem le_lt_combine {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
     : le_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
   simp [-Int.natAbs_pos, -Int.ofNat_pos, le_lt_combine_cert]; intro hp _ h₁ h₂; subst p₃; simp
-  replace h₁ := hmul_int_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
-  replace h₂ := hmul_int_neg_iff (↑p₁.leadCoeff.natAbs) h₂ |>.mpr hp
+  replace h₁ := zsmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
+  replace h₂ := zsmul_neg_iff (↑p₁.leadCoeff.natAbs) h₂ |>.mpr hp
   exact le_add_lt h₁ h₂
 
 def lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
@@ -304,8 +304,8 @@ def lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
 theorem lt_lt_combine {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
     : lt_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx < 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
   simp [-Int.natAbs_pos, -Int.ofNat_pos, lt_lt_combine_cert]; intro hp₁ hp₂ _ h₁ h₂; subst p₃; simp
-  replace h₁ := hmul_int_neg_iff (↑p₂.leadCoeff.natAbs) h₁ |>.mpr hp₁
-  replace h₂ := hmul_int_neg_iff (↑p₁.leadCoeff.natAbs) h₂ |>.mpr hp₂
+  replace h₁ := zsmul_neg_iff (↑p₂.leadCoeff.natAbs) h₁ |>.mpr hp₁
+  replace h₂ := zsmul_neg_iff (↑p₁.leadCoeff.natAbs) h₂ |>.mpr hp₂
   exact lt_add_lt h₁ h₂
 
 def diseq_split_cert (p₁ p₂ : Poly) : Bool :=
@@ -320,7 +320,7 @@ theorem diseq_split {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx :
   next h =>
     apply Or.inr
     simp [h₁] at h
-    rw [← neg_pos_iff, neg_hmul, neg_neg, one_hmul]; assumption
+    rw [← neg_pos_iff, neg_zsmul, neg_neg, one_zsmul]; assumption
 
 theorem diseq_split_resolve {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly)
     : diseq_split_cert p₁ p₂ → p₁.denote' ctx ≠ 0 → ¬p₁.denote' ctx < 0 → p₂.denote' ctx < 0 := by
@@ -409,7 +409,7 @@ theorem eq_of_le_ge {α} [IntModule α] [PartialOrder α] [OrderedAdd α] (ctx :
   intro; subst p₂; simp
   intro h₁ h₂
   replace h₂ := add_le_left h₂ (p₁.denote ctx)
-  rw [add_comm, neg_hmul, one_hmul, ← sub_eq_add_neg, sub_self, zero_add] at h₂
+  rw [add_comm, neg_zsmul, one_zsmul, ← sub_eq_add_neg, sub_self, zero_add] at h₂
   exact PartialOrder.le_antisymm h₁ h₂
 
 /-!
@@ -429,7 +429,7 @@ def zero_lt_one_cert (p : Poly) : Bool :=
 
 theorem zero_lt_one {α} [Ring α] [Preorder α] [OrderedRing α] (ctx : Context α) (p : Poly)
     : zero_lt_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx < 0 := by
-  simp [zero_lt_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one, neg_hmul]
+  simp [zero_lt_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one, neg_zsmul]
   rw [neg_lt_iff, neg_zero]; apply OrderedRing.zero_lt_one
 
 def zero_ne_one_cert (p : Poly) : Bool :=
@@ -478,7 +478,7 @@ def eq_coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
 
 theorem eq_coeff {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
     : eq_coeff_cert p₁ p₂ k → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 := by
-  simp [eq_coeff_cert]; intro h _; subst p₁; simp [*, hmul_nat]
+  simp [eq_coeff_cert]; intro h _; subst p₁; simp [*, zsmul_natCast_eq_nsmul]
   exact NoNatZeroDivisors.eq_zero_of_mul_eq_zero h
 
 def coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
@@ -490,7 +490,7 @@ theorem le_coeff {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Con
   have : ↑k > (0 : Int) := Int.natCast_pos.mpr h
   intro h₁; apply Classical.byContradiction
   intro h₂; replace h₂ := LinearOrder.lt_of_not_le h₂
-  replace h₂ := hmul_int_pos_iff (↑k) h₂ |>.mpr this
+  replace h₂ := zsmul_pos_iff (↑k) h₂ |>.mpr this
   exact Preorder.lt_irrefl 0 (Preorder.lt_of_lt_of_le h₂ h₁)
 
 theorem lt_coeff {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
@@ -499,11 +499,11 @@ theorem lt_coeff {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Con
   have : ↑k > (0 : Int) := Int.natCast_pos.mpr h
   intro h₁; apply Classical.byContradiction
   intro h₂; replace h₂ := LinearOrder.le_of_not_lt h₂
-  replace h₂ := hmul_int_nonneg (Int.le_of_lt this) h₂
+  replace h₂ := zsmul_nonneg (Int.le_of_lt this) h₂
   exact Preorder.lt_irrefl 0 (Preorder.lt_of_le_of_lt h₂ h₁)
 
 theorem diseq_neg {α} [IntModule α] (ctx : Context α) (p p' : Poly) : p' == p.mul (-1) → p.denote' ctx ≠ 0 → p'.denote' ctx ≠ 0 := by
-  simp; intro _ _; subst p'; simp [neg_hmul]
+  simp; intro _ _; subst p'; simp [neg_zsmul]
   intro h; replace h := congrArg (- ·) h; simp [neg_neg, neg_zero] at h
   contradiction
 
@@ -522,8 +522,8 @@ theorem eq_diseq_subst {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context
     have : (k₁.natAbs : Int) * Poly.denote ctx p₂ = 0 := by
       cases Int.natAbs_eq_iff.mp (Eq.refl k₁.natAbs)
       next h => rw [← h]; assumption
-      next h => replace h := congrArg (- ·) h; simp at h; rw [← h, IntModule.neg_hmul, h₃, IntModule.neg_zero]
-    simpa [hmul_nat] using this
+      next h => replace h := congrArg (- ·) h; simp at h; rw [← h, neg_zsmul, h₃, neg_zero]
+    simpa [zsmul_natCast_eq_nsmul] using this
   have := NoNatZeroDivisors.eq_zero_of_mul_eq_zero hne this
   contradiction
 
@@ -547,7 +547,7 @@ def eq_le_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
 theorem eq_le_subst {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly)
     : eq_le_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
   simp [eq_le_subst_cert]; intro h _ h₁ h₂; subst p₃; simp [h₁]
-  exact hmul_int_nonpos h h₂
+  exact zsmul_nonpos h h₂
 
 def eq_lt_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
   let a := p₁.coeff x
@@ -557,7 +557,7 @@ def eq_lt_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
 theorem eq_lt_subst {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly)
     : eq_lt_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
   simp [eq_lt_subst_cert]; intro h _ h₁ h₂; subst p₃; simp [h₁]
-  exact hmul_int_neg_iff (p₁.coeff x) h₂ |>.mpr h
+  exact zsmul_neg_iff (p₁.coeff x) h₂ |>.mpr h
 
 def eq_eq_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
   let a := p₁.coeff x

src/Init/Grind/Ordered/Module.lean

@@ -26,22 +26,15 @@ class ExistsAddOfLT (α : Type u) [LT α] [Zero α] [Add α] where
 
 namespace OrderedAdd
 
-open NatModule
+open AddCommMonoid NatModule
 
 section
 
-variable {M : Type u} [Preorder M] [NatModule M] [OrderedAdd M]
+variable {M : Type u} [Preorder M] [AddCommMonoid M] [OrderedAdd M]
 
 theorem add_le_right_iff {a b : M} (c : M) : a ≤ b ↔ c + a ≤ c + b := by
   rw [add_comm c a, add_comm c b, add_le_left_iff]
 
-theorem hmul_le_hmul {k : Nat} {a b : M} (h : a ≤ b) : k * a ≤ k * b := by
-  induction k with
-  | zero => simp [zero_hmul, Preorder.le_refl]
-  | succ k ih =>
-    rw [add_hmul, one_hmul, add_hmul, one_hmul]
-    exact Preorder.le_trans ((add_le_left_iff a).mp ih) ((add_le_right_iff (k * b)).mp h)
-
 theorem add_le_left {a b : M} (h : a ≤ b) (c : M) : a + c ≤ b + c :=
   (add_le_left_iff c).mp h
 
@@ -73,36 +66,6 @@ theorem add_lt_left_iff {a b : M} (c : M) : a < b ↔ a + c < b + c := by
 theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by
   rw [add_comm c a, add_comm c b, add_lt_left_iff]
 
-theorem hmul_lt_hmul_iff (k : Nat) {a b : M} (h : a < b) : k * a < k * b ↔ 0 < k := by
-  induction k with
-  | zero => simp [zero_hmul, Preorder.lt_irrefl]
-  | succ k ih =>
-    rw [add_hmul, one_hmul, add_hmul, one_hmul]
-    simp only [Nat.zero_lt_succ, iff_true]
-    by_cases hk : 0 < k
-    · simp only [hk, iff_true] at ih
-      exact Preorder.lt_trans ((add_lt_left_iff a).mp ih) ((add_lt_right_iff (k * b)).mp h)
-    · simp [Nat.eq_zero_of_not_pos hk, zero_hmul, zero_add, h]
-
-theorem hmul_pos_iff {k : Nat} {a : M} (h : 0 < a) : 0 < k * a ↔ 0 < k:= by
-  rw [← hmul_lt_hmul_iff k h, hmul_zero]
-
-theorem hmul_nonneg {k : Nat} {a : M} (h : 0 ≤ a) : 0 ≤ k * a := by
-  have := hmul_le_hmul (k := k) h
-  rwa [hmul_zero] at this
-
-theorem hmul_le_hmul_of_le_of_le_of_nonneg
-    {k₁ k₂ : Nat} {x y : M} (hk : k₁ ≤ k₂) (h : x ≤ y) (w : 0 ≤ x) :
-    k₁ * x ≤ k₂ * y := by
-  apply Preorder.le_trans
-  · change k₁ * x ≤ k₂ * x
-    obtain ⟨k', rfl⟩ := Nat.exists_eq_add_of_le hk
-    rw [add_hmul]
-    conv => lhs; rw [← add_zero (k₁ * x)]
-    rw [← add_le_right_iff]
-    exact hmul_nonneg w
-  · exact hmul_le_hmul h
-
 theorem add_le_add {a b c d : M} (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b + d :=
   Preorder.le_trans (add_le_right a hcd) (add_le_left hab d)
 
@@ -110,44 +73,90 @@ end
 
 section
 
-variable {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M]
+variable {M : Type u} [Preorder M] [NatModule M] [OrderedAdd M]
+
+theorem nsmul_le_nsmul {k : Nat} {a b : M} (h : a ≤ b) : k * a ≤ k * b := by
+  induction k with
+  | zero => simp [zero_nsmul, Preorder.le_refl]
+  | succ k ih =>
+    rw [add_nsmul, one_nsmul, add_nsmul, one_nsmul]
+    exact Preorder.le_trans ((add_le_left_iff a).mp ih) ((add_le_right_iff (k * b)).mp h)
+
+theorem nsmul_lt_nsmul_iff (k : Nat) {a b : M} (h : a < b) : k * a < k * b ↔ 0 < k := by
+  induction k with
+  | zero => simp [zero_nsmul, Preorder.lt_irrefl]
+  | succ k ih =>
+    rw [add_nsmul, one_nsmul, add_nsmul, one_nsmul]
+    simp only [Nat.zero_lt_succ, iff_true]
+    by_cases hk : 0 < k
+    · simp only [hk, iff_true] at ih
+      exact Preorder.lt_trans ((add_lt_left_iff a).mp ih) ((add_lt_right_iff (k * b)).mp h)
+    · simp [Nat.eq_zero_of_not_pos hk, zero_nsmul, zero_add, h]
+
+theorem nsmul_pos_iff {k : Nat} {a : M} (h : 0 < a) : 0 < k * a ↔ 0 < k:= by
+  rw [← nsmul_lt_nsmul_iff k h, nsmul_zero]
+
+theorem nsmul_nonneg {k : Nat} {a : M} (h : 0 ≤ a) : 0 ≤ k * a := by
+  have := nsmul_le_nsmul (k := k) h
+  rwa [nsmul_zero] at this
+
+theorem nsmul_le_nsmul_of_le_of_le_of_nonneg
+    {k₁ k₂ : Nat} {x y : M} (hk : k₁ ≤ k₂) (h : x ≤ y) (w : 0 ≤ x) :
+    k₁ * x ≤ k₂ * y := by
+  apply Preorder.le_trans
+  · change k₁ * x ≤ k₂ * x
+    obtain ⟨k', rfl⟩ := Nat.exists_eq_add_of_le hk
+    rw [add_nsmul]
+    conv => lhs; rw [← add_zero (k₁ * x)]
+    rw [← add_le_right_iff]
+    exact nsmul_nonneg w
+  · exact nsmul_le_nsmul h
+
+end
+
+section
+
+open AddCommGroup
+variable {M : Type u} [Preorder M] [AddCommGroup M] [OrderedAdd M]
 
 theorem neg_le_iff {a b : M} : -a ≤ b ↔ -b ≤ a := by
-  rw [OrderedAdd.add_le_left_iff a, IntModule.neg_add_cancel]
-  conv => rhs; rw [OrderedAdd.add_le_left_iff b, IntModule.neg_add_cancel]
+  rw [OrderedAdd.add_le_left_iff a, neg_add_cancel]
+  conv => rhs; rw [OrderedAdd.add_le_left_iff b, neg_add_cancel]
   rw [add_comm]
 
 end
 section
 
 variable {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M]
+open AddCommGroup IntModule
 
-theorem hmul_int_pos_iff (k : Int) {x : M} (h : 0 < x) : 0 < k * x ↔ 0 < k :=
+theorem zsmul_pos_iff (k : Int) {x : M} (h : 0 < x) : 0 < k * x ↔ 0 < k :=
   match k with
   | (k + 1 : Nat) => by
-    simpa [IntModule.hmul_zero, ← IntModule.hmul_nat] using hmul_lt_hmul_iff (k := k + 1) h
-  | (0 : Nat) => by simp [IntModule.zero_hmul]; exact Preorder.lt_irrefl 0
+    simpa [zsmul_zero, ← zsmul_natCast_eq_nsmul] using nsmul_lt_nsmul_iff (k := k + 1) h
+  | (0 : Nat) => by simp [zero_zsmul]; exact Preorder.lt_irrefl 0
   | -(k + 1 : Nat) => by
     have : ¬ (k : Int) + 1 < 0 := by omega
     simp [this]; clear this
-    rw [IntModule.neg_hmul]
+    rw [neg_zsmul]
     rw [Preorder.lt_iff_le_not_le]
     simp
     intro h'
-    rw [OrderedAdd.neg_le_iff, IntModule.neg_zero]
-    simpa [IntModule.hmul_zero, ← IntModule.hmul_nat] using
-      hmul_le_hmul (k := k + 1) (Preorder.le_of_lt h)
+    rw [OrderedAdd.neg_le_iff, neg_zero]
+    simpa [zsmul_zero, ← zsmul_natCast_eq_nsmul] using
+      nsmul_le_nsmul (k := k + 1) (Preorder.le_of_lt h)
 
-theorem hmul_int_nonneg {k : Int} {x : M} (h : 0 ≤ k) (hx : 0 ≤ x) : 0 ≤ k * x :=
+theorem zsmul_nonneg {k : Int} {x : M} (h : 0 ≤ k) (hx : 0 ≤ x) : 0 ≤ k * x :=
   match k, h with
   | (k : Nat), _ => by
-    simpa [IntModule.hmul_nat] using OrderedAdd.hmul_nonneg hx
+    simpa [zsmul_natCast_eq_nsmul] using nsmul_nonneg hx
 
 end
 
-variable {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M]
+section
+variable {M : Type u} [Preorder M] [AddCommGroup M] [OrderedAdd M]
 
-open IntModule
+open AddCommGroup
 
 theorem le_neg_iff {a b : M} : a ≤ -b ↔ b ≤ -a := by
   conv => lhs; rw [← neg_neg a]
@@ -168,31 +177,40 @@ theorem neg_pos_iff {a : M} : 0 < -a ↔ a < 0 := by
   rw [lt_neg_iff, neg_zero]
 
 theorem sub_nonneg_iff {a b : M} : 0 ≤ a - b ↔ b ≤ a := by
-  rw [add_le_left_iff b, IntModule.zero_add, sub_add_cancel]
+  rw [add_le_left_iff b, zero_add, sub_add_cancel]
 
 theorem sub_pos_iff {a b : M} : 0 < a - b ↔ b < a := by
-  rw [add_lt_left_iff b, IntModule.zero_add, sub_add_cancel]
+  rw [add_lt_left_iff b, zero_add, sub_add_cancel]
 
-theorem hmul_int_neg_iff (k : Int) {a : M} (h : a < 0) : k * a < 0 ↔ 0 < k := by
-  simpa [IntModule.hmul_neg, neg_pos_iff] using hmul_int_pos_iff k (neg_pos_iff.mpr h)
+end
 
-theorem hmul_int_nonpos {k : Int} {a : M} (hk : 0 ≤ k) (ha : a ≤ 0) : k * a ≤ 0 := by
-  simpa [IntModule.hmul_neg, neg_nonneg_iff] using hmul_int_nonneg hk (neg_nonneg_iff.mpr ha)
+section
 
-theorem hmul_int_le_hmul_int {a b : M} {k : Int} (hk : 0 ≤ k) (h : a ≤ b) : k * a ≤ k * b := by
-  simpa [hmul_sub, sub_nonneg_iff] using hmul_int_nonneg hk (sub_nonneg_iff.mpr h)
+variable {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M]
+open IntModule
 
-theorem hmul_int_lt_hmul_int_iff (k : Int) {a b : M} (h : a < b) : k * a < k * b ↔ 0 < k := by
-  simpa [hmul_sub, sub_pos_iff] using hmul_int_pos_iff k (sub_pos_iff.mpr h)
+theorem zsmul_neg_iff (k : Int) {a : M} (h : a < 0) : k * a < 0 ↔ 0 < k := by
+  simpa [IntModule.zsmul_neg, neg_pos_iff] using zsmul_pos_iff k (neg_pos_iff.mpr h)
 
-theorem hmul_int_le_hmul_int_of_le_of_le_of_nonneg_of_nonneg
+theorem zsmul_nonpos {k : Int} {a : M} (hk : 0 ≤ k) (ha : a ≤ 0) : k * a ≤ 0 := by
+  simpa [IntModule.zsmul_neg, neg_nonneg_iff] using zsmul_nonneg hk (neg_nonneg_iff.mpr ha)
+
+theorem zsmul_le_zsmul {a b : M} {k : Int} (hk : 0 ≤ k) (h : a ≤ b) : k * a ≤ k * b := by
+  simpa [zsmul_sub, sub_nonneg_iff] using zsmul_nonneg hk (sub_nonneg_iff.mpr h)
+
+theorem zsmul_lt_zsmul_iff (k : Int) {a b : M} (h : a < b) : k * a < k * b ↔ 0 < k := by
+  simpa [zsmul_sub, sub_pos_iff] using zsmul_pos_iff k (sub_pos_iff.mpr h)
+
+theorem zsmul_le_zsmul_of_le_of_le_of_nonneg_of_nonneg
     {k₁ k₂ : Int} {x y : M} (hk : k₁ ≤ k₂) (h : x ≤ y) (w : 0 ≤ k₁) (w' : 0 ≤ x) :
     k₁ * x ≤ k₂ * y := by
   apply Preorder.le_trans
-  · have : 0 ≤ k₁ * (y - x) := hmul_int_nonneg w (sub_nonneg_iff.mpr h)
-    rwa [IntModule.hmul_sub, sub_nonneg_iff] at this
-  · have : 0 ≤ (k₂ - k₁) * y := hmul_int_nonneg (Int.sub_nonneg.mpr hk) (Preorder.le_trans w' h)
-    rwa [IntModule.sub_hmul, sub_nonneg_iff] at this
+  · have : 0 ≤ k₁ * (y - x) := zsmul_nonneg w (sub_nonneg_iff.mpr h)
+    rwa [IntModule.zsmul_sub, sub_nonneg_iff] at this
+  · have : 0 ≤ (k₂ - k₁) * y := zsmul_nonneg (Int.sub_nonneg.mpr hk) (Preorder.le_trans w' h)
+    rwa [IntModule.sub_zsmul, sub_nonneg_iff] at this
+
+end
 
 end OrderedAdd
 

src/Init/Grind/Ordered/Ring.lean

@@ -38,7 +38,7 @@ variable [Preorder R] [OrderedRing R]
 theorem neg_one_lt_zero : (-1 : R) < 0 := by
   have h := zero_lt_one (R := R)
   have := OrderedAdd.add_lt_left h (-1)
-  rw [Semiring.zero_add, Ring.add_neg_cancel] at this
+  rw [AddCommMonoid.zero_add, AddCommGroup.add_neg_cancel] at this
   assumption
 
 theorem ofNat_nonneg (x : Nat) : (OfNat.ofNat x : R) ≥ 0 := by
@@ -48,7 +48,7 @@ theorem ofNat_nonneg (x : Nat) : (OfNat.ofNat x : R) ≥ 0 := by
     have := OrderedRing.zero_lt_one (R := R)
     rw [Semiring.ofNat_succ]
     replace ih := OrderedAdd.add_le_left ih 1
-    rw [Semiring.zero_add] at ih
+    rw [AddCommMonoid.zero_add] at ih
     have := Preorder.lt_of_lt_of_le this ih
     exact Preorder.le_of_lt this
 
@@ -62,8 +62,8 @@ instance [Ring α] [Preorder α] [OrderedRing α] : IsCharP α 0 := IsCharP.mk'
     next x =>
       rw [Semiring.ofNat_succ] at h
       replace h := congrArg (· - 1) h; simp at h
-      rw [Ring.sub_eq_add_neg, Semiring.add_assoc, Ring.add_neg_cancel,
-          Ring.sub_eq_add_neg, Semiring.zero_add, Semiring.add_zero] at h
+      rw [Ring.sub_eq_add_neg, Semiring.add_assoc, AddCommGroup.add_neg_cancel,
+          Ring.sub_eq_add_neg, AddCommMonoid.zero_add, Semiring.add_zero] at h
       have h₁ : (OfNat.ofNat x : α) < 0 := by
         have := OrderedRing.neg_one_lt_zero (R := α)
         rw [h]; assumption
@@ -110,26 +110,26 @@ open OrderedAdd
 
 theorem mul_le_mul_of_nonpos_left {a b c : R} (h : a ≤ b) (h' : c ≤ 0) : c * b ≤ c * a := by
   have := mul_le_mul_of_nonneg_left h (neg_nonneg_iff.mpr h')
-  rwa [Ring.neg_mul, Ring.neg_mul, neg_le_iff, IntModule.neg_neg] at this
+  rwa [Ring.neg_mul, Ring.neg_mul, neg_le_iff, AddCommGroup.neg_neg] at this
 
 theorem mul_le_mul_of_nonpos_right {a b c : R} (h : a ≤ b) (h' : c ≤ 0) : b * c ≤ a * c := by
   have := mul_le_mul_of_nonneg_right h (neg_nonneg_iff.mpr h')
-  rwa [Ring.mul_neg, Ring.mul_neg, neg_le_iff, IntModule.neg_neg] at this
+  rwa [Ring.mul_neg, Ring.mul_neg, neg_le_iff, AddCommGroup.neg_neg] at this
 
 theorem mul_lt_mul_of_neg_left {a b c : R} (h : a < b) (h' : c < 0) : c * b < c * a := by
   have := mul_lt_mul_of_pos_left h (neg_pos_iff.mpr h')
-  rwa [Ring.neg_mul, Ring.neg_mul, neg_lt_iff, IntModule.neg_neg] at this
+  rwa [Ring.neg_mul, Ring.neg_mul, neg_lt_iff, AddCommGroup.neg_neg] at this
 
 theorem mul_lt_mul_of_neg_right {a b c : R} (h : a < b) (h' : c < 0) : b * c < a * c := by
   have := mul_lt_mul_of_pos_right h (neg_pos_iff.mpr h')
-  rwa [Ring.mul_neg, Ring.mul_neg, neg_lt_iff, IntModule.neg_neg] at this
+  rwa [Ring.mul_neg, Ring.mul_neg, neg_lt_iff, AddCommGroup.neg_neg] at this
 
 theorem mul_nonneg {a b : R} (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) : 0 ≤ a * b := by
   simpa [Semiring.zero_mul] using mul_le_mul_of_nonneg_right h₁ h₂
 
 theorem mul_nonneg_of_nonpos_of_nonpos {a b : R} (h₁ : a ≤ 0) (h₂ : b ≤ 0) : 0 ≤ a * b := by
   have := mul_nonneg (neg_nonneg_iff.mpr h₁) (neg_nonneg_iff.mpr h₂)
-  simpa [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg] using this
+  simpa [Ring.neg_mul, Ring.mul_neg, AddCommGroup.neg_neg] using this
 
 theorem mul_nonpos_of_nonneg_of_nonpos {a b : R} (h₁ : 0 ≤ a) (h₂ : b ≤ 0) : a * b ≤ 0 := by
   rw [← neg_nonneg_iff, ← Ring.mul_neg]
@@ -144,7 +144,7 @@ theorem mul_pos {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by
 
 theorem mul_pos_of_neg_of_neg {a b : R} (h₁ : a < 0) (h₂ : b < 0) : 0 < a * b := by
   have := mul_pos (neg_pos_iff.mpr h₁) (neg_pos_iff.mpr h₂)
-  simpa [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg] using this
+  simpa [Ring.neg_mul, Ring.mul_neg, AddCommGroup.neg_neg] using this
 
 theorem mul_neg_of_pos_of_neg {a b : R} (h₁ : 0 < a) (h₂ : b < 0) : a * b < 0 := by
   rw [← neg_pos_iff, ← Ring.mul_neg]

src/Init/Grind/Ring/Basic.lean

@@ -15,7 +15,7 @@ public import Init.Grind.Module.Basic
 public section
 
 /-!
-# A monolithic commutative ring typeclass for internal use in `grind`.
+# Commutative ring typeclasses for internal use in `grind`.
 
 The `Lean.Grind.CommRing` class will be used to convert expressions into the internal representation via polynomials,
 with coefficients expressed via `OfNat` and `Neg`.
@@ -52,12 +52,14 @@ class Semiring (α : Type u) extends Add α, Mul α, HPow α Nat α where
   The field `ofNat_eq_natCast` ensures that these are (propositionally) equal to the values of `natCast`.
   -/
   [ofNat : ∀ n, OfNat α n]
-  /-- Addition is associative. -/
-  add_assoc : ∀ a b c : α, a + b + c = a + (b + c)
-  /-- Addition is commutative. -/
-  add_comm : ∀ a b : α, a + b = b + a
+  /-- Scalar multiplication by natural numbers. -/
+  [nsmul : HMul Nat α α]
   /-- Zero is the right identity for addition. -/
   add_zero : ∀ a : α, a + 0 = a
+  /-- Addition is commutative. -/
+  add_comm : ∀ a b : α, a + b = b + a
+  /-- Addition is associative. -/
+  add_assoc : ∀ a b c : α, a + b + c = a + (b + c)
   /-- Multiplication is associative. -/
   mul_assoc : ∀ a b c : α, a * b * c = a * (b * c)
   /-- One is the right identity for multiplication. -/
@@ -80,6 +82,7 @@ class Semiring (α : Type u) extends Add α, Mul α, HPow α Nat α where
   ofNat_succ : ∀ a : Nat, OfNat.ofNat (α := α) (a + 1) = OfNat.ofNat a + 1 := by intros; rfl
   /-- Numerals are consistently defined with respect to the canonical map from natural numbers. -/
   ofNat_eq_natCast : ∀ n : Nat, OfNat.ofNat (α := α) n = Nat.cast n := by intros; rfl
+  nsmul_eq_natCast_mul : ∀ n : Nat, ∀ a : α, HMul.hMul (α := Nat) n a = Nat.cast n * a := by intros; rfl
 
 /--
 A ring, i.e. a type equipped with addition, negation, multiplication, and a map from the integers,
@@ -90,10 +93,16 @@ Use `CommRing` if the multiplication is commutative.
 class Ring (α : Type u) extends Semiring α, Neg α, Sub α where
   /-- In every ring there is a canonical map from the integers to the ring. -/
   [intCast : IntCast α]
+  /-- Scalar multiplication by integers. -/
+  [zsmul : HMul Int α α]
   /-- Negation is the left inverse of addition. -/
   neg_add_cancel : ∀ a : α, -a + a = 0
   /-- Subtraction is addition of the negative. -/
   sub_eq_add_neg : ∀ a b : α, a - b = a + -b
+  /-- Scalar multiplication by the negation of an integer is the negation of scalar multiplication by that integer. -/
+  neg_zsmul : ∀ (i : Int) (a : α), HMul.hMul (α := Int) (-i : Int) a = -(HMul.hMul (α := Int) i a)
+  /-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers. -/
+  zsmul_natCast_eq_nsmul : ∀ n : Nat, ∀ a : α, HMul.hMul (α := Int) (n : Int) a = HMul.hMul (α := Nat) n a := by intros; rfl
   /-- The canonical map from the integers is consistent with the canonical map from the natural numbers. -/
   intCast_ofNat : ∀ n : Nat, Int.cast (OfNat.ofNat (α := Int) n) = OfNat.ofNat (α := α) n := by intros; rfl
   /-- The canonical map from the integers is consistent with negation. -/
@@ -132,27 +141,32 @@ example [CommRing α] : (CommSemiring.toSemiring : Semiring α) = (Ring.toSemiri
 
 namespace Semiring
 
+open NatModule
+
 variable {α : Type u} [Semiring α]
 
-theorem natCast_zero : ((0 : Nat) : α) = 0 := (ofNat_eq_natCast 0).symm
+theorem natCast_zero : ((0 : Nat) : α) = 0 := by
+  rw [← ofNat_eq_natCast 0]
 theorem natCast_one : ((1 : Nat) : α) = 1 := (ofNat_eq_natCast 1).symm
 
 theorem ofNat_add (a b : Nat) : OfNat.ofNat (α := α) (a + b) = OfNat.ofNat a + OfNat.ofNat b := by
   induction b with
-  | zero => simp [Nat.add_zero, add_zero]
+  | zero => rw [Nat.add_zero, add_zero]
   | succ b ih => rw [Nat.add_succ, ofNat_succ, ih, ofNat_succ b, add_assoc]
 
+instance toNatModule [I : Semiring α] : NatModule α :=
+  { I with
+    zero_nsmul a := by rw [nsmul_eq_natCast_mul, ← ofNat_eq_natCast, zero_mul]
+    one_nsmul a := by rw [nsmul_eq_natCast_mul, ← ofNat_eq_natCast, one_mul]
+    add_nsmul n m a := by rw [nsmul_eq_natCast_mul, ← ofNat_eq_natCast, ofNat_add, right_distrib, ofNat_eq_natCast, ofNat_eq_natCast, ← nsmul_eq_natCast_mul, ← nsmul_eq_natCast_mul]
+    nsmul_zero n := by rw [nsmul_eq_natCast_mul, mul_zero]
+    nsmul_add n a b := by rw [nsmul_eq_natCast_mul, ← ofNat_eq_natCast, left_distrib, ofNat_eq_natCast, ← nsmul_eq_natCast_mul, ← nsmul_eq_natCast_mul] }
+
 theorem natCast_add (a b : Nat) : ((a + b : Nat) : α) = ((a : α) + (b : α)) := by
   rw [← ofNat_eq_natCast, ← ofNat_eq_natCast, ofNat_add, ofNat_eq_natCast, ofNat_eq_natCast]
 theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : α) = ((n : α) + 1) := by
   rw [natCast_add, natCast_one]
 
-theorem zero_add (a : α) : 0 + a = a := by
-  rw [add_comm, add_zero]
-
-theorem add_left_comm (a b c : α) : a + (b + c) = b + (a + c) := by
-  rw [← add_assoc, ← add_assoc, add_comm a]
-
 theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a * OfNat.ofNat b := by
   induction b with
   | zero => simp [Nat.mul_zero, mul_zero]
@@ -177,84 +191,29 @@ theorem natCast_pow (x : Nat) (k : Nat) : ((x ^ k : Nat) : α) = (x : α) ^ k :=
   next => simp [pow_zero, Nat.pow_zero, natCast_one]
   next k ih => simp [pow_succ, Nat.pow_succ, natCast_mul, *]
 
-instance : NatModule α where
-  hMul a x := a * x
-  add_zero := by simp [add_zero]
-  add_assoc := by simp [add_assoc]
-  add_comm := by simp [add_comm]
-  zero_hmul := by simp [natCast_zero, zero_mul]
-  one_hmul := by simp [natCast_one, one_mul]
-  add_hmul := by simp [natCast_add, right_distrib]
-  hmul_zero := by simp [mul_zero]
-  hmul_add := by simp [left_distrib]
-
-theorem hmul_eq_natCast_mul {α} [Semiring α] {k : Nat} {a : α} : HMul.hMul (α := Nat) k a = (k : α) * a := rfl
-
-theorem hmul_eq_ofNat_mul {α} [Semiring α] {k : Nat} {a : α} : HMul.hMul (α := Nat) k a = OfNat.ofNat k * a := by
-  simp [ofNat_eq_natCast, hmul_eq_natCast_mul]
+theorem nsmul_eq_ofNat_mul {α} [Semiring α] {k : Nat} {a : α} : HMul.hMul (α := Nat) k a = OfNat.ofNat k * a := by
+  simp [ofNat_eq_natCast, nsmul_eq_natCast_mul]
 
 end Semiring
 
 namespace Ring
 
-open Semiring
+open AddCommMonoid AddCommGroup NatModule IntModule
+open Semiring hiding add_assoc add_comm
 
 variable {α : Type u} [Ring α]
 
-theorem add_neg_cancel (a : α) : a + -a = 0 := by
-  rw [add_comm, neg_add_cancel]
-
-theorem add_left_inj {a b : α} (c : α) : a + c = b + c ↔ a = b :=
-  ⟨fun h => by simpa [add_assoc, add_neg_cancel, add_zero] using (congrArg (· + -c) h),
-   fun g => congrArg (· + c) g⟩
-
-theorem add_right_inj (a b c : α) : a + b = a + c ↔ b = c := by
-  rw [add_comm a b, add_comm a c, add_left_inj]
-
-theorem neg_zero : (-0 : α) = 0 := by
-  rw [← add_left_inj 0, neg_add_cancel, add_zero]
-
-theorem neg_neg (a : α) : -(-a) = a := by
-  rw [← add_left_inj (-a), neg_add_cancel, add_neg_cancel]
-
-theorem neg_eq_zero (a : α) : -a = 0 ↔ a = 0 :=
-  ⟨fun h => by
-    replace h := congrArg (-·) h
-    simpa [neg_neg, neg_zero] using h,
-   fun h => by rw [h, neg_zero]⟩
-
-theorem neg_eq_iff (a b : α) : -a = b ↔ a = -b := by
-  constructor
-  · intro h
-    rw [← neg_neg a, h]
-  · intro h
-    rw [← neg_neg b, h]
-
-theorem neg_add (a b : α) : -(a + b) = -a + -b := by
-  rw [← add_left_inj (a + b), neg_add_cancel, add_assoc (-a), add_comm a b, ← add_assoc (-b),
-    neg_add_cancel, zero_add, neg_add_cancel]
-
-theorem neg_sub (a b : α) : -(a - b) = b - a := by
-  rw [sub_eq_add_neg, neg_add, neg_neg, sub_eq_add_neg, add_comm]
-
-theorem sub_self (a : α) : a - a = 0 := by
-  rw [sub_eq_add_neg, add_neg_cancel]
-
-theorem sub_eq_iff {a b c : α} : a - b = c ↔ a = c + b := by
-  rw [sub_eq_add_neg]
-  constructor
-  next => intro; subst c; rw [add_assoc, neg_add_cancel, add_zero]
-  next => intro; subst a; rw [add_assoc, add_comm b, neg_add_cancel, add_zero]
-
-theorem sub_eq_zero_iff {a b : α} : a - b = 0 ↔ a = b := by
-  simp [sub_eq_iff, zero_add]
-
-theorem intCast_zero : ((0 : Int) : α) = 0 := intCast_ofNat 0
-theorem intCast_one : ((1 : Int) : α) = 1 := intCast_ofNat 1
-theorem intCast_neg_one : ((-1 : Int) : α) = -1 := by rw [intCast_neg, intCast_ofNat]
 theorem intCast_natCast (n : Nat) : ((n : Int) : α) = (n : α) := by
   erw [intCast_ofNat]
   rw [ofNat_eq_natCast]
+
+instance toAddCommGroup [I : Ring α] : AddCommGroup α :=
+  { I with }
+
+theorem intCast_zero : ((0 : Int) : α) = 0 := by
+  rw [intCast_ofNat 0]
+theorem intCast_one : ((1 : Int) : α) = 1 := intCast_ofNat 1
+theorem intCast_neg_one : ((-1 : Int) : α) = -1 := by rw [intCast_neg, intCast_ofNat]
 theorem intCast_natCast_add_one (n : Nat) : ((n + 1 : Int) : α) = (n : α) + 1 := by
   rw [← Int.natCast_add_one, intCast_natCast, natCast_add, ofNat_eq_natCast]
 theorem intCast_negSucc (n : Nat) : ((-(n + 1) : Int) : α) = -((n : α) + 1) := by
@@ -273,7 +232,8 @@ theorem intCast_nat_sub {x y : Nat} (h : x ≥ y) : (((x - y : Nat) : Int) : α)
       rw [this, intCast_natCast_add_one]
       specialize ih (by omega)
       rw [intCast_natCast] at ih
-      rw [ih, natCast_succ, sub_eq_add_neg, sub_eq_add_neg, add_assoc, add_comm _ 1, ← add_assoc]
+      rw [ih, natCast_succ, sub_eq_add_neg, sub_eq_add_neg, add_assoc,
+        AddCommMonoid.add_comm _ 1, ← add_assoc]
 theorem intCast_add (x y : Int) : ((x + y : Int) : α) = ((x : α) + (y : α)) :=
   match x, y with
   | (x : Nat), (y : Nat) => by
@@ -323,19 +283,36 @@ theorem neg_mul (a b : α) : (-a) * b = -(a * b) := by
 theorem mul_neg (a b : α) : a * (-b) = -(a * b) := by
   rw [neg_eq_mul_neg_one b, neg_eq_mul_neg_one (a * b), mul_assoc]
 
-theorem intCast_nat_mul (x y : Nat) : ((x * y : Int) : α) = ((x : α) * (y : α)) := by
+attribute [local instance] Ring.zsmul in
+theorem zsmul_eq_intCast_mul {k : Int} {a : α} : (HMul.hMul (α := Int) (γ := α) k a : α) = (k : α) * a := by
+  match k with
+  | (k : Nat) =>
+    rw [intCast_natCast, zsmul_natCast_eq_nsmul, nsmul_eq_natCast_mul]
+  | -(k + 1 : Nat) =>
+    rw [intCast_neg, neg_mul, neg_zsmul, intCast_natCast, zsmul_natCast_eq_nsmul, nsmul_eq_natCast_mul]
+
+instance toIntModule [I : Ring α] : IntModule α :=
+  { I, Semiring.toNatModule (α := α) with
+    zero_zsmul a := by rw [← Int.natCast_zero, zsmul_natCast_eq_nsmul, zero_nsmul]
+    one_zsmul a := by rw [← Int.natCast_one, zsmul_natCast_eq_nsmul, one_nsmul]
+    add_zsmul n m a := by rw [zsmul_eq_intCast_mul, intCast_add, right_distrib, zsmul_eq_intCast_mul, zsmul_eq_intCast_mul]
+    zsmul_zero n := by rw [zsmul_eq_intCast_mul, mul_zero]
+    zsmul_add n a b := by
+      rw [zsmul_eq_intCast_mul, left_distrib, zsmul_eq_intCast_mul, zsmul_eq_intCast_mul] }
+
+private theorem intCast_mul_aux (x y : Nat) : ((x * y : Int) : α) = ((x : α) * (y : α)) := by
   rw [Int.ofNat_mul_ofNat, intCast_natCast, natCast_mul]
 
 theorem intCast_mul (x y : Int) : ((x * y : Int) : α) = ((x : α) * (y : α)) :=
   match x, y with
   | (x : Nat), (y : Nat) => by
-    rw [intCast_nat_mul, intCast_natCast, intCast_natCast]
+    rw [intCast_mul_aux, intCast_natCast, intCast_natCast]
   | (x : Nat), (-(y + 1 : Nat)) => by
-    rw [Int.mul_neg, intCast_neg, intCast_nat_mul, intCast_neg, mul_neg, intCast_natCast, intCast_natCast]
+    rw [Int.mul_neg, intCast_neg, intCast_mul_aux, intCast_neg, mul_neg, intCast_natCast, intCast_natCast]
   | (-(x + 1 : Nat)), (y : Nat) => by
-    rw [Int.neg_mul, intCast_neg, intCast_nat_mul, intCast_neg, neg_mul, intCast_natCast, intCast_natCast]
+    rw [Int.neg_mul, intCast_neg, intCast_mul_aux, intCast_neg, neg_mul, intCast_natCast, intCast_natCast]
   | (-(x + 1 : Nat)), (-(y + 1 : Nat)) => by
-    rw [Int.neg_mul_neg, intCast_neg, intCast_neg, neg_mul, mul_neg, neg_neg, intCast_nat_mul,
+    rw [Int.neg_mul_neg, intCast_neg, intCast_neg, neg_mul, mul_neg, neg_neg, intCast_mul_aux,
       intCast_natCast, intCast_natCast]
 
 theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k := by
@@ -343,27 +320,8 @@ theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k :=
   next => simp [pow_zero, Int.pow_zero, intCast_one]
   next k ih => simp [pow_succ, Int.pow_succ, intCast_mul, *]
 
-instance : IntModule α where
-  hmulInt := ⟨fun a x => a * x⟩
-  hmulNat := ⟨fun a x => a * x⟩
-  hmul_nat n x := by
-    change ((n : Int) : α) * x = (n : α) * x
-    rw [intCast_natCast]
-  add_zero := by simp [add_zero]
-  add_assoc := by simp [add_assoc]
-  add_comm := by simp [add_comm]
-  zero_hmul := by simp [intCast_zero, zero_mul]
-  one_hmul := by simp [intCast_one, one_mul]
-  add_hmul := by simp [intCast_add, right_distrib]
-  hmul_zero := by simp [mul_zero]
-  hmul_add := by simp [left_distrib]
-  neg_add_cancel := by simp [neg_add_cancel]
-  sub_eq_add_neg := by simp [sub_eq_add_neg]
-
-theorem hmul_eq_intCast_mul {α} [Ring α] {k : Int} {a : α} : HMul.hMul (α := Int) k a = (k : α) * a := rfl
-
 -- Verify that the diamond from `Ring` to `NatModule` via either `Semiring` or `IntModule` is defeq.
-example [Ring R] : (Semiring.instNatModule : NatModule R) = (IntModule.toNatModule R) := rfl
+example [Ring R] : (Semiring.toNatModule : NatModule R) = IntModule.toNatModule (M := R) := rfl
 
 end Ring
 
@@ -378,7 +336,9 @@ theorem mul_left_comm (a b c : α) : a * (b * c) = b * (a * c) := by
 
 end CommSemiring
 
-open Semiring Ring CommSemiring CommRing
+open Semiring hiding add_comm add_assoc add_zero
+open Ring hiding neg_add_cancel
+open CommSemiring CommRing
 
 /--
 A ring `α` has characteristic `p` if `OfNat.ofNat x = 0` iff `x % p = 0`.
@@ -450,6 +410,8 @@ end Semiring
 
 section Ring
 
+open AddCommMonoid AddCommGroup
+
 variable (p)  {α : Type u} [Ring α] [IsCharP α p]
 
 private theorem mk'_aux {x y : Nat} (p : Nat) (h : y ≤ x) :
@@ -525,7 +487,8 @@ theorem intCast_ext_iff {x y : Int} : (x : α) = (y : α) ↔ x % p = y % p := b
     have : ((x - y : Int) : α) = 0 :=
       (intCast_eq_zero_iff p _).mpr (by rw [Int.sub_emod, h, Int.sub_self, Int.zero_emod])
     replace this := congrArg (· + (y : α)) this
-    simpa [intCast_sub, zero_add, sub_eq_add_neg, add_assoc, neg_add_cancel, add_zero] using this
+    simpa [intCast_sub, zero_add, AddCommGroup.sub_eq_add_neg, add_assoc,
+      neg_add_cancel, add_zero] using this
 
 theorem intCast_emod (x : Int) : ((x % p : Int) : α) = (x : α) := by
   rw [intCast_ext_iff p, Int.emod_emod]
@@ -534,6 +497,8 @@ end Ring
 
 end IsCharP
 
+open AddCommGroup
+
 theorem no_int_zero_divisors {α : Type u} [IntModule α] [NoNatZeroDivisors α] {k : Int} {a : α}
     : k ≠ 0 → k * a = 0 → a = 0 := by
   match k with
@@ -541,15 +506,15 @@ theorem no_int_zero_divisors {α : Type u} [IntModule α] [NoNatZeroDivisors α]
     simp only [ne_eq, Int.natCast_eq_zero]
     intro h₁ h₂
     replace h₁ : k ≠ 0 := by intro h; simp [h] at h₁
-    rw [IntModule.hmul_nat] at h₂
+    rw [IntModule.zsmul_natCast_eq_nsmul] at h₂
     exact NoNatZeroDivisors.eq_zero_of_mul_eq_zero h₁ h₂
   | -(k+1 : Nat) =>
-    rw [IntModule.neg_hmul]
+    rw [IntModule.neg_zsmul]
     intro _ h
     replace h := congrArg (-·) h
     dsimp only at h
-    rw [IntModule.neg_neg, IntModule.neg_zero] at h
-    rw [IntModule.hmul_nat] at h
+    rw [neg_neg, neg_zero] at h
+    rw [IntModule.zsmul_natCast_eq_nsmul] at h
     exact NoNatZeroDivisors.eq_zero_of_mul_eq_zero (Nat.succ_ne_zero _) h
 
 end Lean.Grind

src/Init/Grind/Ring/Envelope.lean

@@ -141,7 +141,7 @@ def Q.ind {β : Q α → Prop} (mk : ∀ (a : α × α), β (Q.mk a)) (q : Q α)
         exact ⟨k, h.symm⟩)
 
 attribute [local simp]
-  Quot.liftOn Semiring.add_zero Semiring.zero_add Semiring.mul_one Semiring.one_mul
+  Quot.liftOn Semiring.add_zero AddCommMonoid.zero_add Semiring.mul_one Semiring.one_mul
   Semiring.natCast_zero Semiring.natCast_one Semiring.mul_zero Semiring.zero_mul
 
 theorem neg_add_cancel (a : Q α) : add (neg a) a = natCast 0 := by
@@ -236,7 +236,28 @@ private theorem pow_zero (a : Q α) : hPow a 0 = natCast 1 := rfl
 
 private theorem pow_succ (a : Q α) (n : Nat) : hPow a (n+1) = mul (hPow a n) a := rfl
 
+def nsmul (n : Nat) (a : Q α) : Q α :=
+  mul (natCast n) a
+
+def zsmul (i : Int) (a : Q α) : Q α :=
+  mul (intCast i) a
+
+theorem neg_zsmul (i : Int) (a : Q α) : zsmul (-i) a = neg (zsmul i a) := by
+  induction a using Quot.ind
+  next a =>
+  cases a; simp [zsmul]
+  split <;> rename_i h₁
+  · split <;> rename_i h₂
+    · omega
+    · simp
+  · split <;> rename_i h₂
+    · simp
+    · have : i = 0 := by omega
+      simp [this]
+
 def ofSemiring : Ring (Q α) := {
+  nsmul := ⟨nsmul⟩
+  zsmul := ⟨zsmul⟩
   ofNat   := fun n => ⟨natCast n⟩
   natCast := ⟨natCast⟩
   intCast := ⟨intCast⟩
@@ -245,7 +266,7 @@ def ofSemiring : Ring (Q α) := {
   neg_add_cancel, sub_eq_add_neg
   mul_one, one_mul, zero_mul, mul_zero, mul_assoc,
   left_distrib, right_distrib, pow_zero, pow_succ,
-  intCast_neg, ofNat_succ
+  intCast_neg, ofNat_succ, neg_zsmul
 }
 
 attribute [instance] ofSemiring
@@ -328,7 +349,8 @@ instance [Semiring α] [AddRightCancel α] [NoNatZeroDivisors α] : NoNatZeroDiv
     simp [r] at h₂
     rcases h₂ with ⟨k', h₂⟩
     replace h₂ := AddRightCancel.add_right_cancel _ _ _ h₂
-    simp [← Semiring.left_distrib] at h₂
+    simp only [← Semiring.left_distrib] at h₂
+    simp only [← Semiring.nsmul_eq_natCast_mul] at h₂
     replace h₂ := NoNatZeroDivisors.no_nat_zero_divisors k (a₁ + b₂) (a₂ + b₁) h₁ h₂
     apply Quot.sound; simp [r]; exists 0; simp [h₂]
 
@@ -400,7 +422,7 @@ instance [Preorder α] [OrderedAdd α] : Preorder (OfSemiring.Q α) where
 
 @[local simp] private theorem mk_pos [Preorder α] [OrderedAdd α] {a₁ a₂ : α} :
     0 < Q.mk (a₁, a₂) ↔ a₂ < a₁ := by
-  simp [← toQ_ofNat, toQ, mk_lt_mk, Semiring.zero_add]
+  simp [← toQ_ofNat, toQ, mk_lt_mk, AddCommMonoid.zero_add]
 
 @[local simp]
 theorem toQ_le [Preorder α] [OrderedAdd α] {a b : α} : toQ a ≤ toQ b ↔ a ≤ b := by

src/Init/Grind/Ring/Field.lean

@@ -57,10 +57,10 @@ theorem inv_inv (a : α) : a⁻¹⁻¹ = a := by
 theorem inv_neg (a : α) : (-a)⁻¹ = -a⁻¹ := by
   by_cases h : a = 0
   · subst h
-    simp [Field.inv_zero, Ring.neg_zero]
+    simp [Field.inv_zero, AddCommGroup.neg_zero]
   · symm
     apply eq_inv_of_mul_eq_one
-    simp [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg, Field.inv_mul_cancel h]
+    simp [Ring.neg_mul, Ring.mul_neg, AddCommGroup.neg_neg, Field.inv_mul_cancel h]
 
 theorem inv_eq_zero_iff {a : α} : a⁻¹ = 0 ↔ a = 0 := by
   constructor
@@ -129,7 +129,7 @@ instance [IsCharP α 0] : NoNatZeroDivisors α := NoNatZeroDivisors.mk' <| by
     rw [Semiring.ofNat_eq_natCast] at w
     replace w := congrArg (fun x => x * b⁻¹) w
     dsimp only [] at w
-    rw [Semiring.hmul_eq_ofNat_mul, Semiring.mul_assoc, Field.mul_inv_cancel h, Semiring.mul_one,
+    rw [Semiring.nsmul_eq_ofNat_mul, Semiring.mul_assoc, Field.mul_inv_cancel h, Semiring.mul_one,
       Semiring.natCast_zero, Semiring.zero_mul, Semiring.ofNat_eq_natCast] at w
     contradiction
 

src/Init/Grind/Ring/OfSemiring.lean

@@ -80,7 +80,9 @@ end Ring.OfSemiring
 
 namespace CommRing
 attribute [local instance] Semiring.natCast Ring.intCast
-open Semiring Ring CommSemiring
+open AddCommMonoid AddCommGroup
+open Semiring hiding add_zero add_comm add_assoc
+open Ring CommSemiring
 
 inductive Poly.NonnegCoeffs : Poly → Prop
   | num (c : Int) : c ≥ 0 → NonnegCoeffs (.num c)

src/Init/Grind/Ring/Poly.lean

@@ -245,7 +245,7 @@ instance : LawfulBEq Poly where
 def Poly.denote [Ring α] (ctx : Context α) (p : Poly) : α :=
   match p with
   | .num k => Int.cast k
-  | .add k m p => Int.cast k * m.denote ctx + denote ctx p
+  | .add k m p => HMul.hMul (α := Int) k (m.denote ctx) + denote ctx p
 
 @[expose]
 def Poly.denote' [Ring α] (ctx : Context α) (p : Poly) : α :=
@@ -257,7 +257,7 @@ where
     bif k == 1 then
       m.denote' ctx
     else
-      Int.cast k * m.denote' ctx
+      HMul.hMul (α := Int) k (m.denote' ctx)
 
   go (p : Poly) (acc : α) : α :=
     match p with
@@ -598,7 +598,10 @@ def NullCert.toPolyC (nc : NullCert) (c : Nat) : Poly :=
 Theorems for justifying the procedure for commutative rings in `grind`.
 -/
 
-open Semiring Ring CommSemiring
+open AddCommMonoid AddCommGroup NatModule IntModule
+open Semiring hiding add_zero add_comm add_assoc
+open Ring hiding sub_eq_add_neg
+open CommSemiring
 
 theorem denoteInt_eq {α} [CommRing α] (k : Int) : denoteInt (α := α) k = k := by
   simp [denoteInt, cond_eq_if] <;> split
@@ -700,18 +703,18 @@ theorem Mon.eq_of_grevlex {m₁ m₂ : Mon} : grevlex m₁ m₂ = .eq → m₁ =
   simp [grevlex]; intro; apply eq_of_revlex
 
 theorem Poly.denoteTerm_eq  {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) : denote'.denoteTerm ctx k m = k * m.denote ctx := by
-  simp [denote'.denoteTerm, Mon.denote'_eq_denote, cond_eq_if]; intro; subst k; rw [Ring.intCast_one, Semiring.one_mul]
+  simp [denote'.denoteTerm, Mon.denote'_eq_denote, cond_eq_if, zsmul_eq_intCast_mul]; intro; subst k; rw [Ring.intCast_one, Semiring.one_mul]
 
 theorem Poly.denote'_eq_denote {α} [Ring α] (ctx : Context α) (p : Poly) : p.denote' ctx = p.denote ctx := by
-  cases p <;> simp [denote', denote, denoteTerm_eq]
+  cases p <;> simp [denote', denote, denoteTerm_eq, zsmul_eq_intCast_mul]
   next k m p =>
     generalize k * m.denote ctx = acc
     fun_induction denote'.go <;> simp [denote, *, Ring.intCast_zero, Semiring.add_zero, denoteTerm_eq]
-    next ih => simp [denoteTerm_eq] at ih; simp [ih, Semiring.add_assoc]
+    next ih => simp [denoteTerm_eq] at ih; simp [ih, Semiring.add_assoc, zsmul_eq_intCast_mul]
 
 theorem Poly.denote_ofMon {α} [CommRing α] (ctx : Context α) (m : Mon)
     : denote ctx (ofMon m) = m.denote ctx := by
-  simp [ofMon, denote, intCast_one, intCast_zero, one_mul, add_zero]
+  simp [ofMon, denote, intCast_one, intCast_zero, one_mul, add_zero, zsmul_eq_intCast_mul]
 
 theorem Poly.denote_ofVar {α} [CommRing α] (ctx : Context α) (x : Var)
     : denote ctx (ofVar x) = x.denote ctx := by
@@ -734,7 +737,7 @@ theorem Poly.denote_insert {α} [CommRing α] (ctx : Context α) (k : Int) (m :
     next h =>
       simp at h <;> simp [*, Mon.denote, denote_addConst, mul_one, add_comm]
     next =>
-      fun_induction insert.go <;> simp_all +zetaDelta [denote]
+      fun_induction insert.go <;> simp_all +zetaDelta [denote, zsmul_eq_intCast_mul]
       next h₁ h₂ =>
         rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, h₂, intCast_zero, zero_mul, zero_add]
       next h₁ _ =>
@@ -756,7 +759,7 @@ theorem Poly.denote_mulConst {α} [CommRing α] (ctx : Context α) (k : Int) (p
     split <;> try simp [*, intCast_one, one_mul]
     fun_induction mulConst.go <;> simp [denote, *]
     next => rw [intCast_mul]
-    next => rw [intCast_mul, left_distrib, mul_assoc]
+    next => rw [left_distrib, ← zsmul_eq_intCast_mul, ← zsmul_eq_intCast_mul, mul_zsmul]
 
 theorem Poly.denote_mulMon {α} [CommRing α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (mulMon k m p).denote ctx = k * m.denote ctx * p.denote ctx := by
@@ -767,7 +770,7 @@ theorem Poly.denote_mulMon {α} [CommRing α] (ctx : Context α) (k : Int) (m :
     next h =>
       simp at h; simp [*, Mon.denote, mul_one, denote_mulConst]
     next =>
-      fun_induction mulMon.go <;> simp [denote, *]
+      fun_induction mulMon.go <;> simp [denote, zsmul_eq_intCast_mul, *]
       next h => simp +zetaDelta at h; simp [*, intCast_zero, mul_zero]
       next => simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc]
       next => simp [Mon.denote_mul, intCast_mul, left_distrib, mul_left_comm, mul_assoc]
@@ -776,7 +779,7 @@ theorem Poly.denote_combine {α} [CommRing α] (ctx : Context α) (p₁ p₂ : P
     : (combine p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   unfold combine; generalize hugeFuel = fuel
   fun_induction combine.go
-    <;> simp [*, denote_concat, denote_addConst, denote, intCast_add, add_comm, add_left_comm, add_assoc]
+    <;> simp [*, denote_concat, denote_addConst, denote, intCast_add, add_comm, add_left_comm, add_assoc, zsmul_eq_intCast_mul]
   case case5 hg _ h _ =>
     simp +zetaDelta at h
     rw [← add_assoc, Mon.eq_of_grevlex hg, ← right_distrib, ← intCast_add, h, intCast_zero, zero_mul, zero_add]
@@ -787,7 +790,7 @@ theorem Poly.denote_combine {α} [CommRing α] (ctx : Context α) (p₁ p₂ : P
 theorem Poly.denote_mul_go {α} [CommRing α] (ctx : Context α) (p₁ p₂ acc : Poly)
     : (mul.go p₂ p₁ acc).denote ctx = acc.denote ctx + p₁.denote ctx * p₂.denote ctx := by
   fun_induction mul.go
-    <;> simp [denote_combine, denote_mulConst, denote, *, right_distrib, denote_mulMon, add_assoc]
+    <;> simp [denote_combine, denote_mulConst, denote, *, right_distrib, denote_mulMon, add_assoc, zsmul_eq_intCast_mul]
 
 theorem Poly.denote_mul {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
     : (mul p₁ p₂).denote ctx = p₁.denote ctx * p₂.denote ctx := by
@@ -860,7 +863,7 @@ theorem NullCert.eq_nzdiv {α} [CommRing α] [NoNatZeroDivisors α] (ctx : Conte
   apply eqsImplies_helper
   intro h₃
   replace h₂ := congrArg (Poly.denote ctx) h₂
-  simp [Expr.denote_toPoly, Poly.denote_mulConst, denote_toPoly, h₃, Expr.denote] at h₂
+  simp [Expr.denote_toPoly, Poly.denote_mulConst, denote_toPoly, h₃, Expr.denote, ← zsmul_eq_intCast_mul] at h₂
   replace h₂ := no_int_zero_divisors h₁ h₂
   rw [sub_eq_zero_iff] at h₂
   assumption
@@ -902,7 +905,7 @@ theorem Poly.denote_insertC {α c} [CommRing α] [IsCharP α c] (ctx : Context
     rw [← IsCharP.intCast_emod (p := c)]
     simp +zetaDelta [*, intCast_zero, zero_mul, zero_add]
   next =>
-    fun_induction insertC.go <;> simp_all +zetaDelta [denote]
+    fun_induction insertC.go <;> simp_all +zetaDelta [denote, zsmul_eq_intCast_mul]
     next h₁ _ h₂ => rw [IsCharP.intCast_emod]
     next h₁ _ h₂ =>
       rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, ← IsCharP.intCast_emod (p := c), h₂,
@@ -928,10 +931,10 @@ theorem Poly.denote_mulConstC {α c} [CommRing α] [IsCharP α c] (ctx : Context
       next => rw [intCast_mul]
       next h _ =>
         simp +zetaDelta at h
-        rw [left_distrib, ← mul_assoc, ← intCast_mul, ← IsCharP.intCast_emod (x := k * _) (p := c),
+        rw [left_distrib, zsmul_eq_intCast_mul, ← mul_assoc, ← intCast_mul, ← IsCharP.intCast_emod (x := k * _) (p := c),
             h, intCast_zero, zero_mul, zero_add]
       next h _ =>
-        simp +zetaDelta [IsCharP.intCast_emod, intCast_mul, mul_assoc, left_distrib]
+        simp +zetaDelta [IsCharP.intCast_emod, intCast_mul, mul_assoc, left_distrib, zsmul_eq_intCast_mul]
 
 theorem Poly.denote_mulMonC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
     : (mulMonC k m p c).denote ctx = k * m.denote ctx * p.denote ctx := by
@@ -950,23 +953,23 @@ theorem Poly.denote_mulMonC {α c} [CommRing α] [IsCharP α c] (ctx : Context
         rw [mul_assoc, mul_left_comm, ← intCast_mul, ← IsCharP.intCast_emod (x := k * _) (p := c), h]
         simp [intCast_zero, mul_zero]
       next h =>
-        simp +zetaDelta [IsCharP.intCast_emod, intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc]
+        simp +zetaDelta [IsCharP.intCast_emod, intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc, zsmul_eq_intCast_mul]
       next h _ =>
-        simp +zetaDelta at h; simp [*, left_distrib]
+        simp +zetaDelta at h; simp [*, left_distrib, zsmul_eq_intCast_mul]
         rw [mul_left_comm]
         conv => rhs; rw [← mul_assoc, ← mul_assoc, ← intCast_mul, ← IsCharP.intCast_emod (p := c)]
         rw [Int.mul_comm] at h
         simp [h, intCast_zero, zero_mul, zero_add]
       next h _ =>
         simp +zetaDelta [*, IsCharP.intCast_emod, Mon.denote_mul, intCast_mul, left_distrib,
-          mul_left_comm, mul_assoc]
+          mul_left_comm, mul_assoc, zsmul_eq_intCast_mul]
 
 theorem Poly.denote_combineC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly)
     : (combineC p₁ p₂ c).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   unfold combineC; generalize hugeFuel = fuel
   fun_induction combineC.go
     <;> simp [*, denote_concat, denote_addConstC, denote, intCast_add,
-          add_comm, add_left_comm, add_assoc, IsCharP.intCast_emod]
+          add_comm, add_left_comm, add_assoc, IsCharP.intCast_emod, zsmul_eq_intCast_mul]
   next hg _ h _ =>
     simp +zetaDelta at h
     rw [← add_assoc, Mon.eq_of_grevlex hg, ← right_distrib, ← intCast_add,
@@ -979,7 +982,7 @@ theorem Poly.denote_combineC {α c} [CommRing α] [IsCharP α c] (ctx : Context
 theorem Poly.denote_mulC_go {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ p₂ acc : Poly)
     : (mulC.go p₂ c p₁ acc).denote ctx = acc.denote ctx + p₁.denote ctx * p₂.denote ctx := by
   fun_induction mulC.go
-    <;> simp [denote_combineC, denote_mulConstC, denote, *, right_distrib, denote_mulMonC, add_assoc]
+    <;> simp [denote_combineC, denote_mulConstC, denote, *, right_distrib, denote_mulMonC, add_assoc, zsmul_eq_intCast_mul]
 
 theorem Poly.denote_mulC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly)
     : (mulC p₁ p₂ c).denote ctx = p₁.denote ctx * p₂.denote ctx := by
@@ -1043,7 +1046,7 @@ theorem NullCert.eq_nzdivC {α c} [CommRing α] [IsCharP α c] [NoNatZeroDivisor
   apply eqsImplies_helper
   intro h₃
   replace h₂ := congrArg (Poly.denote ctx) h₂
-  simp [Expr.denote_toPolyC, Poly.denote_mulConstC, denote_toPolyC, h₃, Expr.denote] at h₂
+  simp [Expr.denote_toPolyC, Poly.denote_mulConstC, denote_toPolyC, h₃, Expr.denote, ← zsmul_eq_intCast_mul] at h₂
   replace h₂ := no_int_zero_divisors h₁ h₂
   rw [sub_eq_zero_iff] at h₂
   assumption
@@ -1119,7 +1122,7 @@ def div_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
 def div {α} [CommRing α] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly)
     : div_cert p₁ k p → p₁.denote ctx = 0 → p.denote ctx = 0 := by
   simp [div_cert]; intro hnz _ h; subst p₁
-  simp [Poly.denote_mulConst] at h
+  simp [Poly.denote_mulConst, ← zsmul_eq_intCast_mul] at h
   exact no_int_zero_divisors hnz h
 
 @[expose]
@@ -1172,7 +1175,7 @@ def imp_keq_cert (lhs rhs : Expr) (k : Int) (p₁ p₂ : Poly) : Bool :=
 theorem imp_keq  {α} [CommRing α] (ctx : Context α) [NoNatZeroDivisors α] (k : Int) (lhs rhs : Expr) (p₁ p₂ : Poly)
     : imp_keq_cert lhs rhs k p₁ p₂ → k * p₁.denote ctx = p₂.denote ctx → lhs.denote ctx = rhs.denote ctx := by
   simp [imp_keq_cert]; intro hnz _ _; subst p₁ p₂
-  simp [Expr.denote_toPoly, Expr.denote, Poly.denote, intCast_zero]
+  simp [Expr.denote_toPoly, Expr.denote, Poly.denote, intCast_zero, ← zsmul_eq_intCast_mul]
   intro h; replace h := no_int_zero_divisors hnz h
   rw [← sub_eq_zero_iff, h]
 
@@ -1213,7 +1216,7 @@ def div_certC (p₁ : Poly) (k : Int) (p : Poly) (c : Nat) : Bool :=
 def divC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly)
     : div_certC p₁ k p c → p₁.denote ctx = 0 → p.denote ctx = 0 := by
   simp [div_certC]; intro hnz _ h; subst p₁
-  simp [Poly.denote_mulConstC] at h
+  simp [Poly.denote_mulConstC, ← zsmul_eq_intCast_mul] at h
   exact no_int_zero_divisors hnz h
 
 @[expose]
@@ -1272,7 +1275,7 @@ def imp_keq_certC (lhs rhs : Expr) (k : Int) (p₁ p₂ : Poly) (c : Nat) : Bool
 theorem imp_keqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) [NoNatZeroDivisors α] (k : Int) (lhs rhs : Expr) (p₁ p₂ : Poly)
     : imp_keq_certC lhs rhs k p₁ p₂ c → k * p₁.denote ctx = p₂.denote ctx → lhs.denote ctx = rhs.denote ctx := by
   simp [imp_keq_certC]; intro hnz _ _; subst p₁ p₂
-  simp [Expr.denote_toPolyC, Expr.denote, Poly.denote, intCast_zero]
+  simp [Expr.denote_toPolyC, Expr.denote, Poly.denote, intCast_zero, ← zsmul_eq_intCast_mul]
   intro h; replace h := no_int_zero_divisors hnz h
   rw [← sub_eq_zero_iff, h]
 
@@ -1294,8 +1297,8 @@ where
 @[expose]
 def Poly.denoteAsIntModule [CommRing α] (ctx : Context α) (p : Poly) : α :=
   match p with
-  | .num k => Int.cast k * One.one
-  | .add k m p => Int.cast k * m.denoteAsIntModule ctx + denoteAsIntModule ctx p
+  | .num k => HMul.hMul (α := Int) k (One.one : α)
+  | .add k m p => HMul.hMul (α := Int) k (m.denoteAsIntModule ctx) + denoteAsIntModule ctx p
 
 theorem Mon.denoteAsIntModule_go_eq_denote {α} [CommRing α] (ctx : Context α) (m : Mon) (acc : α)
     : denoteAsIntModule.go ctx m acc = acc * m.denote ctx := by
@@ -1306,7 +1309,7 @@ theorem Mon.denoteAsIntModule_eq_denote {α} [CommRing α] (ctx : Context α) (m
   cases m <;> simp [denoteAsIntModule, denote, denoteAsIntModule_go_eq_denote]; rfl
 
 theorem Poly.denoteAsIntModule_eq_denote {α} [CommRing α] (ctx : Context α) (p : Poly) : p.denoteAsIntModule ctx = p.denote ctx := by
-  induction p <;> simp [*, denoteAsIntModule, denote, mul_one, One.one, Mon.denoteAsIntModule_eq_denote]
+  induction p <;> simp [*, denoteAsIntModule, denote, mul_one, One.one, Mon.denoteAsIntModule_eq_denote, Ring.zsmul_eq_intCast_mul]
 
 open Stepwise
 
@@ -1404,7 +1407,7 @@ theorem one_eq_zero_unsat {α} [Field α] (ctx : Context α) (p : Poly) : one_eq
 theorem diseq_to_eq {α} [Field α] (a b : α) : a ≠ b → (a - b)*(a - b)⁻¹ = 1 := by
   intro h
   have : a - b ≠ 0 := by
-    intro h'; rw [Ring.sub_eq_zero_iff.mp h'] at h
+    intro h'; rw [sub_eq_zero_iff.mp h'] at h
     contradiction
   exact Field.mul_inv_cancel this
 
@@ -1429,8 +1432,8 @@ theorem Poly.normEq0_eq {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Na
     simp [denote, normEq0]; split <;> simp [denote]
     next h' => rw [of_mod_eq_0 h h', Ring.intCast_zero]
   next a m p ih =>
-    simp [denote, normEq0]; split <;> simp [denote, *]
-    next h' => rw [of_mod_eq_0 h h', Semiring.zero_mul, Semiring.zero_add]
+    simp [denote, normEq0]; split <;> simp [denote, zsmul_eq_intCast_mul, *]
+    next h' => rw [of_mod_eq_0 h h', Semiring.zero_mul, zero_add]
 
 @[expose]
 def eq_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool :=
@@ -1449,7 +1452,7 @@ theorem gcd_eq_0 [CommRing α] (g n m a b : Int) (h : g = a * n + b * m)
   replace h₂ := congrArg (Int.cast (R := α) b * ·) h₂; simp at h₂
   rw [← Ring.intCast_mul, Ring.intCast_zero, Semiring.mul_zero] at h₂
   replace h₁ := congrArg (· + Int.cast (b * m)) h₁; simp at h₁
-  rw [← Ring.intCast_add, h₂, Semiring.zero_add, ← h] at h₁
+  rw [← Ring.intCast_add, h₂, zero_add, ← h] at h₁
   rw [Ring.intCast_zero, h₁]
 
 @[expose]

src/Init/GrindInstances/Ring/BitVec.lean

@@ -16,6 +16,8 @@ public section
 namespace Lean.Grind
 
 instance : CommRing (BitVec w) where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := BitVec.add_assoc
   add_comm := BitVec.add_comm
   add_zero := BitVec.add_zero
@@ -33,6 +35,12 @@ instance : CommRing (BitVec w) where
   pow_succ _ _ := BitVec.pow_succ
   ofNat_succ x := BitVec.ofNat_add x 1
   intCast_neg _ := BitVec.ofInt_neg
+  neg_zsmul i x := by
+    change (BitVec.ofInt _ (-i) * x = _)
+    rw [BitVec.ofInt_neg]
+    rw [BitVec.neg_mul]
+    rfl
+  zsmul_natCast_eq_nsmul _ _ := rfl
 
 instance : IsCharP (BitVec w) (2 ^ w) := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by simp [BitVec.toNat_eq])

src/Init/GrindInstances/Ring/Fin.lean

@@ -74,6 +74,29 @@ private theorem neg_neg [NeZero n] (a : Fin n) : - - a = a := by
    have : NeZero (n - (a + 1)) := ⟨by omega⟩
    rw [Nat.self_sub_mod, Nat.sub_sub_eq_min, Nat.min_eq_right (Nat.le_of_lt h)]
 
+theorem _root_.Nat.sub_sub_right (a : Nat) {b c : Nat} (h : c ≤ b) : a - (b - c) = a + c - b := by omega
+
+theorem neg_mul [NeZero n] (a b : Fin n) : (-a) * b = -(a * b) := by
+  rcases a with ⟨a, ha⟩; rcases b with ⟨b, hb⟩
+  ext
+  simp only [Fin.neg_def, Fin.mul_def, Nat.mod_mul_mod]
+  rw [Nat.sub_mul]
+  rw [Nat.mod_eq_mod_iff]
+  match b with
+  | 0 => refine ⟨1, 0, by simp⟩
+  | b+1 =>
+    refine ⟨a*(b+1)/n, b, ?_⟩
+    rw [Nat.mod_def, Nat.mul_add_one, Nat.mul_comm _ n, Nat.mul_comm b n]
+    have : n * (a * (b + 1) / n) ≤ a * (b + 1) := Nat.mul_div_le (a * (b + 1)) n
+    have := Nat.lt_mul_div_succ (a * (b + 1)) (show 0 < n by omega)
+    rw [Nat.mul_add_one n] at this
+    have : a * (b + 1) ≤ n * b + n := by
+      rw [Nat.mul_add_one]
+      have := Nat.mul_le_mul_right b ha
+      rw [Nat.succ_mul] at this
+      omega
+    omega
+
 open Fin.NatCast Fin.IntCast in
 theorem intCast_neg [NeZero n] (i : Int) : Int.cast (R := Fin n) (-i) = - Int.cast (R := Fin n) i := by
   simp [Int.cast, IntCast.intCast, Fin.intCast]
@@ -81,7 +104,10 @@ theorem intCast_neg [NeZero n] (i : Int) : Int.cast (R := Fin n) (-i) = - Int.ca
   next h₁ h₂ => simp [Int.le_antisymm h₁ h₂, Fin.neg_def]
   next => simp [Fin.neg_neg]
 
+open Fin.NatCast Fin.IntCast in
 instance (n : Nat) [NeZero n] : CommRing (Fin n) where
+  nsmul := ⟨fun k i => (k : Fin n) * i⟩
+  zsmul := ⟨fun k i => (k : Fin n) * i⟩
   natCast := Fin.NatCast.instNatCast n
   intCast := Fin.IntCast.instIntCast n
   add_assoc := Fin.add_assoc
@@ -98,6 +124,8 @@ instance (n : Nat) [NeZero n] : CommRing (Fin n) where
   ofNat_succ := Fin.ofNat_succ
   sub_eq_add_neg := Fin.sub_eq_add_neg
   intCast_neg := Fin.intCast_neg
+  neg_zsmul i a := by simp [intCast_neg, neg_mul]
+  zsmul_natCast_eq_nsmul _ _ := rfl
 
 instance (n : Nat) [NeZero n] : IsCharP (Fin n) n := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by

src/Init/GrindInstances/Ring/Int.lean

@@ -14,6 +14,7 @@ public section
 namespace Lean.Grind
 
 instance : CommRing Int where
+  nsmul := ⟨(· * ·)⟩
   add_assoc := Int.add_assoc
   add_comm := Int.add_comm
   add_zero := Int.add_zero
@@ -30,6 +31,7 @@ instance : CommRing Int where
   pow_succ _ _ := by rfl
   ofNat_succ _ := by rfl
   sub_eq_add_neg _ _ := Int.sub_eq_add_neg
+  neg_zsmul := Int.neg_mul
 
 instance : IsCharP Int 0 := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by erw [Int.ofNat_eq_zero]; simp)

src/Init/GrindInstances/Ring/SInt.lean

@@ -17,13 +17,25 @@ public section
 
 namespace Lean.Grind
 
-instance : NatCast Int8 where
+@[expose]
+def Int8.natCast : NatCast Int8 where
   natCast x := Int8.ofNat x
 
-instance : IntCast Int8 where
+@[expose]
+def Int8.intCast : IntCast Int8 where
   intCast x := Int8.ofInt x
 
+attribute [local instance] Int8.intCast in
+theorem Int8.intCast_neg (i : Int) : ((-i : Int) : Int8) = -(i : Int8) :=
+  Int8.ofInt_neg _
+
+attribute [local instance] Int8.intCast in
+theorem Int8.intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : Int8) = OfNat.ofNat x := Int8.ofInt_eq_ofNat
+
+attribute [local instance] Int8.natCast Int8.intCast in
 instance : CommRing Int8 where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := Int8.add_assoc
   add_comm := Int8.add_comm
   add_zero := Int8.add_zero
@@ -41,6 +53,8 @@ instance : CommRing Int8 where
   pow_succ := Int8.pow_succ
   ofNat_succ x := Int8.ofNat_add x 1
   intCast_neg := Int8.ofInt_neg
+  neg_zsmul i x := by simp [Int8.intCast_neg, Int8.neg_mul]
+  zsmul_natCast_eq_nsmul n a := congrArg (· * a) (Int8.intCast_ofNat _)
 
 instance : IsCharP Int8 (2 ^ 8) := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by
@@ -56,13 +70,25 @@ example : ToInt.Sub Int8 (.sint 8) := inferInstance
 
 instance : ToInt.Pow Int8 (.sint 8) := ToInt.pow_of_semiring (by simp)
 
-instance : NatCast Int16 where
+@[expose]
+def Int16.natCast : NatCast Int16 where
   natCast x := Int16.ofNat x
 
-instance : IntCast Int16 where
+@[expose]
+def Int16.intCast : IntCast Int16 where
   intCast x := Int16.ofInt x
 
+attribute [local instance] Int16.intCast in
+theorem Int16.intCast_neg (i : Int) : ((-i : Int) : Int16) = -(i : Int16) :=
+  Int16.ofInt_neg _
+
+attribute [local instance] Int16.intCast in
+theorem Int16.intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : Int16) = OfNat.ofNat x := Int16.ofInt_eq_ofNat
+
+attribute [local instance] Int16.natCast Int16.intCast in
 instance : CommRing Int16 where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := Int16.add_assoc
   add_comm := Int16.add_comm
   add_zero := Int16.add_zero
@@ -80,6 +106,8 @@ instance : CommRing Int16 where
   pow_succ := Int16.pow_succ
   ofNat_succ x := Int16.ofNat_add x 1
   intCast_neg := Int16.ofInt_neg
+  neg_zsmul i x := by simp [Int16.intCast_neg, Int16.neg_mul]
+  zsmul_natCast_eq_nsmul n a := congrArg (· * a) (Int16.intCast_ofNat _)
 
 instance : IsCharP Int16 (2 ^ 16) := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by
@@ -95,13 +123,25 @@ example : ToInt.Sub Int16 (.sint 16) := inferInstance
 
 instance : ToInt.Pow Int16 (.sint 16) := ToInt.pow_of_semiring (by simp)
 
-instance : NatCast Int32 where
+@[expose]
+def Int32.natCast : NatCast Int32 where
   natCast x := Int32.ofNat x
 
-instance : IntCast Int32 where
+@[expose]
+def Int32.intCast : IntCast Int32 where
   intCast x := Int32.ofInt x
 
+attribute [local instance] Int32.intCast in
+theorem Int32.intCast_neg (i : Int) : ((-i : Int) : Int32) = -(i : Int32) :=
+  Int32.ofInt_neg _
+
+attribute [local instance] Int32.intCast in
+theorem Int32.intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : Int32) = OfNat.ofNat x := Int32.ofInt_eq_ofNat
+
+attribute [local instance] Int32.natCast Int32.intCast in
 instance : CommRing Int32 where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := Int32.add_assoc
   add_comm := Int32.add_comm
   add_zero := Int32.add_zero
@@ -119,6 +159,8 @@ instance : CommRing Int32 where
   pow_succ := Int32.pow_succ
   ofNat_succ x := Int32.ofNat_add x 1
   intCast_neg := Int32.ofInt_neg
+  neg_zsmul i x := by simp [Int32.intCast_neg, Int32.neg_mul]
+  zsmul_natCast_eq_nsmul n a := congrArg (· * a) (Int32.intCast_ofNat _)
 
 instance : IsCharP Int32 (2 ^ 32) := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by
@@ -134,13 +176,25 @@ example : ToInt.Sub Int32 (.sint 32) := inferInstance
 
 instance : ToInt.Pow Int32 (.sint 32) := ToInt.pow_of_semiring (by simp)
 
-instance : NatCast Int64 where
+@[expose]
+def Int64.natCast : NatCast Int64 where
   natCast x := Int64.ofNat x
 
-instance : IntCast Int64 where
+@[expose]
+def Int64.intCast : IntCast Int64 where
   intCast x := Int64.ofInt x
 
+attribute [local instance] Int64.intCast in
+theorem Int64.intCast_neg (i : Int) : ((-i : Int) : Int64) = -(i : Int64) :=
+  Int64.ofInt_neg _
+
+attribute [local instance] Int64.intCast in
+theorem Int64.intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : Int64) = OfNat.ofNat x := Int64.ofInt_eq_ofNat
+
+attribute [local instance] Int64.natCast Int64.intCast in
 instance : CommRing Int64 where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := Int64.add_assoc
   add_comm := Int64.add_comm
   add_zero := Int64.add_zero
@@ -158,6 +212,8 @@ instance : CommRing Int64 where
   pow_succ := Int64.pow_succ
   ofNat_succ x := Int64.ofNat_add x 1
   intCast_neg := Int64.ofInt_neg
+  neg_zsmul i x := by simp [Int64.intCast_neg, Int64.neg_mul]
+  zsmul_natCast_eq_nsmul n a := congrArg (· * a) (Int64.intCast_ofNat _)
 
 instance : IsCharP Int64 (2 ^ 64) := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by
@@ -173,13 +229,25 @@ example : ToInt.Sub Int64 (.sint 64) := inferInstance
 
 instance : ToInt.Pow Int64 (.sint 64) := ToInt.pow_of_semiring (by simp)
 
-instance : NatCast ISize where
+@[expose]
+def ISize.natCast : NatCast ISize where
   natCast x := ISize.ofNat x
 
-instance : IntCast ISize where
+@[expose]
+def ISize.intCast : IntCast ISize where
   intCast x := ISize.ofInt x
 
+attribute [local instance] ISize.intCast in
+theorem ISize.intCast_neg (i : Int) : ((-i : Int) : ISize) = -(i : ISize) :=
+  ISize.ofInt_neg _
+
+attribute [local instance] ISize.intCast in
+theorem ISize.intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : ISize) = OfNat.ofNat x := ISize.ofInt_eq_ofNat
+
+attribute [local instance] ISize.natCast ISize.intCast in
 instance : CommRing ISize where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := ISize.add_assoc
   add_comm := ISize.add_comm
   add_zero := ISize.add_zero
@@ -197,6 +265,9 @@ instance : CommRing ISize where
   pow_succ := ISize.pow_succ
   ofNat_succ x := ISize.ofNat_add x 1
   intCast_neg := ISize.ofInt_neg
+  neg_zsmul i x := by simp [ISize.intCast_neg, ISize.neg_mul]
+  zsmul_natCast_eq_nsmul n a := congrArg (· * a) (ISize.intCast_ofNat _)
+
 open System.Platform (numBits)
 
 instance : IsCharP ISize (2 ^ numBits) := IsCharP.mk' _ _

src/Init/GrindInstances/Ring/UInt.lean

@@ -18,12 +18,19 @@ namespace UInt8
 /-- Variant of `UInt8.ofNat_mod_size` replacing `2 ^ 8` with `256`.-/
 theorem ofNat_mod_size' : ofNat (x % 256) = ofNat x := ofNat_mod_size
 
-instance : NatCast UInt8 where
+@[expose]
+def natCast : NatCast UInt8 where
   natCast x := UInt8.ofNat x
 
-instance : IntCast UInt8 where
+@[expose]
+def intCast : IntCast UInt8 where
   intCast x := UInt8.ofInt x
 
+attribute [local instance] natCast intCast
+
+theorem intCast_neg (x : Int) : ((-x : Int) : UInt8) = - (x : UInt8) := by
+  simp only [Int.cast, IntCast.intCast, UInt8.ofInt_neg]
+
 theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt8) = OfNat.ofNat x := by
     -- A better proof would be welcome!
     simp only [Int.cast, IntCast.intCast]
@@ -41,12 +48,19 @@ namespace UInt16
 /-- Variant of `UInt16.ofNat_mod_size` replacing `2 ^ 16` with `65536`.-/
 theorem ofNat_mod_size' : ofNat (x % 65536) = ofNat x := ofNat_mod_size
 
-instance : NatCast UInt16 where
+@[expose]
+def natCast : NatCast UInt16 where
   natCast x := UInt16.ofNat x
 
-instance : IntCast UInt16 where
+@[expose]
+def intCast : IntCast UInt16 where
   intCast x := UInt16.ofInt x
 
+attribute [local instance] natCast intCast
+
+theorem intCast_neg (x : Int) : ((-x : Int) : UInt16) = - (x : UInt16) := by
+  simp only [Int.cast, IntCast.intCast, UInt16.ofInt_neg]
+
 theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt16) = OfNat.ofNat x := by
     -- A better proof would be welcome!
     simp only [Int.cast, IntCast.intCast]
@@ -64,12 +78,19 @@ namespace UInt32
 /-- Variant of `UInt32.ofNat_mod_size` replacing `2 ^ 32` with `4294967296`.-/
 theorem ofNat_mod_size' : ofNat (x % 4294967296) = ofNat x := ofNat_mod_size
 
-instance : NatCast UInt32 where
+@[expose]
+def natCast : NatCast UInt32 where
   natCast x := UInt32.ofNat x
 
-instance : IntCast UInt32 where
+@[expose]
+def intCast : IntCast UInt32 where
   intCast x := UInt32.ofInt x
 
+attribute [local instance] natCast intCast
+
+theorem intCast_neg (x : Int) : ((-x : Int) : UInt32) = - (x : UInt32) := by
+  simp only [Int.cast, IntCast.intCast, UInt32.ofInt_neg]
+
 theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt32) = OfNat.ofNat x := by
     -- A better proof would be welcome!
     simp only [Int.cast, IntCast.intCast]
@@ -87,12 +108,19 @@ namespace UInt64
 /-- Variant of `UInt64.ofNat_mod_size` replacing `2 ^ 64` with `18446744073709551616`.-/
 theorem ofNat_mod_size' : ofNat (x % 18446744073709551616) = ofNat x := ofNat_mod_size
 
-instance : NatCast UInt64 where
+@[expose]
+def natCast : NatCast UInt64 where
   natCast x := UInt64.ofNat x
 
-instance : IntCast UInt64 where
+@[expose]
+def intCast : IntCast UInt64 where
   intCast x := UInt64.ofInt x
 
+attribute [local instance] natCast intCast
+
+theorem intCast_neg (x : Int) : ((-x : Int) : UInt64) = - (x : UInt64) := by
+  simp only [Int.cast, IntCast.intCast, UInt64.ofInt_neg]
+
 theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : UInt64) = OfNat.ofNat x := by
     -- A better proof would be welcome!
     simp only [Int.cast, IntCast.intCast]
@@ -107,12 +135,19 @@ end UInt64
 
 namespace USize
 
-instance : NatCast USize where
+@[expose]
+def natCast : NatCast USize where
   natCast x := USize.ofNat x
 
-instance : IntCast USize where
+@[expose]
+def intCast : IntCast USize where
   intCast x := USize.ofInt x
 
+attribute [local instance] natCast intCast
+
+theorem intCast_neg (x : Int) : ((-x : Int) : USize) = - (x : USize) := by
+  simp only [Int.cast, IntCast.intCast, USize.ofInt_neg]
+
 theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : USize) = OfNat.ofNat x := by
     -- A better proof would be welcome!
     simp only [Int.cast, IntCast.intCast]
@@ -127,7 +162,10 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : USize) = OfNat.of
 end USize
 namespace Lean.Grind
 
+attribute [local instance] UInt8.natCast UInt8.intCast in
 instance : CommRing UInt8 where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := UInt8.add_assoc
   add_comm := UInt8.add_comm
   add_zero := UInt8.add_zero
@@ -146,6 +184,8 @@ instance : CommRing UInt8 where
   ofNat_succ x := UInt8.ofNat_add x 1
   intCast_neg := UInt8.ofInt_neg
   intCast_ofNat := UInt8.intCast_ofNat
+  neg_zsmul i a := by simp [UInt8.intCast_neg, UInt8.neg_mul]
+  zsmul_natCast_eq_nsmul n a := congrArg (· * a) (UInt8.intCast_ofNat _)
 
 instance : IsCharP UInt8 256 := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by
@@ -159,7 +199,10 @@ example : ToInt.Sub UInt8 (.uint 8) := inferInstance
 
 instance : ToInt.Pow UInt8 (.uint 8) := ToInt.pow_of_semiring (by simp)
 
+attribute [local instance] UInt16.natCast UInt16.intCast in
 instance : CommRing UInt16 where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := UInt16.add_assoc
   add_comm := UInt16.add_comm
   add_zero := UInt16.add_zero
@@ -178,6 +221,8 @@ instance : CommRing UInt16 where
   ofNat_succ x := UInt16.ofNat_add x 1
   intCast_neg := UInt16.ofInt_neg
   intCast_ofNat := UInt16.intCast_ofNat
+  neg_zsmul i a := by simp [UInt16.intCast_neg, UInt16.neg_mul]
+  zsmul_natCast_eq_nsmul n a := congrArg (· * a) (UInt16.intCast_ofNat _)
 
 instance : IsCharP UInt16 65536 := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by
@@ -191,7 +236,10 @@ example : ToInt.Sub UInt16 (.uint 16) := inferInstance
 
 instance : ToInt.Pow UInt16 (.uint 16) := ToInt.pow_of_semiring (by simp)
 
+attribute [local instance] UInt32.natCast UInt32.intCast in
 instance : CommRing UInt32 where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := UInt32.add_assoc
   add_comm := UInt32.add_comm
   add_zero := UInt32.add_zero
@@ -210,6 +258,8 @@ instance : CommRing UInt32 where
   ofNat_succ x := UInt32.ofNat_add x 1
   intCast_neg := UInt32.ofInt_neg
   intCast_ofNat := UInt32.intCast_ofNat
+  neg_zsmul i a := by simp [UInt32.intCast_neg, UInt32.neg_mul]
+  zsmul_natCast_eq_nsmul n a := congrArg (· * a) (UInt32.intCast_ofNat _)
 
 instance : IsCharP UInt32 4294967296 := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by
@@ -223,7 +273,10 @@ example : ToInt.Sub UInt32 (.uint 32) := inferInstance
 
 instance : ToInt.Pow UInt32 (.uint 32) := ToInt.pow_of_semiring (by simp)
 
+attribute [local instance] UInt64.natCast UInt64.intCast in
 instance : CommRing UInt64 where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := UInt64.add_assoc
   add_comm := UInt64.add_comm
   add_zero := UInt64.add_zero
@@ -242,6 +295,8 @@ instance : CommRing UInt64 where
   ofNat_succ x := UInt64.ofNat_add x 1
   intCast_neg := UInt64.ofInt_neg
   intCast_ofNat := UInt64.intCast_ofNat
+  neg_zsmul i a := by simp [UInt64.intCast_neg, UInt64.neg_mul]
+  zsmul_natCast_eq_nsmul n a := congrArg (· * a) (UInt64.intCast_ofNat _)
 
 instance : IsCharP UInt64 18446744073709551616 := IsCharP.mk' _ _
   (ofNat_eq_zero_iff := fun x => by
@@ -255,7 +310,10 @@ example : ToInt.Sub UInt64 (.uint 64) := inferInstance
 
 instance : ToInt.Pow UInt64 (.uint 64) := ToInt.pow_of_semiring (by simp)
 
+attribute [local instance] USize.natCast USize.intCast in
 instance : CommRing USize where
+  nsmul := ⟨(· * ·)⟩
+  zsmul := ⟨(· * ·)⟩
   add_assoc := USize.add_assoc
   add_comm := USize.add_comm
   add_zero := USize.add_zero
@@ -274,6 +332,8 @@ instance : CommRing USize where
   ofNat_succ x := USize.ofNat_add x 1
   intCast_neg := USize.ofInt_neg
   intCast_ofNat := USize.intCast_ofNat
+  neg_zsmul i a := by simp [USize.intCast_neg, USize.neg_mul]
+  zsmul_natCast_eq_nsmul n a := congrArg (· * a) (USize.intCast_ofNat _)
 
 open System.Platform
 

src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean

@@ -25,7 +25,7 @@ where
     if k == 1 then
       return (← getStruct).vars[x]!
     else
-      return mkApp2 (← getStruct).hmulFn (mkIntLit k) (← getStruct).vars[x]!
+      return mkApp2 (← getStruct).zsmulFn (mkIntLit k) (← getStruct).vars[x]!
 
   go (p : Poly) (acc : Expr) : M Expr := do
     match p with
@@ -40,8 +40,8 @@ where
   | .var x => return (← getStruct).vars[x]!
   | .add a b => return mkApp2 (← getStruct).addFn (← go a) (← go b)
   | .sub a b => return mkApp2 (← getStruct).subFn (← go a) (← go b)
-  | .natMul k a => return mkApp2 (← getStruct).hmulNatFn (mkNatLit k) (← go a)
-  | .intMul k a => return mkApp2 (← getStruct).hmulFn (mkIntLit k) (← go a)
+  | .natMul k a => return mkApp2 (← getStruct).nsmulFn (mkNatLit k) (← go a)
+  | .intMul k a => return mkApp2 (← getStruct).zsmulFn (mkIntLit k) (← go a)
   | .neg a => return mkApp (← getStruct).negFn (← go a)
 
 private def mkEq (a b : Expr) : M Expr := do
@@ -64,12 +64,12 @@ def EqCnstr.denoteExpr (c : EqCnstr) : M Expr := do
   mkEq (← c.p.denoteExpr) (← getStruct).ofNatZero
 
 private def denoteNum (k : Int) : LinearM Expr := do
-  return mkApp2 (← getStruct).hmulFn (mkIntLit k) (← getOne)
+  return mkApp2 (← getStruct).zsmulFn (mkIntLit k) (← getOne)
 
 def _root_.Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Grind.CommRing.Poly) : LinearM Expr := do
   match p with
   | .num k => denoteNum k
-  | .add k m p => return mkApp2 (← getStruct).addFn (mkApp2 (← getStruct).hmulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p)
+  | .add k m p => return mkApp2 (← getStruct).addFn (mkApp2 (← getStruct).zsmulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p)
 
 def _root_.Lean.Grind.CommRing.Poly.toIntModuleExpr (p : Grind.CommRing.Poly) (generation := 0) : LinearM Expr := do
   let e ← p.denoteAsIntModuleExpr

src/Lean/Meta/Tactic/Grind/Arith/Linear/Internalize.lean

@@ -51,7 +51,7 @@ partial def markVars (e : Expr) : LinearM Unit := do
     if isAddInst (← getStruct) i then markVars a; markVars b else markVar e
   | HSub.hSub _ _ _ i a b => if isSubInst (← getStruct) i then markVars a; markVars b else markVar e
   | HMul.hMul _ _ _ i a b =>
-    if isHMulInst (← getStruct) i then
+    if isHMulIntInst (← getStruct) i then
       if (← getIntValue? a).isSome then
         return (← markVar b)
     if isHMulNatInst (← getStruct) i then
@@ -67,7 +67,7 @@ partial def markVars (e : Expr) : LinearM Unit := do
         return
     markVar e
   | HSMul.hSMul _ _ _ i a b =>
-    if isHSMulInst (← getStruct) i then
+    if isHSMulIntInst (← getStruct) i then
       if (← getIntValue? a).isSome then
         return (← markVar b)
     if isHSMulNatInst (← getStruct) i then

src/Lean/Meta/Tactic/Grind/Arith/Linear/Reify.lean

@@ -13,16 +13,16 @@ def isAddInst (struct : Struct) (inst : Expr) : Bool :=
   isSameExpr struct.addFn.appArg! inst
 def isZeroInst (struct : Struct) (inst : Expr) : Bool :=
   isSameExpr struct.zero.appArg! inst
-def isHMulInst (struct : Struct) (inst : Expr) : Bool :=
-  isSameExpr struct.hmulFn.appArg! inst
+def isHMulIntInst (struct : Struct) (inst : Expr) : Bool :=
+  isSameExpr struct.zsmulFn.appArg! inst
 def isHMulNatInst (struct : Struct) (inst : Expr) : Bool :=
-  isSameExpr struct.hmulNatFn.appArg! inst
+  isSameExpr struct.nsmulFn.appArg! inst
 def isHomoMulInst (struct : Struct) (inst : Expr) : Bool :=
   if let some homomulFn := struct.homomulFn? then isSameExpr homomulFn inst else false
-def isHSMulInst (struct : Struct) (inst : Expr) : Bool :=
-  if let some smulFn := struct.hsmulFn? then isSameExpr smulFn.appArg! inst else false
+def isHSMulIntInst (struct : Struct) (inst : Expr) : Bool :=
+  if let some smulFn := struct.zsmulFn? then isSameExpr smulFn.appArg! inst else false
 def isHSMulNatInst (struct : Struct) (inst : Expr) : Bool :=
-  if let some smulFn := struct.hsmulNatFn? then isSameExpr smulFn.appArg! inst else false
+  if let some smulFn := struct.nsmulFn? then isSameExpr smulFn.appArg! inst else false
 def isSubInst (struct : Struct) (inst : Expr) : Bool :=
   isSameExpr struct.subFn.appArg! inst
 def isNegInst (struct : Struct) (inst : Expr) : Bool :=
@@ -75,7 +75,7 @@ where
   isOfNatZero (e : Expr) : LinearM Bool := do
     withDefault <| isDefEq e (← getStruct).ofNatZero
   processHMul (i a b : Expr) : LinearM (Option LinExpr) := do
-    if isHMulInst (← getStruct) i then
+    if isHMulIntInst (← getStruct) i then
       let some k ← getIntValue? a | return none
       return some (.intMul k (← go b))
     else if isHMulNatInst (← getStruct) i then
@@ -83,7 +83,7 @@ where
       return some (.natMul k (← go b))
     return none
   processHSMul (i a b : Expr) : LinearM (Option LinExpr) := do
-    if isHSMulInst (← getStruct) i then
+    if isHSMulIntInst (← getStruct) i then
       let some k ← getIntValue? a | return none
       return some (.intMul k (← go b))
     else if isHSMulNatInst (← getStruct) i then

src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean

@@ -87,7 +87,7 @@ where
       let .some inst ← trySynthInstance instType
         | throwError "`grind linarith` failed to find instance{indentExpr instType}"
       return inst
-    let rec getHMulInst : GoalM Expr := do
+    let rec getHMulIntInst : GoalM Expr := do
       let instType := mkApp3 (mkConst ``HMul [0, u, u]) Int.mkType type type
       let .some inst ← trySynthInstance instType
         | throwError "`grind linarith` failed to find instance{indentExpr instType}"
@@ -113,6 +113,8 @@ where
       let heteroToField := mkApp2 (mkConst toHeteroName [u]) type toField
       ensureDefEq parentInst heteroToField
     let some intModuleInst ← getInst? ``Grind.IntModule | return none
+    let addCommGroupInst ← getInst ``Grind.AddCommGroup
+    let addCommMonoidInst ← getInst ``Grind.AddCommMonoid
     let zeroInst ← getInst ``Zero
     let zero ← internalizeConst <| mkApp2 (mkConst ``Zero.zero [u]) type zeroInst
     let ofNatZeroType := mkApp2 (mkConst ``OfNat [u]) type (mkRawNatLit 0)
@@ -126,16 +128,18 @@ where
     let subFn ← internalizeFn <| mkApp4 (mkConst ``HSub.hSub [u, u, u]) type type type subInst
     let negInst ← getInst ``Neg
     let negFn ← internalizeFn <| mkApp2 (mkConst ``Neg.neg [u]) type negInst
-    let hmulInst ← getHMulInst
-    let hmulFn ← internalizeFn <| mkApp4 (mkConst ``HMul.hMul [0, u, u]) Int.mkType type type hmulInst
-    let hmulNatInst ← getHMulNatInst
-    let hmulNatFn ← internalizeFn <| mkApp4 (mkConst ``HMul.hMul [0, u, u]) Nat.mkType type type hmulNatInst
-    ensureToFieldDefEq zeroInst intModuleInst ``Grind.IntModule.toZero
-    ensureToHomoFieldDefEq addInst intModuleInst ``Grind.IntModule.toAdd ``instHAdd
-    ensureToHomoFieldDefEq subInst intModuleInst ``Grind.IntModule.toSub ``instHSub
-    ensureToFieldDefEq negInst intModuleInst ``Grind.IntModule.toNeg
-    ensureToFieldDefEq hmulInst intModuleInst ``Grind.IntModule.hmulInt
-    ensureToFieldDefEq hmulNatInst intModuleInst ``Grind.IntModule.hmulNat
+    let zsmulInst ← getHMulIntInst
+    let zsmulFn ← internalizeFn <| mkApp4 (mkConst ``HMul.hMul [0, u, u]) Int.mkType type type zsmulInst
+    let nsmulInst ← getHMulNatInst
+    let nsmulFn ← internalizeFn <| mkApp4 (mkConst ``HMul.hMul [0, u, u]) Nat.mkType type type nsmulInst
+    ensureToFieldDefEq addCommGroupInst intModuleInst ``Grind.IntModule.toAddCommGroup
+    ensureToFieldDefEq addCommMonoidInst addCommGroupInst ``Grind.AddCommGroup.toAddCommMonoid
+    ensureToFieldDefEq zeroInst addCommMonoidInst ``Grind.AddCommMonoid.toZero
+    ensureToHomoFieldDefEq addInst addCommMonoidInst ``Grind.AddCommMonoid.toAdd ``instHAdd
+    ensureToHomoFieldDefEq subInst addCommGroupInst ``Grind.AddCommGroup.toSub ``instHSub
+    ensureToFieldDefEq negInst addCommGroupInst ``Grind.AddCommGroup.toNeg
+    ensureToFieldDefEq zsmulInst intModuleInst ``Grind.IntModule.zsmul
+    ensureToFieldDefEq nsmulInst intModuleInst ``Grind.IntModule.nsmul
     let preorderInst? ← getInst? ``Grind.Preorder
     let orderedAddInst? ← if let some preorderInst := preorderInst? then
       let isOrderedType := mkApp3 (mkConst ``Grind.OrderedAdd [u]) type addInst preorderInst
@@ -163,8 +167,8 @@ where
       let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Nat.mkType type type
       let .some smulInst ← trySynthInstance smulType | return none
       internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Nat.mkType type smulInst smulInst
-    let hsmulFn? ← getHSMulFn?
-    let hsmulNatFn? ← getHSMulNatFn?
+    let zsmulFn? ← getHSMulFn?
+    let nsmulFn? ← getHSMulNatFn?
     let ringId? ← CommRing.getRingId? type
     let semiringInst? ← getInst? ``Grind.Semiring
     let ringInst? ← getInst? ``Grind.Ring
@@ -201,7 +205,7 @@ where
     let id := (← get').structs.size
     let struct : Struct := {
       id, type, u, intModuleInst, preorderInst?, orderedAddInst?, partialInst?, linearInst?, noNatDivInst?
-      leFn?, ltFn?, addFn, subFn, negFn, hmulFn, hmulNatFn, hsmulFn?, hsmulNatFn?, zero, one?
+      leFn?, ltFn?, addFn, subFn, negFn, zsmulFn, nsmulFn, zsmulFn?, nsmulFn?, zero, one?
       ringInst?, commRingInst?, orderedRingInst?, charInst?, ringId?, fieldInst?, ofNatZero, homomulFn?
     }
     modify' fun s => { s with structs := s.structs.push struct }

src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean

@@ -119,10 +119,10 @@ structure Struct where
   leFn?            : Option Expr
   ltFn?            : Option Expr
   addFn            : Expr
-  hmulFn           : Expr
-  hmulNatFn        : Expr
-  hsmulFn?         : Option Expr
-  hsmulNatFn?      : Option Expr
+  zsmulFn          : Expr
+  nsmulFn          : Expr
+  zsmulFn?         : Option Expr
+  nsmulFn?         : Option Expr
   homomulFn?       : Option Expr -- homogeneous multiplication if structure is a ring
   subFn            : Expr
   negFn            : Expr

tests/lean/grind/algebra/nat_mod.lean

@@ -0,0 +1,20 @@
+-- I'll start collecting particularly horrific examples
+-- involving `Nat` modulo and div with variable denominators.
+
+example (a b n : Nat) (ha : a < n) : (n - a) * b % n = (n - a * b % n) % n := by
+  rw [Nat.sub_mul]
+  rw [Nat.mod_eq_mod_iff]
+  match b with
+  | 0 => refine ⟨1, 0, by simp⟩
+  | b+1 =>
+    refine ⟨a*(b+1)/n, b, ?_⟩
+    rw [Nat.mod_def, Nat.mul_add_one, Nat.mul_comm _ n, Nat.mul_comm b n]
+    have : n * (a * (b + 1) / n) ≤ a * (b + 1) := Nat.mul_div_le (a * (b + 1)) n
+    have := Nat.lt_mul_div_succ (a * (b + 1)) (show 0 < n by omega)
+    rw [Nat.mul_add_one n] at this
+    have : a * (b + 1) ≤ n * b + n := by
+      rw [Nat.mul_add_one]
+      have := Nat.mul_le_mul_right b ha
+      rw [Nat.succ_mul] at this
+      omega
+    omega

tests/lean/run/async_base_functions.lean

@@ -5,7 +5,7 @@ open Std
 
 open Std.Internal.IO.Async
 
-def wait (ms : Nat) (ref : Std.Mutex Nat) (val : Nat) : Async Unit := do
+def wait (ms : UInt32) (ref : Std.Mutex Nat) (val : Nat) : Async Unit := do
   ref.atomically (·.modify (· * val))
   IO.sleep ms
   ref.atomically (·.modify (· + val))

tests/lean/run/infoFromFailure.lean

@@ -16,7 +16,7 @@ info: B.foo "hello" : String × String
 ---
 trace: [Meta.synthInstance] ❌️ Add String
   [Meta.synthInstance] new goal Add String
-    [Meta.synthInstance.instances] #[@Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd, @Lean.Grind.Semiring.toAdd]
+    [Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
   [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
     [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
     [Meta.synthInstance] new goal Lean.Grind.Semiring String
@@ -39,20 +39,30 @@ trace: [Meta.synthInstance] ❌️ Add String
       [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing]
   [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring String ≟ Lean.Grind.Ring String
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add String
-    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
-    [Meta.synthInstance] new goal Lean.Grind.IntModule String
-      [Meta.synthInstance.instances] #[@Lean.Grind.Ring.instIntModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.instIntModule to Lean.Grind.IntModule String
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add String
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add String
     [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
+    [Meta.synthInstance] new goal Lean.Grind.AddCommMonoid String
+      [Meta.synthInstance.instances] #[@Lean.Grind.AddCommGroup.toAddCommMonoid, @Lean.Grind.NatModule.toAddCommMonoid]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid String ≟ Lean.Grind.AddCommMonoid String
     [Meta.synthInstance] new goal Lean.Grind.NatModule String
-      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.instNatModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.instNatModule to Lean.Grind.NatModule String
+      [Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.toNatModule]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
-  [Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
+    [Meta.synthInstance] new goal Lean.Grind.IntModule String
+      [Meta.synthInstance.instances] #[@Lean.Grind.Ring.toIntModule]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid String ≟ Lean.Grind.AddCommMonoid String
+    [Meta.synthInstance] new goal Lean.Grind.AddCommGroup String
+      [Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toAddCommGroup, @Lean.Grind.Ring.toAddCommGroup]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup String ≟ Lean.Grind.AddCommGroup String
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup String ≟ Lean.Grind.AddCommGroup String
   [Meta.synthInstance] result <not-available>
 -/
 #guard_msgs in
@@ -63,7 +73,7 @@ trace: [Meta.synthInstance] ❌️ Add String
 /--
 trace: [Meta.synthInstance] ❌️ Add Bool
   [Meta.synthInstance] new goal Add Bool
-    [Meta.synthInstance.instances] #[@Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd, @Lean.Grind.Semiring.toAdd]
+    [Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
   [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
     [Meta.synthInstance] new goal Lean.Grind.Semiring Bool
@@ -86,20 +96,30 @@ trace: [Meta.synthInstance] ❌️ Add Bool
       [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing]
   [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring Bool ≟ Lean.Grind.Ring Bool
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAdd to Add Bool
-    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
-    [Meta.synthInstance] new goal Lean.Grind.IntModule Bool
-      [Meta.synthInstance.instances] #[@Lean.Grind.Ring.instIntModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.instIntModule to Lean.Grind.IntModule Bool
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add Bool
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
+    [Meta.synthInstance] new goal Lean.Grind.AddCommMonoid Bool
+      [Meta.synthInstance.instances] #[@Lean.Grind.AddCommGroup.toAddCommMonoid, @Lean.Grind.NatModule.toAddCommMonoid]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid Bool ≟ Lean.Grind.AddCommMonoid Bool
     [Meta.synthInstance] new goal Lean.Grind.NatModule Bool
-      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.instNatModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.instNatModule to Lean.Grind.NatModule Bool
+      [Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.toNatModule]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
-  [Meta.synthInstance] ✅️ apply Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
+    [Meta.synthInstance] new goal Lean.Grind.IntModule Bool
+      [Meta.synthInstance.instances] #[@Lean.Grind.Ring.toIntModule]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid Bool ≟ Lean.Grind.AddCommMonoid Bool
+    [Meta.synthInstance] new goal Lean.Grind.AddCommGroup Bool
+      [Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toAddCommGroup, @Lean.Grind.Ring.toAddCommGroup]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup Bool ≟ Lean.Grind.AddCommGroup Bool
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup Bool ≟ Lean.Grind.AddCommGroup Bool
   [Meta.synthInstance] result <not-available>
 -/
 #guard_msgs in

tests/lean/run/lossy_casts.lean

@@ -0,0 +1,61 @@
+import Std
+/-!
+Ensure that we have not created lossy cast instances.
+-/
+
+/--
+error: type mismatch
+  x
+has type
+  Nat
+but is expected to have type
+  Fin 8
+-/
+#guard_msgs in
+example (x : Nat) : Fin 8 := x
+
+/--
+error: type mismatch
+  x
+has type
+  Nat
+but is expected to have type
+  UInt8
+-/
+#guard_msgs in
+example (x : Nat) : UInt8 := x
+
+/--
+error: type mismatch
+  x
+has type
+  Nat
+but is expected to have type
+  USize
+-/
+#guard_msgs in
+example (x : Nat) : USize := x
+
+/--
+error: type mismatch
+  x
+has type
+  Nat
+but is expected to have type
+  Int8
+-/
+#guard_msgs in
+example (x : Nat) : Int8 := x
+
+/--
+error: type mismatch
+  x
+has type
+  Nat
+but is expected to have type
+  ISize
+-/
+#guard_msgs in
+example (x : Nat) : ISize := x
+
+-- TODO: currently there is a global lossy instance `NatCast (BitVec w)`, that should be removed.