fix: make sure "dependent elimination failed" error is on cases (#9551)

This PR fixes the error position for the "dependent elimination failed"
error for the `cases` tactic.

src/Lean/Elab/Tactic/Induction.lean

@@ -372,7 +372,7 @@ where
     goWithIncremental #[]
 
   -- continuation in the correct incrementality context
-  goWithIncremental (tacSnaps : Array (SnapshotBundle TacticParsedSnapshot)) := do
+  goWithIncremental (tacSnaps : Array (SnapshotBundle TacticParsedSnapshot)) := withRef tacStx do
     let hasAlts := altStxs?.isSome
     let altStxs := altStxs?.getD #[]
     let mut alts := alts

tests/lean/interactive/incrementalInduction.lean

@@ -70,3 +70,11 @@ theorem cases (n : Nat) : True := by
     dbg_trace "c 2"
                 --^ sync
                 --^ insert: ".5"
+
+-- RESET
+/-!
+Regression test: make sure the dependent elimination error appears on `cases`
+-/
+example (f : Nat → Nat) (n : Nat) (h : f n = n) := by
+  cases h
+  --^ collectDiagnostics

tests/lean/interactive/incrementalInduction.lean.expected.out

@@ -37,3 +37,14 @@ c 2
 c 1.5
 c 2
 c 2.5
+{"version": 1,
+ "uri": "file:///incrementalInduction.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 7}},
+   "message":
+   "dependent elimination failed, failed to solve equation\n  n = f n",
+   "fullRange":
+   {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 7}}}]}