From 98569c7cf02c236b6d25cb46b5c990aea3431c27 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 25 Jul 2025 12:02:42 -0700
Subject: [PATCH] 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                   |  2 +-
 tests/lean/interactive/incrementalInduction.lean      |  8 ++++++++
 .../incrementalInduction.lean.expected.out            | 11 +++++++++++
 3 files changed, 20 insertions(+), 1 deletion(-)

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}}}]}