perf: don't type check if no let decls are being referenced

[Rob23oba]

This PR optimizes mkValueTypeClosure to not type check the expressions if they don't refer to let declarations. The type check step only exists to detect which let declarations are actually non-dependent so if they are no let declarations involved, this step can simply be skipped.

[Rob23oba]

!bench

[leanprover-radar]

Benchmark results for 599c07f against 6aec22b are in. There are significant results. @Rob23oba

• ✅ build//instructions: -9.3G (-0.08%)

Large changes (1✅)

• ✅ elab/omega_stress//instructions: -511.5M (-13.60%)

Medium changes (2✅)

• ✅ build/module/Std.Data.DTreeMap.Internal.Operations//instructions: -1.5G (-3.57%) (reduced significance based on absolute threshold)
• ✅ misc/import Init.Data.List.Sublist//instructions: -301.9M (-2.98%)

Small changes (65✅, 1🟥)

• ✅ build/module/Init.Control.StateRef//instructions: -7.6M (-0.84%)
• ✅ build/module/Init.Core//instructions: -40.5M (-0.41%)
• ✅ build/module/Init.Data.Array.Erase//instructions: -33.3M (-0.46%)
• ✅ build/module/Init.Data.Array.Lemmas//instructions: -92.7M (-0.17%)
• ✅ build/module/Init.Data.ByteArray.Bootstrap//instructions: -9.5M (-1.34%)
• ✅ build/module/Init.Data.Fin.Lemmas//instructions: -88.9M (-0.80%)
• ✅ build/module/Init.Data.Int.DivMod.Bootstrap//instructions: -99.3M (-1.86%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Int.DivMod.Lemmas//instructions: -601.7M (-1.56%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Int.Lemmas//instructions: -48.3M (-1.01%)
• ✅ build/module/Init.Data.Int.Order//instructions: -183.0M (-2.01%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Iterators.Combinators.Monadic.FilterMap//instructions: -22.7M (-1.13%)
• ✅ build/module/Init.Data.Iterators.Lemmas.Combinators.FilterMap//instructions: -31.9M (-0.17%)
• ✅ build/module/Init.Data.List.Basic//instructions: -107.7M (-0.82%)
• ✅ build/module/Init.Data.List.BasicAux//instructions: -22.2M (-0.99%)
• ✅ build/module/Init.Data.List.Erase//instructions: -139.6M (-1.98%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.List.Lemmas//instructions: -531.8M (-1.37%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.List.Lex//instructions: -267.1M (-3.08%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.List.MinMaxIdx//instructions: -32.9M (-0.34%)
• ✅ build/module/Init.Data.List.MinMaxOn//instructions: -101.7M (-1.55%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.List.Nat.InsertIdx//instructions: -43.6M (-1.15%) (reduced significance based on absolute threshold)
• and 46 more

[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 6aec22b9d2b2ac082c480b5890a0cb87cdd2b81c --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-10 21:38:31)

[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 6aec22b9d2b2ac082c480b5890a0cb87cdd2b81c --onto b1cd183c9978c3bedddc33baf7c9599baaeca046. You can force reference manual CI using the force-manual-ci label. (2026-08-10 21:38:33)