simp produces proof terms that lead to `(kernel) deterministic timeout`

Prerequisites

• Check that your issue is not already filed:
• Reduce the issue to a minimal, self-contained, reproducible test case.
• Test your test case against the latest nightly release

Description

simp produces a proof term that times out in the kernel with (kernel) deterministic timeout. This seems somewhat similar to https://github.com/leanprover/lean4/pull/14770.

Context

Encountered in a pre-release version of Veil. We are working around the issue by post-processing the proof terms.

Steps to Reproduce

import Lean
/-!
Performance bug: kernel def-eq is exponentially slower than `Meta.isDefEq` on
app-vs-lambda (eta) pairs whose application side is expensive to normalize, and
`simp` produces such proof terms, even with `-implicitDefEqProofs`. It should
rewrite the proof term to avoid the kernel timeout.

The two sides of `bug` below differ *only by eta*: `interp t` vs
`fun x => interp t x`. `Meta.isDefEq` answers `true` in ~1 ms (it tries eta
early). The kernel instead delta-normalizes the application side before eta
applies, i.e. it symbolically evaluates the interpreter over the whole tree:

  depth 6:  ~0.2 s
  depth 8:  ~25 s
  depth 10+: (kernel) deterministic timeout (default heartbeats)

while the elaborator-side check stays ~1 ms at every depth.

We ran into this in Veil.
-/

inductive T where
  | leaf
  | node (l r : T)

/-- Complete binary tree of depth `n` with structurally distinct subtrees
(so pointer-equality caching cannot collapse the comparison). -/
def mkT : Nat → Nat → T
  | 0, _ => .leaf
  | n+1, i => .node (mkT n (2*i)) (mkT n (2*i+1))

/-- A tiny "interpreter": function-valued structural recursion. -/
def interp : T → Nat → Nat
  | .leaf => Nat.succ
  | .node l r => interp l ∘ interp r

def wrap (f : Nat → Nat) : Nat → Nat := f

theorem wrap_eq (f : Nat → Nat) : wrap f = fun x => f x := rfl

-- `simp` (both with and without -implicitDefEqProofs) closes this instantly and
-- emits the proof; the kernel then times out checking it at `addDecl`.
theorem viaSimp : wrap (interp (mkT 10 0)) = interp (mkT 10 0) := by
  simp -implicitDefEqProofs only [wrap_eq]

Versions

Observed on all versions from Lean 4.28.0 (and potentially before) through
v4.34.0-rc1, also including nightly-2026-08-17 (4.35.0), on macOS 26.6.1.

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 self-contained Lean reproduction with simp -implicitDefEqProofs only [wrap_eq] and compare the behavior of Meta.isDefEq with kernel checking at addDecl. Trace how simp produces the proof term and how the kernel checks it; done means the reproduced theorem is accepted without a deterministic timeout.