fix: return canonically typed subgoals from Sym.Pattern.unify?

[sgraf812]

This PR makes Sym.Pattern.unify? instantiate assigned metavariables in the types of the metavariables it creates for pattern variables, so subgoals returned by Sym.BackwardRule.apply are typed canonically with respect to the assignments made during the application.

All pattern-variable metavariables are created (mkPreResult) before the pending constraints are solved, so solving a pending constraint can assign a metavariable that already occurs in a sibling's type. Syntactic tests on such a subgoal type (isForall, isProp, head tests) then see a bare assigned metavariable where the pretty printer shows the instantiated type; vcgen's excess-state introduction stalls on exactly this after Lean.Order.le_of_forall_le. The stored types are now updated in place (MVarId.setType) after pending constraints are processed; the instantiated type is definitionally equal to the stored one. Unassigned siblings remain metavariable references, so assignments made by the caller still propagate. The instantiation pass runs only when an assignment can have happened after minting (pending constraints, tPending type checks, a universe conflict resolved by isLevelDefEq, or instance synthesis on a type containing metavariables); a fully syntactic match skips it, which keeps the overhead at ≤0.4% instructions on an apply-heavy microbenchmark and at noise level on vcgen/grind workloads. Pattern.match? is unchanged.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 950d7a3 against 58a8cd7 are in. No significant results found. @sgraf812

• 🟥 build//instructions: +1.6G (+0.01%)

Small changes (1✅, 1🟥)

• 🟥 build/module/Lean.Meta.Sym.Pattern//instructions: +751.2M (+5.45%) (reduced significance based on *//lines)
• ✅ compiled/deriv//maxrss: -383kiB (-0.07%)

[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 58a8cd7017bc4fa37adafb821bb2bebb1f99479c --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-27 16:52:25)

[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 58a8cd7017bc4fa37adafb821bb2bebb1f99479c --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force reference manual CI using the force-manual-ci label. (2026-07-27 16:52:26)