fix: prune goals assigned by isDefEq in sym => mode

This PR fixes a bug in `sym =>` interactive mode where goals whose
metavariable was assigned by `isDefEq` (e.g. via `apply Eq.refl`) were
not pruned. `pruneSolvedGoals` previously only filtered out goals
flagged as inconsistent, so an already-assigned goal would linger as an
unsolved goal. It now also removes goals whose metavariable is already
assigned.

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

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

@@ -68,7 +68,10 @@ def setGoals (goals : List Goal) : GrindTacticM Unit :=
 
 def pruneSolvedGoals : GrindTacticM Unit := do
   let gs ← getGoals
-  let gs := gs.filter fun g => !g.inconsistent
+  let gs ← gs.filterM fun g => do
+    if g.inconsistent then return false
+    -- The metavariable may have been assigned by `isDefEq`
+    return !(← g.mvarId.isAssigned)
   setGoals gs
 
 def getUnsolvedGoals : GrindTacticM (List Goal) := do

tests/elab/sym_interactive_bugs.lean

@@ -14,3 +14,8 @@ example (x y : Nat) (h : x ≤ y) : (1 - 1) + x  ≤ y + (1 + 0) := by
     simp chainSimp
     -- In the following tactic the goal is closed while preprocessing the target
     lia
+
+example : ∃ x, x = a := by
+  sym =>
+    apply Exists.intro
+    apply Eq.refl