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, for example isLambda to control whether to get a forall or lambda, and inferNames for whether to use the mkForallFVars' machinery to infer names for anonymous metavariables
• 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)

[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)