still failing, however

src/Init/Data/BitVec/Lemmas.lean

@@ -2173,10 +2173,10 @@ theorem toInt_append {x : BitVec n} {y : BitVec m} :
   simp only [toInt_append, toInt_zero, toNat_ofNat, Nat.zero_mod, Int.cast_ofNat_Int, Int.add_zero,
     ite_eq_right_iff]
   -- FIXME: fails because some definition is not exposed correctly. But which?
-  -- grind only [two_mul_toInt_lt, le_two_mul_toInt, = toInt_zero_length]
-  intros h
-  subst h
-  simp [BitVec.eq_nil x]
+  grind only [two_mul_toInt_lt, le_two_mul_toInt, = toInt_zero_length]
+  -- intros h
+  -- subst h
+  -- simp [BitVec.eq_nil x]
 
 @[simp, grind =] theorem toInt_zero_append {n m : Nat} {x : BitVec n} :
     (0#m ++ x).toInt = if m = 0 then x.toInt else x.toNat := by

src/Init/Grind/Ring/Poly.lean

@@ -18,6 +18,8 @@ namespace Lean.Grind
 -- These are no longer global instances, so we need to turn them on here.
 attribute [local instance] Semiring.natCast Ring.intCast
 namespace CommRing
+
+@[expose]
 abbrev Var := Nat
 
 inductive Expr where
@@ -56,7 +58,15 @@ def Expr.denote {α} [Ring α] (ctx : Context α) : Expr → α
 structure Power where
   x : Var
   k : Nat
-  deriving BEq, Repr, Inhabited, Hashable
+  deriving Repr, Inhabited, Hashable
+
+@[expose]
+def Power.beq : Power → Power → Bool
+  | ⟨x₁, k₁⟩, ⟨x₂, k₂⟩ => x₁ == x₂ && k₁ == k₂
+
+@[expose]
+instance : BEq Power where
+  beq := Power.beq
 
 instance : LawfulBEq Power where
   eq_of_beq {a} := by cases a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
@@ -77,7 +87,17 @@ def Power.denote {α} [Semiring α] (ctx : Context α) : Power → α
 inductive Mon where
   | unit
   | mult (p : Power) (m : Mon)
-  deriving BEq, Repr, Inhabited, Hashable
+  deriving Repr, Inhabited, Hashable
+
+@[expose]
+def Mon.beq : Mon → Mon → Bool
+  | .unit, .unit => true
+  | .mult p₁ m₁, .mult p₂ m₂ => p₁ == p₂ && beq m₁ m₂
+  | _, _ => false
+
+@[expose]
+instance : BEq Mon where
+  beq := Mon.beq
 
 instance : LawfulBEq Mon where
   eq_of_beq {a} := by
@@ -212,7 +232,17 @@ def Mon.grevlex (m₁ m₂ : Mon) : Ordering :=
 inductive Poly where
   | num (k : Int)
   | add (k : Int) (v : Mon) (p : Poly)
-  deriving BEq, Repr, Inhabited, Hashable
+  deriving Repr, Inhabited, Hashable
+
+@[expose]
+def Poly.beq : Poly → Poly → Bool
+    | .num k₁, .num k₂ => k₁ == k₂
+    | .add k₁ m₁ p₁, .add k₂ m₂ p₂ => k₁ == k₂ && m₁ == m₂ && beq p₁ p₂
+    | _, _ => false
+
+@[expose]
+instance : BEq Poly where
+  beq := Poly.beq
 
 instance : LawfulBEq Poly where
   eq_of_beq {a} := by

tests/lean/grind/algebra/module_normalization.lean

@@ -1,7 +1,8 @@
--- Tests for `grind` as a module normalization tactic, when only `NatModule`, `IntModule`, or `RatModule` is available.
+-- Tests for `grind` as a module normalization tactic, when only `NatModule` is available.
 
 open Lean.Grind
 
+-- We could solve these by embedding a `NatModule` into its `IntModule` completion.
 section NatModule
 
 variable (R : Type u) [NatModule R]
@@ -11,6 +12,6 @@ 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 (b c : R) : 2 * (b + c) = c + 2 * b + c := by grind
 
 end NatModule