feat: extensional tree maps

[Rob23oba]

This PR adds the types Std.ExtDTreeMap, Std.ExtTreeMap and Std.ExtTreeSet of extensional tree maps and sets. These are very similar in construction to the existing extensional hash maps with one exception: extensional tree maps and sets provide all functions from regular tree maps and sets. This is possible because in contrast to hash maps, tree maps are always ordered.

[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 614e6122f75cd6a1d553ac58c0a65ab47da40dc3 --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-11 10:26:55)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 77fd1ba6b91b0bb439bb5a75b819d1f3588a853f --onto faffe863343211d03d07d4ef19d90a2aa9d6fc8c. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-12 17:48:09)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 40d2c9946319716228b414e501e71b7f959e1619 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-26 13:21:33)

[kim-em]

Could we have a constructor TreeMap \to ExtTreeMap?

[TwoFX]

Could we have a constructor TreeMap \to ExtTreeMap?

In https://github.com/leanprover/lean4/pull/8004#discussion_r2056101702 we decided to do all of the "connect the map variants" functions at a later date with a structured plan instead of doing one of them ad-hoc now, so it is expected that this is not part of this PR.