split fails with non-fvar discriminants and dependent motives

Consider this

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

n : Nat
⊢ Fin.last n =
    match id n with
    | 0 => Fin.last 0
    | n.succ => Fin.last (n + 1)
-/
#guard_msgs(pass trace, all) in
example (n : Nat) : Fin.last n = match (motive := ∀ n, Fin (n+1)) id n with
  | 0 => Fin.last 0
  | n + 1 => Fin.last (n + 1) := by
  split <;> rfl

it works if the discriminant id n were a simple variable n.

This seems to be the core issue of underlying #10195, and is blocking #10268 and similar constructions.

Versions

Lean 4.25.0-nightly-2025-09-16

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 reproducer in the issue with Lean 4.25.0-nightly-2025-09-16 and inspect the implementation of the split tactic and its handling of dependent motives. Done means the example's split <;> rfl succeeds for the non-variable discriminant while preserving the existing behavior shown in the issue.