fix tests

src/Init/Grind/CommRing/Basic.lean

@@ -10,6 +10,7 @@ import Init.Data.Zero
 import Init.Data.Int.DivMod.Lemmas
 import Init.Data.Int.Pow
 import Init.TacticsExtra
+import Init.Grind.Module.Basic
 
 /-!
 # A monolithic commutative ring typeclass for internal use in `grind`.
@@ -108,6 +109,24 @@ theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂
   next => simp [pow_zero, mul_one]
   next k₂ ih => rw [Nat.add_succ, pow_succ, pow_succ, ih, mul_assoc]
 
+instance : NatModule α where
+  hMul a x := a * x
+  add_zero := by simp [add_zero]
+  zero_add := by simp [zero_add]
+  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]
+  mul_hmul := by simp [natCast_mul, mul_assoc]
+
+theorem hmul_eq_natCast_mul {α} [Semiring α] {k : Nat} {a : α} : HMul.hMul (α := Nat) k a = (k : α) * a := rfl
+
+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]
+
 end Semiring
 
 namespace Ring
@@ -243,6 +262,24 @@ 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
+  hMul a x := a * x
+  add_zero := by simp [add_zero]
+  zero_add := by simp [zero_add]
+  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]
+  mul_hmul := by simp [intCast_mul, mul_assoc]
+  neg_hmul := by simp [intCast_neg, neg_mul]
+  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
+
 end Ring
 
 namespace CommSemiring
@@ -347,14 +384,7 @@ theorem natCast_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) :
 
 end IsCharP
 
-/--
-Special case of Mathlib's `NoZeroSMulDivisors Nat α`.
--/
-class NoNatZeroDivisors (α : Type u) [Ring α] where
-  no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0
-
-export NoNatZeroDivisors (no_nat_zero_divisors)
-
+-- TODO: This should be generalizable to any `IntModule α`, not just `Ring α`.
 theorem no_int_zero_divisors {α : Type u} [Ring α] [NoNatZeroDivisors α] {k : Int} {a : α}
     : k ≠ 0 → k * a = 0 → a = 0 := by
   match k with
@@ -362,13 +392,12 @@ theorem no_int_zero_divisors {α : Type u} [Ring α] [NoNatZeroDivisors α] {k :
     simp [intCast_natCast]
     intro h₁ h₂
     replace h₁ : k ≠ 0 := by intro h; simp [h] at h₁
-    rw [← ofNat_eq_natCast] at h₂
     exact no_nat_zero_divisors k a h₁ h₂
   | -(k+1 : Nat) =>
     rw [Int.natCast_add, ← Int.natCast_add, intCast_neg, intCast_natCast]
     intro _ h
     replace h := congrArg (-·) h; simp at h
-    rw [← neg_mul, neg_neg, neg_zero, ← ofNat_eq_natCast] at h
+    rw [← neg_mul, neg_neg, neg_zero, ← hmul_eq_natCast_mul] at h
     exact no_nat_zero_divisors (k+1) a (Nat.succ_ne_zero _) h
 
 end Lean.Grind

src/Init/Grind/CommRing/Fin.lean

@@ -104,7 +104,11 @@ instance (n : Nat) [NeZero n] : CommRing (Fin n) where
   intCast_neg := Fin.intCast_neg
 
 instance (n : Nat) [NeZero n] : IsCharP (Fin n) n where
-  ofNat_eq_zero_iff x := by simp only [OfNat.ofNat, Fin.ofNat']; simp
+  ofNat_eq_zero_iff x := by
+    change Fin.ofNat' _ _ = Fin.ofNat' _ _ ↔ _
+    simp only [Fin.ofNat']
+    simp only [Nat.zero_mod]
+    simp only [Fin.mk.injEq]
 
 end Fin
 

src/Init/Grind/Module/Basic.lean

@@ -49,13 +49,6 @@ instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
     hmul_add := by simp [IntModule.hmul_add]
     mul_hmul := by simp [IntModule.mul_hmul] }
 
-/--
-We keep track of rational linear combinations as integer linear combinations,
-but with the assurance that we can cancel the GCD of the coefficients.
--/
-class RatModule (M : Type u) extends IntModule M where
-  no_int_zero_divisors : ∀ (k : Int) (a : M), k ≠ 0 → k * a = 0 → a = 0
-
 /-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
 class Preorder (α : Type u) extends LE α, LT α where
   le_refl : ∀ a : α, a ≤ a
@@ -73,4 +66,12 @@ class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
   hmul_nonneg : ∀ (k : Int) (a : M), 0 ≤ a → 0 ≤ k → 0 ≤ k * a
   hmul_nonpos : ∀ (k : Int) (a : M), a ≤ 0 → 0 ≤ k → k * a ≤ 0
 
+/--
+Special case of Mathlib's `NoZeroSMulDivisors Nat α`.
+-/
+class NoNatZeroDivisors (α : Type u) [Zero α] [HMul Nat α α] where
+  no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → k * a = 0 → a = 0
+
+export NoNatZeroDivisors (no_nat_zero_divisors)
+
 end Lean.Grind

src/Init/Grind/Module/Int.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Grind.Module.Basic
+import Init.Grind.CommRing.Int
 import Init.Omega
 
 /-!
@@ -15,21 +16,6 @@ import Init.Omega
 
 namespace Lean.Grind
 
-instance : IntModule Int where
-  add_zero := Int.add_zero
-  zero_add := Int.zero_add
-  add_comm := Int.add_comm
-  add_assoc := Int.add_assoc
-  zero_hmul := Int.zero_mul
-  one_hmul := Int.one_mul
-  add_hmul := Int.add_mul
-  neg_hmul := Int.neg_mul
-  hmul_zero := Int.mul_zero
-  hmul_add := Int.mul_add
-  mul_hmul := Int.mul_assoc
-  neg_add_cancel := Int.add_left_neg
-  sub_eq_add_neg _ _ := Int.sub_eq_add_neg
-
 instance : Preorder Int where
   le_refl := Int.le_refl
   le_trans _ _ _ := Int.le_trans

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean

@@ -111,8 +111,13 @@ where
         | trace_goal[grind.ring] "found instance for{indentExpr charType}\nbut characteristic is not a natural number"; pure none
       trace_goal[grind.ring] "characteristic: {n}"
       pure <| some (charInst, n)
-    let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type ringInst
-    let noZeroDivInst? := (← trySynthInstance noZeroDivType).toOption
+    let noZeroDivInst? ← withNewMCtxDepth do
+      let zeroType := mkApp (mkConst ``Zero [u]) type
+      let .some zeroInst ← trySynthInstance zeroType | return none
+      let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type
+      let .some hmulInst ← trySynthInstance hmulType | return none
+      let noZeroDivType := mkApp3 (mkConst ``Grind.NoNatZeroDivisors [u]) type zeroInst hmulInst
+      LOption.toOption <$> trySynthInstance noZeroDivType
     trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
     let addFn ← getAddFn type u semiringInst
     let mulFn ← getMulFn type u semiringInst

tests/lean/grind/module_normalization.lean

@@ -10,8 +10,8 @@ example (a b : R) : a + b = b + a := by grind
 example (a : R) : a + 0 = a := by grind
 example (a : R) : 0 + a = a := by grind
 example (a b c : R) : a + b + c = a + (b + c) := by grind
-example (a : R) : 2 • a = a + a := by grind
-example (a b : R) : 2 • (b + c) = c + 2 • b + c := by grind
+example (a : R) : 2 * a = a + a := by grind
+example (a b : R) : 2 * (b + c) = c + 2 * b + c := by grind
 
 end NatModule
 
@@ -23,10 +23,10 @@ example (a b : R) : a + b = b + a := by grind
 example (a : R) : a + 0 = a := by grind
 example (a : R) : 0 + a = a := by grind
 example (a b c : R) : a + b + c = a + (b + c) := by grind
-example (a : R) : 2 • a = a + a := by grind
-example (a : R) : (-2 : Int) • a = -a - a := by grind
-example (a b : R) : 2 • (b + c) = c + 2 • b + c := by grind
-example (a b c : R) : 2 • (b + c) - 3 • c + b + b = c + 5 • b - 2 • c := by grind
-example (a b c : R) : 2 • (b + c) + (-3 : Int) • c + b + b = c + (5 : Int) • b - 2 • c := by grind
+example (a : R) : 2 * a = a + a := by grind
+example (a : R) : (-2 : Int) * a = -a - a := by grind
+example (a b : R) : 2 * (b + c) = c + 2 * b + c := by grind
+example (a b c : R) : 2 * (b + c) - 3 * c + b + b = c + 5 * b - 2 * c := by grind
+example (a b c : R) : 2 * (b + c) + (-3 : Int) * c + b + b = c + (5 : Int) * b - 2 • c := by grind
 
 end IntModule

tests/lean/grind/module_relations.lean

@@ -8,20 +8,20 @@ variable (R : Type u) [IntModule R]
 
 -- In an `IntModule`, we should be able to handle relations
 -- this is harder, and less important, than being able to do this in `RatModule`.
-example (a b : R) (h : a + b = 0) : 3 • a - 7 • b = 9 • a + a := by grind
-example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - b + (-b) + a := by grind
+example (a b : R) (h : a + b = 0) : 3 * a - 7 * b = 9 * a + a := by grind
+example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - b + (-b) + a := by grind
 
 end IntModule
 
 section RatModule
 
-variable (R : Type u) [RatModule R]
+variable (R : Type u) [IntModule R] [NoNatZeroDivisors R]
 
-example (a b : R) (h : a + b = 0) : 3 • a - 7 • b = 9 • a + a := by grind
-example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - b + (-b) + a := by grind
+example (a b : R) (h : a + b = 0) : 3 * a - 7 * b = 9 * a + a := by grind
+example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - b + (-b) + a := by grind
 
 -- In a `RatModule` we can clear common divisors.
 example (a : R) (h : a + a = 0) : a = 0 := by grind
-example (a b c : R) (h : 2 • a + 2 • b = 4 • c) : 3 • a + c = 5 • c - 3 • b := by grind
+example (a b c : R) (h : 2 * a + 2 * b = 4 * c) : 3 * a + c = 5 * c - 3 * b := by grind
 
 end RatModule

tests/lean/grind/ordered_modules.lean

@@ -2,7 +2,7 @@ open Lean.Grind
 
 set_option grind.warning false
 
-variable (R : Type u) [RatModule R] [Preorder R] [IntModule.IsOrdered R]
+variable (R : Type u) [IntModule R] [NoNatZeroDivisors R] [Preorder R] [IntModule.IsOrdered R]
 
 example (a b c : R) (h : a < b) : a + c < b + c := by grind
 example (a b c : R) (h : a < b) : c + a < c + b := by grind
@@ -15,50 +15,50 @@ example (a b : R) (h : a ≤ b) : -b ≤ -a := by grind
 example (a b : R) (h : a ≤ b) : -a ≤ -b := by grind
 
 example (a : R) (h : 0 < a) : 0 ≤ a := by grind
-example (a : R) (h : 0 < a) : -2 • a < 0 := by grind
+example (a : R) (h : 0 < a) : -2 * a < 0 := by grind
 
 example (a b c : R) (_ : a ≤ b) (_ : b ≤ c) : a ≤ c := by grind
 example (a b c : R) (_ : a ≤ b) (_ : b < c) : a < c := by grind
 example (a b c : R) (_ : a < b) (_ : b ≤ c) : a < c := by grind
 example (a b c : R) (_ : a < b) (_ : b < c) : a < c := by grind
 
-example (a : R) (h : 2 • a < 0) : a < 0 := by grind
-example (a : R) (h : 2 • a < 0) : 0 ≤ -a := by grind
+example (a : R) (h : 2 * a < 0) : a < 0 := by grind
+example (a : R) (h : 2 * a < 0) : 0 ≤ -a := by grind
 
 example (a b : R) (_ : a < b) (_ : b < a) : False := by grind
 example (a b : R) (_ : a < b ∧ b < a) : False := by grind
 example (a b : R) (_ : a < b) : a ≠ b := by grind
 
-example (a b c e v0 v1 : R) (h1 : v0 = 5 • a) (h2 : v1 = 3 • b) (h3 : v0 + v1 + c = 10 • e) :
-    v0 + 5 • e + (v1 - 3 • e) + (c - 2 • e) = 10 • e := by
+example (a b c e v0 v1 : R) (h1 : v0 = 5 * a) (h2 : v1 = 3 * b) (h3 : v0 + v1 + c = 10 * e) :
+    v0 + 5 * e + (v1 - 3 * e) + (c - 2 * e) = 10 * e := by
   grind
 
 example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
   grind
-example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) (h3 : 12 • y - 4 • z < 0) : False := by
+example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
   grind
 
 example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) (h3 : 12 * y - 4 * z < 0) :
     False := by grind
-example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) (h3 : 12 • y - 4 • z < 0) :
+example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) :
     False := by grind
 
 example (x y z : Int) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3*y := by
   grind
-example (x y z : R) (hx : x ≤ 3 • y) (h2 : y ≤ 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
+example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
 
 example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) : ¬ 12*y - 4* z < 0 := by
   grind
-example (x y z : R) (h1 : 2 • x < 3 • y) (h2 : -4 • x + 2 • z < 0) : ¬ 12 • y - 4 • z < 0 := by
+example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12 * y - 4 * z < 0 := by
   grind
 
 example (x y z : Int) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
-example (x y z : R) (hx : ¬ x > 3 • y) (h2 : ¬ y > 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
+example (x y z : R) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
 
 example (x y z : Nat) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
-example (x y z : R) (hx : x ≤ 3 • y) (h2 : y ≤ 2 • z) (h3 : x ≥ 6 • z) : x = 3 • y := by
+example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind

tests/lean/run/infoFromFailure.lean

@@ -16,21 +16,7 @@ info: B.foo "hello" : String × String
 ---
 trace: [Meta.synthInstance] ❌️ Add String
   [Meta.synthInstance] new goal Add String
-    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd, @Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd]
-  [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.RatModule.toIntModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.RatModule.toIntModule to Lean.Grind.IntModule String
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
-    [Meta.synthInstance] no instances for Lean.Grind.RatModule String
-      [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add String
-    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
-    [Meta.synthInstance] new goal Lean.Grind.NatModule String
-      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule]
-  [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.instances] #[@Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.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
@@ -51,6 +37,20 @@ trace: [Meta.synthInstance] ❌️ Add String
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring String ≟ Lean.Grind.Ring String
     [Meta.synthInstance] no instances for Lean.Grind.CommRing String
       [Meta.synthInstance.instances] #[]
+  [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.tryResolve] ✅️ Add String ≟ Add 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.tryResolve] ✅️ Lean.Grind.NatModule String ≟ 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] result <not-available>
 -/
 #guard_msgs in
@@ -61,21 +61,7 @@ trace: [Meta.synthInstance] ❌️ Add String
 /--
 trace: [Meta.synthInstance] ❌️ Add Bool
   [Meta.synthInstance] new goal Add Bool
-    [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd, @Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.toAdd]
-  [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.RatModule.toIntModule]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.RatModule.toIntModule to Lean.Grind.IntModule Bool
-    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
-    [Meta.synthInstance] no instances for Lean.Grind.RatModule Bool
-      [Meta.synthInstance.instances] #[]
-  [Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAdd to Add Bool
-    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
-    [Meta.synthInstance] new goal Lean.Grind.NatModule Bool
-      [Meta.synthInstance.instances] #[Lean.Grind.IntModule.toNatModule]
-  [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.instances] #[@Lean.Grind.NatModule.toAdd, @Lean.Grind.IntModule.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
@@ -96,6 +82,20 @@ trace: [Meta.synthInstance] ❌️ Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring Bool ≟ Lean.Grind.Ring Bool
     [Meta.synthInstance] no instances for Lean.Grind.CommRing Bool
       [Meta.synthInstance.instances] #[]
+  [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.tryResolve] ✅️ Add Bool ≟ Add 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.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ 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] result <not-available>
 -/
 #guard_msgs in