feat: add union on ExtDHashMap/ExtHashMap/ExtHashSet

[wkrozowski]

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

[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 12750d25b5651a87f3ec89d7ec2669c711cbac4f --onto 97d63db52cd2fc3353f8a75f48209de0011f1bd3. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-27 13:45:58)
• ❗ 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 16:26:52)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 00e29075f38e5307b404b656805da137e5c52942 --onto d47b474e41e4b134239ef70fa3c15778cc771bcf. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-10 12:42:15)

[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 12750d25b5651a87f3ec89d7ec2669c711cbac4f --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-27 13:46:00)
• ❗ 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 16:26:53)

[TwoFX]

One more request: in DHashMap/Basic.lean, in the docstring for union, there is a typo: it should say contained instead of contains. Would you mind quickly fixing that as part of this PR.

The PR looks good modulo some minor comments, feel free to merge after fixing.