From d9c3bbf1b49b5ca33d1cce3d8d185a76969dfcd6 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 19 Mar 2026 14:52:16 +0100
Subject: [PATCH] fix: prevent `induction`/`cases` from swallowing diagnostics
 when `using` clause contains `by` (#12953)

This PR fixes an issue where the `induction` and `cases` tactics would
swallow diagnostics (such as unsolved goals errors) when the `using`
clause contains a nested tactic.

Closes #12815
---
 src/Lean/Elab/Tactic/Induction.lean   | 30 ++++++++++++++++++---------
 src/Lean/Meta/Tactic/Grind/Types.lean |  3 +++
 tests/elab/12815.lean                 | 16 ++++++++++++++
 3 files changed, 39 insertions(+), 10 deletions(-)
 create mode 100644 tests/elab/12815.lean

diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 95b086a551..cf59515d01 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -999,9 +999,13 @@ def evalInduction : Tactic := fun stx =>
   match expandInduction? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
-    let (targets, toTag) ← elabElimTargets stx[1].getSepArgs
-    let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := true)
-    let targets ← withMainContext <| addImplicitTargets elimInfo targets
+    -- Disable tactic incrementality during setup to prevent nested `by` blocks (e.g. in `using`)
+    -- from consuming the snapshot meant for `evalAlts`.
+    let (targets, toTag, elimInfo) ← Term.withoutTacticIncrementality true do
+      let (targets, toTag) ← elabElimTargets stx[1].getSepArgs
+      let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := true)
+      let targets ← withMainContext <| addImplicitTargets elimInfo targets
+      return (targets, toTag, elimInfo)
     evalInductionCore stx elimInfo targets toTag
 
 
@@ -1081,8 +1085,10 @@ def evalFunInduction : Tactic := fun stx =>
   match expandInduction? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
-    let (elimInfo, targets) ← elabFunTarget (cases := false) stx[1]
-    let targets ← generalizeTargets targets
+    let (elimInfo, targets) ← Term.withoutTacticIncrementality true do
+      let (elimInfo, targets) ← elabFunTarget (cases := false) stx[1]
+      let targets ← generalizeTargets targets
+      return (elimInfo, targets)
     evalInductionCore stx elimInfo targets
 
 /--
@@ -1122,9 +1128,11 @@ def evalCases : Tactic := fun stx =>
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
     -- syntax (name := cases) "cases " elimTarget,+ (" using " term)? (inductionAlts)? : tactic
-    let (targets, toTag) ← elabElimTargets stx[1].getSepArgs
-    let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := false)
-    let targets ← withMainContext <| addImplicitTargets elimInfo targets
+    let (targets, toTag, elimInfo) ← Term.withoutTacticIncrementality true do
+      let (targets, toTag) ← elabElimTargets stx[1].getSepArgs
+      let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := false)
+      let targets ← withMainContext <| addImplicitTargets elimInfo targets
+      return (targets, toTag, elimInfo)
     evalCasesCore stx elimInfo targets toTag
 
 @[builtin_tactic Lean.Parser.Tactic.funCases, builtin_incremental]
@@ -1132,8 +1140,10 @@ def evalFunCases : Tactic := fun stx =>
   match expandInduction? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
-    let (elimInfo, targets) ← elabFunTarget (cases := true) stx[1]
-    let targets ← generalizeTargets targets
+    let (elimInfo, targets) ← Term.withoutTacticIncrementality true do
+      let (elimInfo, targets) ← elabFunTarget (cases := true) stx[1]
+      let targets ← generalizeTargets targets
+      return (elimInfo, targets)
     evalCasesCore stx elimInfo targets
 
 builtin_initialize
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 5866646c69..7ec33cfa68 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -611,6 +611,9 @@ where
   go (a b : Expr) : Bool :=
     if a.isApp && b.isApp then
       hasSameRoot enodes a.appArg! b.appArg! && go a.appFn! b.appFn!
+    else if a.isApp || b.isApp then
+      -- Different number of arguments: not congruent.
+      false
     else
       -- Remark: we do not check whether the types of the functions are equal here
       -- because we are not in the `MetaM` monad.
diff --git a/tests/elab/12815.lean b/tests/elab/12815.lean
new file mode 100644
index 0000000000..253d00e3ea
--- /dev/null
+++ b/tests/elab/12815.lean
@@ -0,0 +1,16 @@
+/-! Diagnostics from induction alternatives must not be swallowed when the `using`
+clause contains a nested `by` tactic block. https://github.com/leanprover/lean4/issues/12815 -/
+
+axiom myElim (h : True) (P : Nat → Prop) (n : Nat)
+    (zero : P 0) (succ : ∀ n, P n → P (n + 1)) : P n
+
+/--
+error: unsolved goals
+case zero
+⊢ True
+-/
+#guard_msgs in
+theorem foo : True := by
+  induction 0 using myElim (by trivial) with
+  | zero => skip
+  | succ _ ih => exact ih