feat: tree map lemmas about empty, isEmpty, insert, contains

[datokrat]

This PR adds some lemmas about the new tree map. These lemmas are about the interactions of empty, isEmpty, insert, contains. Some lemmas about the interaction of contains with the others will follow in a later PR.

[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 c073da20ce2d30b2df6436852fd229a5eae7b323 --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 15:17:01)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0f1133fe69caddf47b5d3766888da929513917af --onto befee896b38349a51dad1627360adbab317f3192. (2025-02-11 17:42:12)

[datokrat]

I ordered the lemmas in the same way as for the HashMap and stopped as soon as I reached approximately 500 lines. Hence, there are still some lemmas about the interaction of contains with the other operations missing.