fix: show error messages on name conflicts in mutual blocks

[jrr6]

This PR adds error messages for inductive declarations with conflicting constructor names and mutual declarations with conflicting names.

Closes #6694.

[jrr6]

Of note, because conflicting definitions are elaborated simultaneously and without inherently privileging one or the other, I've opted to display errors at both conflicting locations to aid visual localization. This does come with the trade-off of differing from our conflicting-name errors outside mutual blocks, which appear only at the last occurrence in the file. My sense was that mutual blocks already behave differently in nontrivial ways from other declarations, so this deviation in presentation is, as it were, consistent with those other inconsistencies. Alternatively, we could simply surface errors at the last declaration in the mutual block (and likewise for the last problematic inductive/constructor) as we do elsewhere, though at the cost of making the user hunt for the conflicting declaration (jump-to-definition won't work in these instances because the mutual/inductive elaborates monolithically).

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6939 has successfully built against this PR. (2025-02-04 04:50:23) View Log
• ✅ Mathlib branch lean-pr-testing-6939 has successfully built against this PR. (2025-02-05 02:10:18) View Log
• ✅ Mathlib branch lean-pr-testing-6939 has successfully built against this PR. (2025-02-05 02:58:30) View Log
• ✅ Mathlib branch lean-pr-testing-6939 has successfully built against this PR. (2025-02-05 04:18:49) View Log