Auxiliary lemmas for Std.ExtTreeMap

mergeWith and filter lemmas for Std.ExtTreeMap, used by the multivariate polynomial representation in CompPoly.Multivariate.Unlawful.

Vendored from Verified-zkEVM/ExtTreeMapLemmas (tag v4.29.1, commit 3fee686227f18dca03bb7fc42ca5a9275d6cfda6). The original imported Mathlib.Tactic wholesale; here we narrow to the specific tactic modules actually needed by the proofs below.

theorem Std.ExtTreeMap.getElem?_pfilter {α : Type u} {β : Type v} {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 u} {β : Type v} {cmp : α → α → Ordering} {f : α → β → Bool} : filter f ∅ = ∅

theorem Std.ExtTreeMap.getElem?_mergeWith_at {α : Type u} {β : Type v} {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 u} {β : Type v} {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 u} {β : Type v} {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 u} {β : Type v} {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 u} {β : Type v} {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 u} {β : Type v} {f : α → β → β → β} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t : ExtTreeMap α β cmp} : mergeWith f t ∅ = t

theorem Std.ExtTreeMap.mergeWith_of_comm {α : Type u} {β : Type v} {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 u} {β : Type v} {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 u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {f : α → β → Bool} {k : α} {m : ExtTreeMap α β cmp} : (filter f m)[k]? = Option.filter (f k) m[k]?

theorem Std.ExtTreeMap.filter_mem {α : Type u} {β : Type v} {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 u} {β : Type v} {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 u} {β : Type v} {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