perf: reduce elaboration time and proof size of tree map internals

[Rob23oba]

There are several things done here:

1. Use the modified simp_to_model which already exists in hash maps. This version of simp_to_model allows specifying the query operations to use in addition to the modifying operations. This is mostly to improve elaboration time and actually increases olean size.
2. Instead of proving toListModel_balance directly, we write toListModel_balanceₘ and use that instead (this saves ~3 MB).
3. Use fun_cases and dsimp instead of rw [x.eq_def] more frequently in Balancing.olean (this saves a bit over 2 MB).
4. Mark updateCell and other functions dependent on it as noncomputable. The main problem with updateCell is how other functions, in particular glue, get recursively inlined, which blows the size of the IR (this saves ~1 MB).
5. Instead of using simp_to_model to prove results on insert!, erase!, etc., simpas are used now, e.g. simpa only [insert_eq_insert!] using isEmpty_insert h. This mainly improves elaboration time although the olean size also goes down by ~0.3 MB.

[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 2363d2fa873a6e5f6e48505b3f1387583c5ef14c --onto 8fc8e8ed19ef218022f5a94cbf5e472e3b777e44. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-12 17:07:21)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2363d2fa873a6e5f6e48505b3f1387583c5ef14c --onto c1d145e9d70569274ac868805b4a8591d09718af. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-13 17:10:58)

[TwoFX]

Thanks!