fix: auto-introduce in sym => mode when goal closes during preprocessing

This PR fixes a bug in `sym =>` interactive mode where satellite solvers
(`lia`, `ring`, `linarith`) would throw an internal error if their automatic
`intros + assertAll` preprocessing step already closed the goal. Previously,
`evalCheck` used `liftAction` which discarded the closure result, so the
subsequent `liftGoalM` call failed due to the absence of a main goal.
`liftAction` is now split so the caller can distinguish the closed and
subgoals cases and skip the solver body when preprocessing already finished
the job.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -329,13 +329,19 @@ def liftGoalM (k : GoalM α) : GrindTacticM α := do
   replaceMainGoal [goal]
   return a
 
-def liftAction (a : Action) : GrindTacticM Unit := do
+inductive LiftActionCoreResult where
+  | closed | subgoals
+
+def liftActionCore (a : Action) : GrindTacticM LiftActionCoreResult := do
   let goal ← getMainGoal
   let ka := fun _ => throwError "tactic is not applicable"
   let kp := fun goal => return .stuck [goal]
   match (← liftGrindM <| a goal ka kp) with
-  | .closed _ => replaceMainGoal []
-  | .stuck gs => replaceMainGoal gs
+  | .closed _ => replaceMainGoal []; return .closed
+  | .stuck gs => replaceMainGoal gs; return .subgoals
+
+def liftAction (a : Action) : GrindTacticM Unit := do
+  discard <| liftActionCore a
 
 def done : GrindTacticM Unit := do
   pruneSolvedGoals

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -111,7 +111,9 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
      This matches the behavior of these tactics in default tactic mode
      where `lia` can close `x > 1 → x + y + z > 0` directly. -/
   if (← read).sym then
-    liftAction <| Action.intros 0 >> Action.assertAll
+    match (← liftActionCore <| Action.intros 0 >> Action.assertAll) with
+    | .closed   => return () -- closed the goal
+    | .subgoals => pure () -- continue
   let recover := (← read).recover
   liftGoalM do
     let progress ← k

tests/elab/sym_interactive_bugs.lean

@@ -0,0 +1,16 @@
+
+example (p q : Prop) : p → q → p ∧ q := by
+  sym =>
+    intro hp hq
+    apply And.intro
+    apply hp
+    apply hq
+
+register_sym_simp chainSimp where
+  post := ground >> rewrite [Nat.add_zero, Nat.zero_add]
+
+example (x y : Nat) (h : x ≤ y) : (1 - 1) + x  ≤ y + (1 + 0) := by
+  sym =>
+    simp chainSimp
+    -- In the following tactic the goal is closed while preprocessing the target
+    lia