Cannot derive eq_def for an @[irreducible] well-founded definition

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

@[irreducible] on a well-founded recursive definition makes it fail to
elaborate:

@[irreducible] def f (n : Nat) (u : Unit) : Nat := if h : n = 0 then 0 else f (n-1) u
  termination_by n

error: Cannot derive f.eq_def from f._unary.eq_def
  Tactic `apply` failed: could not unify the conclusion of 'f._unary.eq_def'

Context

Found by an experimental fuzzer.

Steps to Reproduce

1. Put these two lines in Repro.lean:

   @[irreducible] def f (n : Nat) (u : Unit) : Nat := if h : n = 0 then 0 else f (n-1) u
     termination_by n
   

2. Run lean Repro.lean.

Expected behavior: the file elaborates, as it does without the attribute.

Actual behavior:

Repro.lean:1:0: error: Cannot derive f.eq_def from f._unary.eq_def
  Tactic `apply` failed: could not unify the conclusion of 'f._unary.eq_def'
    f._unary ?u ?n = if h : ?n = 0 then 0 else f._unary ?u (?n - 1)
  with the goal
    f._unary u n = if h : n = 0 then 0 else f (n - 1) u
  
  Note: The full type of 'f._unary.eq_def' is
    ∀ (u : Unit) (n : Nat), f._unary u n = if h : n = 0 then 0 else f._unary u (n - 1)
  
  n : Nat
  u : Unit
  ⊢ f._unary u n = if h : n = 0 then 0 else f (n - 1) u

Versions

Lean 4.35.0-nightly-2026-08-27
Target: x86_64-unknown-linux-gnu Linux

Impact

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

Start with the minimal reproducer in Repro.lean and run it with the specified Lean nightly version. Investigate how the irreducible attribute affects derivation of f.eq_def from f._unary.eq_def for the well-founded definition. Done means the reproducer elaborates successfully with @[irreducible], as it does without the attribute.