theorem Std.ExtTreeMap.getElem?_pfilter {α β : Type} {cmp : α → α → Ordering} [TransCmp cmp] {m : ExtTreeMap α β cmp} {f : α → β → Bool} {k : α} : (filter f m)[k]? = m[k]?.pfilter fun (v : β) (h' : m[k]? = some v) => f (m.getKey k ⋯) v

@[simp]

theorem Std.ExtTreeMap.filter_empty {α β : Type} {cmp : α → α → Ordering} {f : α → β → Bool} : filter f ∅ = ∅

theorem Std.ExtTreeMap.get?_mergeWith_at {α β : Type} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {m₁ m₂ : ExtTreeMap α β cmp} {f : α → β → β → β} {k : α} : (mergeWith f m₁ m₂)[k]? = match m₁[k]?, m₂[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.ExtTreeMap.mergeWith_of_mem_mem {α β : Type} {cmp : α → α → Ordering} {k : α} {m₁ m₂ : ExtTreeMap α β cmp} {f : α → β → β → β} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : k ∈ m₁) (h₂ : k ∈ m₂) : (mergeWith f m₁ m₂)[k]? = some (f k m₁[k] m₂[k])

theorem Std.ExtTreeMap.mergeWith_of_mem_left {α β : Type} {cmp : α → α → Ordering} {k : α} {m₁ m₂ : ExtTreeMap α β cmp} {f : α → β → β → β} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : k ∈ m₁) (h₂ : k ∉ m₂) : (mergeWith f m₁ m₂)[k]? = m₁[k]?

theorem Std.ExtTreeMap.mergeWith_of_mem_right {α β : Type} {cmp : α → α → Ordering} {k : α} {m₁ m₂ : ExtTreeMap α β cmp} {f : α → β → β → β} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : k ∉ m₁) (h₂ : k ∈ m₂) : (mergeWith f m₁ m₂)[k]? = m₂[k]?

theorem Std.ExtTreeMap.mergeWith_of_not_mem {α β : Type} {cmp : α → α → Ordering} {k : α} {m₁ m₂ : ExtTreeMap α β cmp} {f : α → β → β → β} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : k ∉ m₁) (h₂ : k ∉ m₂) : (mergeWith f m₁ m₂)[k]? = none

@[simp]

theorem Std.ExtTreeMap.mergeWith_empty {α β : Type} {f : α → β → β → β} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t : ExtTreeMap α β cmp} : mergeWith f t ∅ = t

theorem Std.ExtTreeMap.mergeWith_of_comm {α β : Type} {cmp : α → α → Ordering} {m₁ m₂ : ExtTreeMap α β cmp} {f : α → β → β → β} [TransCmp cmp] [LawfulEqCmp cmp] (h : ∀ {x : α}, Commutative (f x)) : mergeWith f m₁ m₂ = mergeWith f m₂ m₁

@[simp]

theorem Std.ExtTreeMap.toList_ofList {α β : Type} {cmp : α → α → Ordering} {m : ExtTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEq α] : ofList m.toList cmp = m

@[simp]

theorem Std.ExtTreeMap.getElem?_filter_with_getKey {α : Type} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {β : Type} {f : α → β → Bool} {k : α} {m : ExtTreeMap α β cmp} : (filter f m)[k]? = Option.filter (f k) m[k]?

theorem Std.ExtTreeMap.filter_mem {α β : Type} {cmp : α → α → Ordering} {k : α} {m : ExtTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : α → β → Bool} (h : k ∈ m) : f k m[k] = true → (filter f m)[k]? = some m[k]

theorem Std.ExtTreeMap.filter_not_mem {α β : Type} {cmp : α → α → Ordering} {k : α} {m : ExtTreeMap α β cmp} [TransCmp cmp] {f : α → β → Bool} (h : k ∉ m) : (filter f m)[k]? = none

theorem Std.ExtTreeMap.filter_not_pred {α β : Type} {cmp : α → α → Ordering} {k : α} {m : ExtTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : α → β → Bool} (h : k ∈ m) : ¬f k m[k] = true → (filter f m)[k]? = none