fix: improved dependency tracking in metacontext and abstractMVars

[kmill]

This PR fixes some issues involving tracking dependencies through metavariables. First, functions like Lean.exprDependsOn' were not following dependencies through delayed metavariable assignments. Second, abstractMVars was abstracting metavariables that free variables in the expression themselves depended on, creating type incorrect terms.

API changes:

• findExprDependsOn has been split into two; the metavariable version is findExprDependsOnMVar. This is because they have different considerations for metavariable dependence — only the latter needs to follow delayed assignments for example
• These functions now take an optional local context, for tracing dependencies through types and values of free variables.
• Similary, findLocalDeclDependsOn has an accompanying findLocalDeclDependsOnMVar.
• dependsOnPred is deprecated in favor of findExprDependsOn
• localDeclDependsOnPred is deprecated in favor of findLocalDeclDependsOn
• added collectFVarDeps and collectMVarDeps for finding the complete sets of backward dependencies of an expression, with respect to a given local context
• setMVarUserNamesAt now takes a predicate rather than an array
• abstractMVars has additional options
  • isLambda controls whether to get a forall or lambda
  • inferNames controls whether or not to use the mkForallFVars' machinery to infer names for anonymous metavariables
  • levelsNotFixed is intended for typeclass instance synthesis. It causes all level metavariables to be abstracted regardless of whether or not they are fixed by the local context. It is a workaround for level metavariable assignments not persisting across withNewMCtxDepth.
• AbstractMVarsResult has been extended with a little more information, and the mvars field has been replaced with exprArgs, anticipating a potential feature where abstractMVars can properly handle delayed assignments. Currently it treats them as plain metavariables, which can lead to underapplied delayed assignments if you use this field for creating an application!

Closes #2483, closes #9286

[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 0f730662de0bbaa6ed07484d8f0e411de2bcd1ea --onto 87180a09c49c91577e54284703c73c5ca76be126. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-21 19:42:07)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0f730662de0bbaa6ed07484d8f0e411de2bcd1ea --onto 90b5e3185b3b948ce1c75281d3e95f370c8493a6. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-22 20:51:47)

[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 0f730662de0bbaa6ed07484d8f0e411de2bcd1ea --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-21 19:42:09)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-31 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-04-01 12:20:47)

[kmill]

!bench

[leanprover-radar]

Benchmark results for d4d3eaa against 0f73066 are in. Significant changes detected! @kmill

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

No significant changes detected.

[kmill]

!bench

[leanprover-radar]

Benchmark results for f8b0545 against 0f73066 are in. Significant changes detected! @kmill

• 🟥 build//instructions: +36.2G (+0.30%)

Medium changes (1✅, 5🟥)

• 🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.1G (+0.52%)
• 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: +1.2G (+1.02%)
• 🟥 elab/big_match_nat_split//instructions: +216.0M (+1.83%)
• ✅ elab/big_struct_dep//instructions: -109.5M (-0.75%)
• 🟥 elab/omega_stress//instructions: +48.3M (+1.12%)
• 🟥 misc/import Std.Data.Internal.List.Associative//instructions: +670.5M (+0.85%)

Small changes (2✅, 142🟥)

Too many entries to display here. View the full report on radar instead.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13025 build failed against this PR. (2026-04-01 12:25:05) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13025 build failed against this PR. (2026-04-01 15:22:16) View Log