fix: handle non-internalized terms in semiring reifier

This PR fixes a panic in `grind` where `sreifyCore?` could encounter
power subterms not yet internalized in the E-graph during nested
propagation. The ring reifier (`reifyCore?`) already had a defensive
`alreadyInternalized` check before creating variables, but the semiring
reifier (`sreifyCore?`) was missing this guard. When `propagatePower`
decomposed `a ^ (b₁ + b₂)` into `a^b₁ * a^b₂` and the resulting terms
triggered further propagation, the semiring reifier could be called on
subterms not yet in the E-graph, causing `markTerm` to fail.

Closes #12428

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean

@@ -137,11 +137,15 @@ variable [MonadLiftT GoalM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemi
 Similar to `reify?` but for `CommSemiring`
 -/
 partial def sreifyCore? (e : Expr) : m (Option SemiringExpr) := do
+  let mkVar (e : Expr) : m Var := do
+    unless (← alreadyInternalized e) do
+      internalize e 0
+    mkSVarCore e
   let toVar (e : Expr) : m SemiringExpr := do
-    return .var (← mkSVarCore e)
+    return .var (← mkVar e)
   let asVar (e : Expr) : m SemiringExpr := do
     reportSAppIssue e
-    return .var (← mkSVarCore e)
+    return .var (← mkVar e)
   let rec go (e : Expr) : m SemiringExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>

tests/lean/run/grind_12428.lean

@@ -0,0 +1,14 @@
+import Std.Do
+
+-- `grind` should not panic on this example (issue #12428).
+-- The bug was that `sreifyCore?` could encounter power subterms
+-- not yet internalized in the E-graph during nested propagation.
+example
+  (n x' y : Nat)
+  (pref : List Nat)
+  (cur : Nat)
+  (suff : List Nat)
+  (h : List.range' 0 n 1 = pref ++ cur :: suff) :
+  y ^ x' * n ^ x' = x' ^ n := by
+  fail_if_success grind
+  sorry