fix: stuck "Missing alternative name" with incremental processing (#10848)

This PR fixes an issue where adding a missing case name after the pipe
in `induction` would not remove the now-obsolete error message.

Fixes #10847

Author: Kha

src/Lean/Elab/Tactic/Induction.lean

@@ -397,6 +397,7 @@ where
 
     -- `checkAltNames` may have looked at arbitrary alternatives, so we need to disable incremental
     -- processing of alternatives if it had any effect lest we end up with stale messages
+    let tacSnaps := if (← MonadLog.hasErrors) then #[] else tacSnaps
     Term.withoutTacticIncrementality (cond := (← MonadLog.hasErrors)) do
 
     let mut alts := alts

tests/lean/interactive/incrementalCombinator.lean

@@ -87,3 +87,15 @@ example (n : Nat) : n = n := by
   | one => simp
   | succ => simp
 --^ collectDiagnostics
+
+/-!
+"Missing alternative name" should not stick around.
+-/
+-- RESET
+example (n : Nat) : n = n := by
+  induction n with
+  | zero => simp
+  |  -- insert here
+  --^ sync
+  --^ insert: "succ => sorry"
+  --^ collectDiagnostics

tests/lean/interactive/incrementalCombinator.lean.expected.out

@@ -87,3 +87,13 @@ i 1.5
    "fullRange":
    {"start": {"line": 1, "character": 0},
     "end": {"line": 6, "character": 18}}}]}
+{"version": 2,
+ "uri": "file:///incrementalCombinator.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 2,
+   "range":
+   {"start": {"line": 1, "character": 0}, "end": {"line": 1, "character": 7}},
+   "message": "declaration uses 'sorry'",
+   "fullRange":
+   {"start": {"line": 1, "character": 0}, "end": {"line": 1, "character": 7}}}]}