fix: preserve error locations when expanding match arms

[nomeata]

This PR ensures that error messages such as “redundant alternative” have
the right error location even if the arms share their RHS. Fixes #10781.

This is a variant of #10783 that changes the syntax to introduce an explicit matchAltPats syntax node.

[nomeata]

This doesn’t work yet. Among other things, the expansion of intro pat into intro x; match x with | pat => ?_ doesn’t pick up the new syntax yet.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-13 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. (2025-10-15 11:08:43)

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-10786 build this PR didn't complete normally. (2025-10-15 11:11:05) View Log