perf: try letToHave for dependent lets in cbv

[wkrozowski]

This PR makes the cbv tactic try letToHave on dependent let bindings
before falling back to zeta reduction. When the conversion succeeds, the
resulting non-dependent let is beta-reduced directly, avoiding unnecessary
zeta expansion.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for b5a3c41 against e2b500b are in. There are no significant changes. @wkrozowski

• 🟥 build//instructions: +27.3M (+0.00%)

Small changes (1✅, 1🟥)

• 🟥 build/module/Lean.Meta.Tactic.Cbv.Main//instructions: +89.9M (+1.42%) (reduced significance based on *//lines)
• ✅ lake/inundation/env//task-clock: -7ms (-4.44%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e2b500b204cacbb3149f42feda880c8bdfcab7db --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-09 18:11:35)

[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 e2b500b204cacbb3149f42feda880c8bdfcab7db --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-09 18:11:37)