feat: support more indexed monads in elabDoWith

[sgraf812]

This PR adds two new fields to DoOps, splitMonadApp? and mkMonadApp, so that callers of elabDoWith can use indexed monads like Measure α (where Measure : (α : Type u) → [MeasureSpace α] → Type u carries instance arguments) that the default m α decomposition cannot handle. The existing behavior moves into DoOps.default.

splitMonadApp? replaces the hard-coded .app m α step inside the extractMonadInfo recursion, and mkMonadApp replaces the hard-coded mkApp m α used to construct the monadic type.

[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 34df7320668250fa586c2bbb706637896581a3f9 --onto 43ef70db63e2c1c1720b84fd153125c96a00c5d2. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-20 16:34:41)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase da8bcf79160085502377aea35b4c338cfa34a72d --onto 43ef70db63e2c1c1720b84fd153125c96a00c5d2. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-20 18:07:01)

[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 34df7320668250fa586c2bbb706637896581a3f9 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-20 16:34:43)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase da8bcf79160085502377aea35b4c338cfa34a72d --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-20 18:07:03)