diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean
index 00a7f62138..5678875312 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean
+++ b/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
diff --git a/tests/lean/run/grind_commsemiring.lean b/tests/lean/run/grind_commsemiring.lean
new file mode 100644
index 0000000000..5d2633f2e8
--- /dev/null
+++ b/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