theorem Std.DTreeMap.Const.get?_foldl_no_touch {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (k : α) (f : α → β → β → β) (l : List (α × β)) (t : DTreeMap α (fun (x : α) => β) cmp) (hno : ∀ (p : α × β), p ∈ l → cmp p.fst k ≠ Ordering.eq) : get? (List.foldl (fun (acc : DTreeMap α (fun (x : α) => β) cmp) (p : α × β) => alter acc p.fst fun (x : Option β) => match x with | none => some p.snd | some b₁ => some (f p.fst b₁ p.snd)) t l) k = get? t k

theorem Std.DTreeMap.Const.get?_mergeWith {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (f : α → β → β → β) (t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp) (k : α) : get? (mergeWith f t₁ t₂) k = match get? t₁ k, get? t₂ k with | some v₁, some v₂ => some (f k v₁ v₂) | some v₁, none => some v₁ | none, some v₂ => some v₂ | none, none => none

theorem Std.DTreeMap.Internal.Impl.Const.get?_filter_with_getKey_pfilter {α : Type u} {β : Type v} [Ord α] [TransOrd α] (m : Impl α fun (x : α) => β) (h : m.WF) (f : α → β → Bool) (k : α) : get? (filter f m ⋯).impl k = (get? m k).pfilter fun (v : β) (h' : get? m k = some v) => f (m.getKey k ⋯) v

theorem Std.DTreeMap.get?_filter_with_getKey_pfilter {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] (m : DTreeMap α (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