Add getElem?_mergeWith lemma for TreeMap/DTreeMap

Summary

TreeMap and DTreeMap are missing a semantic lemma for mergeWith that specifies the behavior of getElem? after merging.

Proposed Lemma

@[simp] theorem getElem?_mergeWith [TransCmp cmp] [LawfulEqCmp cmp] 
    {t₁ t₂ : TreeMap α β cmp} {f : α → β → β → β} {k : α} :
    (t₁.mergeWith f t₂)[k]? =
      match t₁[k]?, t₂[k]? with
      | some v1, some v2 => some (f k v1 v2)
      | some v1, none => some v1
      | none, some v2 => some v2
      | none, none => none

Motivation

This lemma is needed for proving properties about maps used as heaps in separation logic (specifically for the Iris proof mode in Lean). Currently, users must prove this from scratch using internal implementation details.

The existing mergeWith lemmas only cover congruence for the ~m equivalence relation, not semantic behavior.

Implementation Notes

A proof exists in https://github.com/alok/iris-lean/blob/feat/heap-instances-105/src/Iris/Std/HeapInstances.lean using:

• foldl_alter_getElem? helper lemma
• Connection through internal Impl.Const.mergeWith!
• Case analysis on membership in both trees

The lemma should ideally be added at all levels: DTreeMap.Internal, DTreeMap, TreeMap, and ExtTreeMap.

Start with the existing mergeWith lemmas and the foldl_alter_getElem? helper, then trace the connection through Impl.Const.mergeWith!. Use the proof in Iris/Std/HeapInstances.lean as a reference and handle membership in both trees across DTreeMap.Internal, DTreeMap, TreeMap, and ExtTreeMap. Done means the proposed semantic getElem? lemma is available at all listed levels.