refactor: use simp_to_model for TreeMap mergeWith

[ctkrug]

Description

Replace the bespoke TreeMap.mergeWith lookup proof and its private fold helpers with a direct simp_to_model proof. This preserves both public theorem signatures while replacing 122 lines of implementation-specific machinery with a 10-line model-based proof.

This draft depends on the Std model bridge in leanprover/lean4#14526.

Validation performed on the exact committed diff:

• native Lean v4.32 release build with the proposed Std bridge
• focused downstream simp_to_model bridge checker
• full Iris-Lean build (259 jobs)
• independent theorem-signature and proof-safety checker

Fixes #127.

Checklist

• My code follows the mathlib naming and code style conventions
• No file-level authors list needs updating for this proof refactor

Generative AI Guidelines

AI assistance was used to investigate and draft the refactor. The final proof was manually reviewed, the duplicated constructions were removed, both public theorem signatures were preserved, and all checks listed above passed.

[markusdemedeiros]

Awesome! Thanks for figuring this out.