Add getElem?_mergeWith lemma for TreeMap/DTreeMap

[alok]

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.