`split` tactic introduces useless hypothesis

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

First example:

example {n : Nat} : (match n with | 0 => 1 | n + 1 => n + 1) = n + 1 := by
  split

here we get the goals

n✝ : Nat
⊢ 1 = 0 + 1


n✝¹ n✝ : Nat
⊢ n✝ + 1 = n✝.succ + 1

but it would be nicer if this was

⊢ 1 = 0 + 1


n✝ : Nat
⊢ n✝ + 1 = n✝.succ + 1

Second example:

example : (fun foo => match foo with | 0 => 1 | n + 1 => n + 2) = (fun bar => bar + 1) := by
  ext baz
  split

here we get the goals

foo✝ : Nat
⊢ 1 = 0 + 1


foo✝ n✝ : Nat
⊢ n✝ + 2 = n✝.succ + 1

but it would be nicer if this was

⊢ 1 = 0 + 1


n✝ : Nat
⊢ n✝ + 2 = n✝.succ + 1

Versions

4.21.0-nightly-2025-05-12 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.

No source file or test entry point is named. Start by running the two minimal examples against the Lean nightly version to confirm the extra hypotheses, then locate the implementation and tests for the split tactic. Done means both examples produce only the necessary hypotheses while preserving their stated goals.