diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index a96e1079a8..30459f2a1a 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/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
diff --git a/tests/lean/interactive/incrementalInduction.lean b/tests/lean/interactive/incrementalInduction.lean
index 75cbb75a20..6e33328a46 100644
--- a/tests/lean/interactive/incrementalInduction.lean
+++ b/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
diff --git a/tests/lean/interactive/incrementalInduction.lean.expected.out b/tests/lean/interactive/incrementalInduction.lean.expected.out
index 3531b214f3..f38e0c39d8 100644
--- a/tests/lean/interactive/incrementalInduction.lean.expected.out
+++ b/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}}}]}