feat: an .else_eq theorem for sparse casesOn

[nomeata]

This PR adds a realizable .else_eq theorem for sparse casesOn constructions, for rewriting the else case.

This code was complicated by having to work around the kernel reduction issues in #11181 around Nat.xor etc.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-25 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-11-27 15:49:55)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-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-12-14 12:33:46)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-11402 has successfully built against this PR. (2025-11-27 16:52:07) View Log
• ✅ Mathlib branch lean-pr-testing-11402 has successfully built against this PR. (2025-12-14 13:40:38) View Log

[nomeata]

This crept in together with #11666