feat: add union on DTreeMap/TreeMap/TreeSet

[wkrozowski]

This PR adds union operations on DTreeMap/TreeMap/TreeSet and their raw variants and 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 69d8d63d58e56e873654341d4dddaac2c4a70737 --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-24 11:01:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 69d8d63d58e56e873654341d4dddaac2c4a70737 --onto 705084d9ba258dec704af428d7ce2444525f9ffb. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-30 23:49:06)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 69d8d63d58e56e873654341d4dddaac2c4a70737 --onto 3e86729ee0e11548a47f9b294d5292ada92c0b40. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-03 13:44:29)

[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 69d8d63d58e56e873654341d4dddaac2c4a70737 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-24 11:01:41)

[wkrozowski]

@datokrat Thanks for your comments! I have responded to and fixed everything :)

[datokrat]

Looks good to me if you address the naming of union_insert lemmas!