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

@@ -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

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.

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