Auxiliary lemmas for Std.ExtDTreeMap

Bridge lemma lifting DTreeMap.get?_filter_with_getKey_pfilter to Std.ExtDTreeMap, used in turn by the Std.ExtTreeMap layer.

Vendored from Verified-zkEVM/ExtTreeMapLemmas (tag v4.29.1, commit 3fee686227f18dca03bb7fc42ca5a9275d6cfda6).

theorem Std.ExtDTreeMap.get?_filter_with_getKey_pfilter {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} [TransCmp cmp] (m : ExtDTreeMap α (fun (x : α) => β) cmp) (f : α → β → Bool) (k : α) : Const.get? (filter f m) k = (Const.get? m k).pfilter fun (v : β) (h' : Const.get? m k = some v) => f (m.getKey k ⋯) v