chore: refactor match elaborator to be used from the do elaborator

[sgraf812]

This PR provides the necessary hooks for the new do elaborator to call into the let and match elaborator.

The do match elaborator needs access to a couple of functions from the term match elaborator to implement its own elabMatchAlt. In particular, withEqs, withPatternVars and checkNumPatterns need to be exposed. Furthermore, I think it makes sense to share instantiateAltLHSs.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 9a89539 against 818a0ec are in! @sgraf812

• ✅ build//instructions: -659.6M (-0.01%)

Small changes (1✅, 3🟥)

• ✅ build/module/Lean.Elab.Match//instructions: -92.9M (-0.34%)
• 🟥 build/module/Lean.Elab.MatchAltView//bytes .ilean: +230B (+17.22%)
• 🟥 build/module/Lean.Elab.MatchAltView//bytes .olean: +9kiB (+18.25%)
• 🟥 build/module/Lean.Elab.MatchAltView//bytes .olean.private: +1kiB (+11.06%)

[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 818a0ec6a74d6b9db984e197a1a959e5c540b682 --onto 4cdc199f772977113bd6c1bf87a6c02b78d5c4d3. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-12 09:45:35)

[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 818a0ec6a74d6b9db984e197a1a959e5c540b682 --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-12 09:45:37)