`induction` tactic swallows IDE diagnostics

[TwoFX]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Here is some code:

namespace Nat

theorem base_induction {P : Nat → Prop} {n : Nat} (b : Nat) (hb : 1 < b) (single : ∀ m, m < b → P m)
    (digit : ∀ m k, k < b → P m → P (b * m + k)) : P n := by
  sorry

end Nat

theorem bar : 1 < 10 := by decide

theorem foo {n : Nat} : List.foldl (fun n c => n * 10 + (c.toNat - 48)) 0 (Nat.toDigits 10 n) = n := by
  induction n using Nat.base_induction 10 (by decide) with
  | single m hm =>
    skip
  | digit => sorry

When opening this code in VS Code or Lean 4 web, no diagnostics are shown on foo. Specifically, the unsolved goals error on the single arm of the induction is missing.

When you replace the by decide in the using clause of the induction by bar, then the error is shown as expected.

Also, when you replace the sorry in the digit arm by done, then both arms show an error as expected.

When compiling the code using lake build, the error is printed as expected.

Expected behavior: Unsolved goals error shows in the IDE

Actual behavior: Unsolved goals error is missing.

Versions

Lean 4.30.0-nightly-2026-03-05 on live.lean-lang.org

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.