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

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

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>