perf: try eta-expansion before delta-reduction in the kernel

[Kha]

This PR fixes (kernel) deterministic timeout errors on proof terms whose two sides differ only by eta, such as the ones simp produces when rewriting with a function-valued equation. The kernel now answers those definitional equality checks as quickly as Meta.isDefEq already did.

Meta.isExprDefEqExpensive tries isDefEqEta before whnfCore and lazy delta-reduction, but type_checker::is_def_eq_core only tried try_eta_expansion after lazy_delta_reduction. So for f a =?= fun x => f a x the kernel delta-normalized f a instead of eta-expanding it, and as soon as the unfolded side became a lambda itself, quick_is_def_eq committed to is_def_eq_binding without backtracking and descended into the normalized subterms. When f is a structural recursion over a tree, that is exponential in the tree's depth: the reproducer in tests/elab/14803.lean took 19s at depth 8 and timed out at depth 10, and now takes 0.1s.

Since the kernel has no metavariables, (fun x => t) =?= s holds iff (fun x => t) =?= (fun x => s x), so trying eta first cannot lose solutions. The try_eta_expansion call after lazy_delta_reduction is kept because that reduction updates both sides and may expose a lambda the earlier check did not see.

Closes #14803

[Kha]

!bench

[Kha]

!bench mathlib

[leanprover-radar]

Benchmark results for e5bda08 against fd0efc4 are in. There are significant results. @Kha

• ✅ build//instructions: -2.0G (-0.02%)

Large changes (3✅)

• ✅ compiled/rbmap_checkpoint//instructions: -2.6G (-17.06%)
• ✅ compiled/rbmap_checkpoint//task-clock: -719ms (-32.92%)
• ✅ compiled/rbmap_checkpoint//wall-clock: -725ms (-33.03%)

Small changes (1✅, 21🟥)

• 🟥 build/module/Init.Data.Range.Polymorphic.UInt//instructions: +13.6M (+0.31%)
• ✅ compiled/const_fold//instructions: -111.5M (-1.53%)
• 🟥 elab/big_beq//maxrss: +11MiB (+0.59%)
• 🟥 elab/big_beq_rec//maxrss: +11MiB (+0.63%)
• 🟥 elab/big_deceq//maxrss: +11MiB (+0.60%)
• 🟥 elab/big_deceq_rec//maxrss: +11MiB (+0.64%)
• 🟥 elab/big_match//maxrss: +11MiB (+0.58%)
• 🟥 elab/big_match_nat//maxrss: +11MiB (+0.62%)
• 🟥 elab/big_match_partial//maxrss: +11MiB (+0.62%)
• 🟥 elab/bv_decide_inequality//wall-clock: +69ms (+1.71%)
• 🟥 elab/delayed_lift//maxrss: +10MiB (+0.58%)
• 🟥 elab/delayed_sharing//maxrss: +11MiB (+0.60%)
• 🟥 elab/let_to_have_closed_body//maxrss: +8MiB (+0.47%)
• 🟥 elab/lift_lets_binders//maxrss: +10MiB (+0.55%)
• 🟥 elab/lift_lets_chain//maxrss: +11MiB (+0.61%)
• 🟥 elab/lift_lets_dag//maxrss: +11MiB (+0.62%)
• 🟥 elab/lift_lets_parallel//maxrss: +11MiB (+0.60%)
• 🟥 elab/lift_lets_spine//maxrss: +11MiB (+0.64%)
• 🟥 elab/string_simp_ne//maxrss: +12MiB (+0.64%)
• 🟥 elab/sym_let_to_have_nested//maxrss: +10MiB (+0.55%)
• and 2 more

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@75f0e66 against leanprover-community/mathlib4-nightly-testing@7e7506d are in. No significant results found. @Kha

• 🟥 build//instructions: +95.1G (+0.07%)

Medium changes (2🟥)

• 🟥 build/module/Mathlib.Algebra.Category.Ring.Under.Property//instructions: +2.9G (+13.41%)
• 🟥 build/module/Mathlib.RingTheory.Morita.Matrix//instructions: +12.2G (+16.49%)

Small changes (5🟥)

• 🟥 build/module/Mathlib.Algebra.Category.BialgCat.Monoidal//instructions: +940.0M (+2.68%)
• 🟥 build/module/Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op//instructions: +886.5M (+16.55%) (reduced significance based on absolute threshold)
• 🟥 build/module/Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex//instructions: +1.2G (+17.26%)
• 🟥 build/module/Mathlib.Tactic.GRewrite//instructions: +55.4M (+2.81%)
• 🟥 build/module/ProofWidgets.Component.PenroseDiagram//instructions: +27.4M (+0.81%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-22 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-25 15:14:49)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14927 has successfully built against this PR. (2026-08-25 16:11:07) View Log