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