diff --git a/src/Init/Grind/Module/Basic.lean b/src/Init/Grind/Module/Basic.lean
index 9ba285283b..d0352a7182 100644
--- a/src/Init/Grind/Module/Basic.lean
+++ b/src/Init/Grind/Module/Basic.lean
@@ -255,7 +255,7 @@ For a module over the integers this is equivalent to
 (See the alternative constructor `NoNatZeroDivisors.mk'`,
 and the theorem `eq_zero_of_mul_eq_zero`.)
 -/
-class NoNatZeroDivisors (α : Type u) [HMul Nat α α] where
+class NoNatZeroDivisors (α : Type u) [NatModule α] where
   /-- If `k * a ≠ k * b` then `k ≠ 0` or `a ≠ b`.-/
   no_nat_zero_divisors : ∀ (k : Nat) (a b : α), k ≠ 0 → k * a = k * b → a = b
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean b/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean
index aaacc95af5..08ec0ee2c2 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Insts.lean
@@ -18,9 +18,9 @@ def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : GoalM (Opti
   return some (charInst, n)
 
 def getNoZeroDivInst? (u : Level) (type : Expr) : GoalM (Option Expr) := do
-  let hmulType := mkApp3 (mkConst ``HMul [0, u, u]) (mkConst ``Nat []) type type
-  let some hmulInst ← synthInstance? hmulType | return none
-  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst
+  let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
+  let some natModuleInst ← synthInstance? natModuleType | return none
+  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
   synthInstance? noZeroDivType
 
 end Lean.Meta.Grind.Arith
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
index 748f7bec87..7013bcf63e 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
@@ -103,9 +103,9 @@ private def mkOrderedRingInst? (u : Level) (type : Expr) (semiringInst? preorder
   return some inst
 
 private def mkNoNatZeroDivInst? (u : Level) (type : Expr) : GoalM (Option Expr) := do
-  let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type
-  let some hmulInst ← synthInstance? hmulNat | return none
-  synthInstance? <| mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst
+  let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
+  let some natModuleInst ← synthInstance? natModuleType | return none
+  synthInstance? <| mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
 
 def getStructId? (type : Expr) : GoalM (Option Nat) := do
   unless (← getConfig).linarith do return none