`split` fails with `let` declarations

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

split fails when the discriminant of a match being split is a let variable.

Context

Writing a definition with partial_fixpoint. Consider:

def test : Nat :=
  let a := 1
  match a with | 0 => test | k + 1 => 0
partial_fixpoint

Steps to Reproduce

/--
error: Tactic `split` failed: Could not split an `if` or `match` expression in the goal

a : Nat := 3
⊢ (match a with
    | 0 => 3
    | k.succ => 3) =
    3
---
trace: [split.failure] `split` tactic failed at
      match a with
      | 0 => 3
      | k.succ => 3
    Dependent elimination failed: Failed to solve equation
      a = 0
-/
#guard_msgs in
example : let a := 3; (match a with | 0 | k + 1 => 3) = 3 := by
  intro a
  set_option trace.split.failure true in
  split

Expected behavior: split produces a new state containing h : a = 0 or h : a = k.succ.

Actual behavior: split immediately tries to substitute the equation, resulting in the error.

Versions

Lean 4.31.0-nightly-2026-04-02

Impact

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

Start by running the minimal #guard_msgs reproduction and inspect the split tactic behavior with trace.split.failure enabled. The expected result is a state containing either h : a = 0 or h : a = k.succ, rather than immediate substitution and failure.