feat: add union on ExtDTreeMap/ExtTreeMap/ExtTreeSet

[wkrozowski]

This PR adds union operation on ExtDHashMap/ExtHashMap/ExtHashSet nd provides lemmas about union operations.

Stacked on top of #10946.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 00e29075f38e5307b404b656805da137e5c52942 --onto 3e86729ee0e11548a47f9b294d5292ada92c0b40. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-03 19:23:08)

[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 00e29075f38e5307b404b656805da137e5c52942 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-03 19:23:10)