fix: grind propagates 0 * a = 0 for CommSemiring (#11881)

This PR fixes an issue where `grind` failed to prove `f ≠ 0` from `f * r
≠ 0` when using `Lean.Grind.CommSemiring`, but succeeded with
`Lean.Grind.Semiring`.

The `propagateMul` propagator handles `0 * a = 0` and `a * 0 = 0` rules
for semirings that don't have full ring support in grind. Previously,
`CommSemiring` was excluded because it uses a ring envelope for
normalization, but that approach doesn't propagate these equalities back
to the original terms. Now `CommSemiring` also uses `propagateMul`.

Reported as
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Grind.20failure.20for.20CommSemiring.2C.20not.20Semiring

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean

@@ -82,7 +82,12 @@ See comment at `propagateMul`.
 private def isUnsupportedSemiring? (type : Expr) : GoalM (Option Expr) := do
   if isSupportedSemiringQuick type then return none
   if (← getCommRingId? type).isSome then return none
-  if (← getCommSemiringId? type).isSome then return none
+  if let some id ← getCommSemiringId? type then
+    -- CommSemiring also needs `propagateMul` because the ring envelope approach
+    -- does not propagate `0 * a = 0` back to original terms.
+    -- In the future, we want to add support for propagating equalities when the
+    -- `CommSemiring` implements `AddRightCancel`.
+    return some (← SemiringM.run id (return (← getSemiring).semiringInst))
   if let some id ← getNonCommRingId? type then
     let inst ← NonCommRingM.run id do return (← getRing).semiringInst
     return some inst

tests/lean/run/grind_commsemiring.lean

@@ -0,0 +1,35 @@
+/-!
+# Tests for grind with CommSemiring
+
+These tests verify that grind properly propagates `0 * a = 0` and `a * 0 = 0`
+for CommSemiring types, not just Semiring types.
+
+See: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Grind.20failure.20for.20CommSemiring.2C.20not.20Semiring
+-/
+
+-- Basic test with Semiring
+example {R : Type} [Lean.Grind.Semiring R] (f r : R) (hg : f * r ≠ 0) :
+    f ≠ 0 := by
+  grind
+
+-- Same test should also work with CommSemiring
+example {R : Type} [Lean.Grind.CommSemiring R] (f r : R) (hg : f * r ≠ 0) :
+    f ≠ 0 := by
+  grind
+
+-- Symmetric case: r * f ≠ 0 implies f ≠ 0
+example {R : Type} [Lean.Grind.CommSemiring R] (f r : R) (hg : r * f ≠ 0) :
+    f ≠ 0 := by
+  grind
+
+-- Both factors must be nonzero
+example {R : Type} [Lean.Grind.CommSemiring R] (f r : R) (hg : f * r ≠ 0) :
+    f ≠ 0 ∧ r ≠ 0 := by
+  grind
+
+-- mul_one and one_mul propagation
+example {R : Type} [Lean.Grind.CommSemiring R] (f g : R) (h1 : 1 * f = g) (h2 : g ≠ f) : False := by
+  grind
+
+example {R : Type} [Lean.Grind.CommSemiring R] (f g : R) (h1 : f * 1 = g) (h2 : g ≠ f) : False := by
+  grind