chore: parameterize NoNatZeroDivisors by NatModule instead of HMul (#9527)

This PR changes `Lean.Grind.NoNatZeroDivisors` so that it is
parametrised by a `NatModule` instance rather than just a `HMul`
instance. This is sufficiently general for our purposes, and is a
band-aid (~40% improvement) for the performance problems we've been
seeing coming from inference here. The problems observed in Mathlib may
not see much improvement, however.

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
 

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

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