perf: cache and canonicalize lifts of substituted values in instantiateMVars

[nomeata]

This PR fixes an exponential blowup (time and memory, typically surfacing as an out-of-memory failure) in instantiateMVars on proof terms that repeatedly reference hypotheses introduced via MVarId.assert/intro — as done by MVarId.note, replaceLocalDecl, simp at h, and, per step, by LNSym's sym_n tactic. Fixes #14329.

Since #12233, instantiateMVars resolves delayed metavariable assignments in a single fused pass that carries an fvar substitution through the chain. The substituted values can contain loose bvars of enclosing binders, so every occurrence of such an fvar at a deeper binder depth needs the value lifted by the depth difference, and lift_loose_bvars materializes a fresh copy each time. Because substitution values have all enclosing substitutions already applied, they physically embed the lifted copies made for earlier hypotheses, so lifting them copies those again: with each step referencing the previous step's hypotheses k times, the copies compound to k^N nodes. In the LNSym reproduction this means ~4x growth per simulated instruction and an OOM at 12 steps.

This PR routes all lifting of substitution values through a single lift implementation with a cache that lives for the whole pass: results are memoized per (node, cutoff, amount), so all occurrences of a value at the same depth — including values shared between substitution entries — share one copy, and whole-value results are indexed back to their origin, so lifting an already-lifted value redirects to one canonical copy per (origin, cumulative amount) instead of copying the copy. Together this materializes every lift at most once, which bounds the instantiated term by one copy per distinct cumulative depth and restores linear behavior on the workloads above. The origin redirect is a pure sharing optimization: it fires only when the cutoff at the redirect is at most the recorded shift — in which case all loose bvars of the copy are shifted and the composition lift d ∘ lift s = lift (s + d) is exact — and otherwise falls back to the structural copy, which is always correct. The implementation follows the patterns of lift_loose_bvars and replace_rec_fn: subtree pruning via the cached loose-bvar range, sharing-gated caching of interior nodes, allocation-free rebuilds via update_*, and retention of the expressions behind raw-pointer cache keys.

Verified against the LNSym reproduction from #14329: the instantiated proof term is back to linear size (matching the v4.29 node counts), and the full 27-step popcount32 probe elaborates in about 1.2s where it previously exceeded 41GB. The two reproducer patterns are added as tests/elab/issue14329a.lean (occurrences at one binder depth, covered by memoization alone) and tests/elab/issue14329b.lean (occurrences at several binder depths, requiring the origin redirect). Instruction-count A/B on the elab_bench suite (same compiler, sources with and without the patch) is neutral within ±0.2%, including the benchmarks #12233 was built for (delayed_assign, delayed_sharing, bv_decide_*, big_struct_dep), and the full test suite passes against both stage 1 and stage 2 with a clean stage 2 stdlib build.

The mathlib benchmarks show one significant change: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit drops by 26.2G instructions (-55%), to below its historical minimum. This is the bounded version of the same defect: the module's instruction count had regressed from ~24G to ~30G exactly when nightly-testing first picked up #12233, and further to ~47G with nightly-2026-04-16. Its two proofs (Borceux's Theorem 2.13.4) are long element-chasing scripts that interleave existential destructuring (obtain ⟨...⟩ := IsFiltered.sup_exists ..., adding binder depth) with hypothesis rewriting (simp only [...] at h, i.e. assert-introduced hypotheses), and then reference those hypotheses several times from deeper in the proof (e.g. h feeding four (h j).choose* definitions) — so the lifted copies of their large proof terms were duplicated at every level, costing a factor of about 2 on this file, where the longer mechanically generated chains of LNSym's sym_n in #14329 grow exponentially and fail outright.

🤖 Generated with Claude Code

[nomeata]

!perf

[nomeata]

!bench

[leanprover-radar]

Benchmark results for a769696 against 3259610 are in. No significant results found. @nomeata

• ✅ build//instructions: -246.4M (-0.00%)

Medium changes (1🟥)

• 🟥 size/all/.cpp//lines: +133.0 (+0.47%)

Small changes (3✅)

• ✅ build/module/Init.Data.String.Lemmas.Pattern.Basic//instructions: -79.2M (-0.87%)
• ✅ elab/big_struct_dep1//instructions: -29.1M (-0.56%)
• ✅ elab/delayed_assign//wall-clock: -28ms (-6.67%)

[nomeata]

!bench

[leanprover-radar]

Benchmark results for c957944 against 3259610 are in. No significant results found. @nomeata

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

Medium changes (1🟥)

• 🟥 size/all/.cpp//lines: +134.0 (+0.47%)

Small changes (4✅)

• ✅ build/module/Init.Data.String.Lemmas.Pattern.Basic//instructions: -74.1M (-0.82%)
• ✅ elab/big_struct_dep1//instructions: -28.5M (-0.55%)
• ✅ misc/leanchecker --fresh Init//task-clock: -1s (-4.37%)
• ✅ misc/leanchecker --fresh Init//wall-clock: -1s (-4.34%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-07-23 13:26:30)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14520 has successfully built against this PR. (2026-07-23 14:52:15) View Log
• ✅ Mathlib branch lean-pr-testing-14520 has successfully built against this PR. (2026-07-23 21:38:26) View Log

[nomeata]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@b63a683 against leanprover-community/mathlib4-nightly-testing@eaeb601 are in. No significant results found. @nomeata

• 🟥 build//instructions: +73.6G (+0.05%)

Medium changes (1✅)

• ✅ build/module/Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit//instructions: -26.2G (-54.99%)

[nomeata]

!bench

[leanprover-radar]

Benchmark results for c0296ec against 3259610 are in. No significant results found. @nomeata

• ✅ build//instructions: -89.1M (-0.00%)

Medium changes (1🟥)

• 🟥 size/all/.cpp//lines: +134.0 (+0.47%)

Small changes (4✅)

• ✅ build/module/Init.Data.String.Lemmas.Pattern.Basic//instructions: -87.2M (-0.96%)
• ✅ elab/big_struct_dep1//instructions: -29.6M (-0.57%)
• ✅ misc/leanchecker --fresh Init//task-clock: -1s (-4.80%)
• ✅ misc/leanchecker --fresh Init//wall-clock: -1s (-4.75%)