perf: eta contract instead of lambda lifting if possible

[hargoniX]

This PR adapts the lambda lifter in LCNF to eta contract instead of lambda lift if possible. This prevents the creation of a few hundred unnecessary lambdas across the code base.

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for 7671691 against 5e165e3 are in! @hargoniX

Runs (2)

• 🟥 build exited with code 2
• 🟥 other exited with code 1

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for 05654e8 against 310abce are in! @hargoniX

Minor changes (1)

• ✅ channel.lean//instructions: -290.6M (-0.7%)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 310abce62b40e4b876f797c4aef7e29d483feb42 --onto 5bd331e85d9d110a29fb3367dbb21854010ffcbd. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-01 19:41:25)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 310abce62b40e4b876f797c4aef7e29d483feb42 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-01 19:41:27)