Extensional tree map lemmas #
This file contains lemmas about Std.ExtTreeMap
.
@[simp]
theorem
Std.ExtTreeMap.insert_ne_empty
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.contains_congr
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k k' : α}
(hab : cmp k k' = Ordering.eq)
:
theorem
Std.ExtTreeMap.mem_congr
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k k' : α}
(hab : cmp k k' = Ordering.eq)
:
theorem
Std.ExtTreeMap.ne_empty_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{a : α}
(h : a ∈ t)
:
@[simp]
theorem
Std.ExtTreeMap.insert_eq_insert
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{p : α × β}
:
@[simp]
theorem
Std.ExtTreeMap.contains_insert
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[h : TransCmp cmp]
{k a : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.mem_insert
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
:
theorem
Std.ExtTreeMap.mem_insert_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.mem_of_mem_insert
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
:
a ∈ t.insert k v → cmp k a ≠ Ordering.eq → a ∈ t
theorem
Std.ExtTreeMap.isEmpty_eq_size_beq_zero
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
:
@[simp]
theorem
Std.ExtTreeMap.contains_erase
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
:
@[simp]
theorem
Std.ExtTreeMap.mem_erase
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
:
theorem
Std.ExtTreeMap.mem_of_mem_erase
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
:
@[simp]
theorem
Std.ExtTreeMap.containsThenInsert_fst
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.containsThenInsert_snd
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.containsThenInsertIfNew_fst
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.containsThenInsertIfNew_snd
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.getElem_congr
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{a b : α}
(hab : cmp a b = Ordering.eq)
{h' : a ∈ t}
:
@[simp]
theorem
Std.ExtTreeMap.getD_insert_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{fallback v : β}
:
@[simp]
theorem
Std.ExtTreeMap.getD_erase_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{fallback : β}
:
theorem
Std.ExtTreeMap.getD_congr
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{a b : α}
{fallback : β}
(hab : cmp a b = Ordering.eq)
:
theorem
Std.ExtTreeMap.compare_getKey?_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
:
theorem
Std.ExtTreeMap.getKey?_congr
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k k' : α}
(h' : cmp k k' = Ordering.eq)
:
theorem
Std.ExtTreeMap.getKey?_eq_some_of_contains
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k : α}
(h' : t.contains k = true)
:
theorem
Std.ExtTreeMap.getKey?_eq_some
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k : α}
(h' : k ∈ t)
:
theorem
Std.ExtTreeMap.getKey_insert
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
{h₁ : a ∈ t.insert k v}
:
@[simp]
theorem
Std.ExtTreeMap.getKey_insert_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.compare_getKey_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
(h' : k ∈ t)
:
theorem
Std.ExtTreeMap.getKey_congr
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k₁ k₂ : α}
(h' : cmp k₁ k₂ = Ordering.eq)
(h₁ : k₁ ∈ t)
:
@[simp]
theorem
Std.ExtTreeMap.getKey_eq
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k : α}
(h' : k ∈ t)
:
theorem
Std.ExtTreeMap.getKey!_congr
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[Inhabited α]
{k k' : α}
(h' : cmp k k' = Ordering.eq)
:
theorem
Std.ExtTreeMap.getKey!_eq_of_contains
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
[Inhabited α]
{k : α}
(h' : t.contains k = true)
:
theorem
Std.ExtTreeMap.getKey!_eq_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
[Inhabited α]
{k : α}
(h' : k ∈ t)
:
@[simp]
theorem
Std.ExtTreeMap.getKeyD_insert_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{a fallback : α}
{b : β}
:
@[simp]
theorem
Std.ExtTreeMap.getKeyD_erase_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k fallback : α}
:
theorem
Std.ExtTreeMap.getKeyD_congr
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k k' fallback : α}
(h' : cmp k k' = Ordering.eq)
:
theorem
Std.ExtTreeMap.getKeyD_eq_of_contains
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k fallback : α}
(h' : t.contains k = true)
:
theorem
Std.ExtTreeMap.getKeyD_eq_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k fallback : α}
(h' : k ∈ t)
:
@[simp]
theorem
Std.ExtTreeMap.insertIfNew_ne_empty
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.contains_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.mem_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.contains_insertIfNew_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.mem_insertIfNew_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.contains_of_contains_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
:
(t.insertIfNew k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
theorem
Std.ExtTreeMap.mem_of_mem_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
:
a ∈ t.insertIfNew k v → cmp k a ≠ Ordering.eq → a ∈ t
theorem
Std.ExtTreeMap.mem_of_mem_insertIfNew'
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
:
a ∈ t.insertIfNew k v → ¬(cmp k a = Ordering.eq ∧ ¬k ∈ t) → a ∈ t
This is a restatement of mem_of_mem_insertIfNew
that is written to exactly match the
proof obligation in the statement of get_insertIfNew
.
theorem
Std.ExtTreeMap.size_le_size_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.size_insertIfNew_le
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.getElem_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
{h₁ : a ∈ t.insertIfNew k v}
:
theorem
Std.ExtTreeMap.getD_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{fallback v : β}
:
theorem
Std.ExtTreeMap.getKey?_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
:
theorem
Std.ExtTreeMap.getKey_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a : α}
{v : β}
{h₁ : a ∈ t.insertIfNew k v}
:
theorem
Std.ExtTreeMap.getKey!_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[Inhabited α]
{k a : α}
{v : β}
:
theorem
Std.ExtTreeMap.getKeyD_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k a fallback : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.getThenInsertIfNew?_fst
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.getThenInsertIfNew?_snd
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
instance
Std.ExtTreeMap.instLawfulGetElemMem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[TransCmp cmp]
:
LawfulGetElem (ExtTreeMap α β cmp) α β fun (m : ExtTreeMap α β cmp) (a : α) => a ∈ m
@[simp]
theorem
Std.ExtTreeMap.contains_keys
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[BEq α]
[LawfulBEqCmp cmp]
[TransCmp cmp]
{k : α}
:
@[simp]
theorem
Std.ExtTreeMap.mem_keys
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[LawfulEqCmp cmp]
[TransCmp cmp]
{k : α}
:
theorem
Std.ExtTreeMap.distinct_keys
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
:
List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) t.keys
theorem
Std.ExtTreeMap.ordered_keys
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
:
List.Pairwise (fun (a b : α) => cmp a b = Ordering.lt) t.keys
theorem
Std.ExtTreeMap.find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k k' : α}
{v : β}
:
theorem
Std.ExtTreeMap.find?_toList_eq_none_iff_contains_eq_false
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
:
@[simp]
theorem
Std.ExtTreeMap.find?_toList_eq_none_iff_not_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
:
theorem
Std.ExtTreeMap.distinct_keys_toList
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
:
List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) t.toList
theorem
Std.ExtTreeMap.ordered_keys_toList
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
:
List.Pairwise (fun (a b : α × β) => cmp a.fst b.fst = Ordering.lt) t.toList
theorem
Std.ExtTreeMap.foldlM_eq_foldlM_toList
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
{m : Type w → Type w'}
[TransCmp cmp]
[Monad m]
[LawfulMonad m]
{f : δ → α → β → m δ}
{init : δ}
:
theorem
Std.ExtTreeMap.foldl_eq_foldl_toList
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
[TransCmp cmp]
{f : δ → α → β → δ}
{init : δ}
:
theorem
Std.ExtTreeMap.foldrM_eq_foldrM_toList
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
{m : Type w → Type w'}
[TransCmp cmp]
[Monad m]
[LawfulMonad m]
{f : α → β → δ → m δ}
{init : δ}
:
theorem
Std.ExtTreeMap.foldr_eq_foldr_toList
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
[TransCmp cmp]
{f : α → β → δ → δ}
{init : δ}
:
@[simp]
theorem
Std.ExtTreeMap.forIn_eq_forIn
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
{m : Type w → Type w'}
[TransCmp cmp]
[Monad m]
[LawfulMonad m]
{f : α → β → δ → m (ForInStep δ)}
{init : δ}
:
theorem
Std.ExtTreeMap.forIn_eq_forIn_toList
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
{m : Type w → Type w'}
[TransCmp cmp]
[Monad m]
[LawfulMonad m]
{f : α × β → δ → m (ForInStep δ)}
{init : δ}
:
theorem
Std.ExtTreeMap.foldlM_eq_foldlM_keys
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
{m : Type w → Type w'}
[TransCmp cmp]
[Monad m]
[LawfulMonad m]
{f : δ → α → m δ}
{init : δ}
:
theorem
Std.ExtTreeMap.foldl_eq_foldl_keys
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
[TransCmp cmp]
{f : δ → α → δ}
{init : δ}
:
theorem
Std.ExtTreeMap.foldrM_eq_foldrM_keys
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
{m : Type w → Type w'}
[TransCmp cmp]
[Monad m]
[LawfulMonad m]
{f : α → δ → m δ}
{init : δ}
:
theorem
Std.ExtTreeMap.foldr_eq_foldr_keys
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
[TransCmp cmp]
{f : α → δ → δ}
{init : δ}
:
theorem
Std.ExtTreeMap.forIn_eq_forIn_keys
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
{δ : Type w}
{m : Type w → Type w'}
[TransCmp cmp]
[Monad m]
[LawfulMonad m]
{f : α → δ → m (ForInStep δ)}
{init : δ}
:
@[simp]
theorem
Std.ExtTreeMap.insertMany_nil
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
:
@[simp]
theorem
Std.ExtTreeMap.insertMany_list_singleton
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.insertMany_cons
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l : List (α × β)}
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.insertMany_append
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l₁ l₂ : List (α × β)}
:
@[simp]
theorem
Std.ExtTreeMap.contains_insertMany_list
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
{k : α}
:
theorem
Std.ExtTreeMap.mem_of_mem_insertMany_list
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
{k : α}
:
theorem
Std.ExtTreeMap.getKey?_insertMany_list_of_contains_eq_false
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
{k : α}
(contains_eq_false : (List.map Prod.fst l).contains k = false)
:
theorem
Std.ExtTreeMap.getKey?_insertMany_list_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.ExtTreeMap.getKey_insertMany_list_of_contains_eq_false
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
{k : α}
(contains_eq_false : (List.map Prod.fst l).contains k = false)
{h' : k ∈ t.insertMany l}
:
theorem
Std.ExtTreeMap.getKey_insertMany_list_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
{h' : k' ∈ t.insertMany l}
:
theorem
Std.ExtTreeMap.getKey!_insertMany_list_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[Inhabited α]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.ExtTreeMap.getKeyD_insertMany_list_of_contains_eq_false
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
{k fallback : α}
(contains_eq_false : (List.map Prod.fst l).contains k = false)
:
theorem
Std.ExtTreeMap.getKeyD_insertMany_list_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l : List (α × β)}
{k k' fallback : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.ExtTreeMap.size_insertMany_list
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
:
theorem
Std.ExtTreeMap.size_le_size_insertMany_list
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l : List (α × β)}
:
theorem
Std.ExtTreeMap.size_insertMany_list_le
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l : List (α × β)}
:
@[simp]
theorem
Std.ExtTreeMap.isEmpty_insertMany_list
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l : List (α × β)}
:
theorem
Std.ExtTreeMap.getElem?_insertMany_list_of_contains_eq_false
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
{k : α}
(contains_eq_false : (List.map Prod.fst l).contains k = false)
:
theorem
Std.ExtTreeMap.getElem?_insertMany_list_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
{v : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.ExtTreeMap.getElem?_insertMany_list
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
{k : α}
:
theorem
Std.ExtTreeMap.getElem_insertMany_list_of_contains_eq_false
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
{k : α}
(contains : (List.map Prod.fst l).contains k = false)
{h' : k ∈ t.insertMany l}
:
theorem
Std.ExtTreeMap.getElem_insertMany_list_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
{v : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
{h' : k' ∈ t.insertMany l}
:
theorem
Std.ExtTreeMap.getElem!_insertMany_list_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
{v : β}
[Inhabited β]
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.ExtTreeMap.getD_insertMany_list_of_contains_eq_false
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)}
{k : α}
{fallback : β}
(contains_eq_false : (List.map Prod.fst l).contains k = false)
:
theorem
Std.ExtTreeMap.getD_insertMany_list_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
{v fallback : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
@[simp]
theorem
Std.ExtTreeMap.insertManyIfNewUnit_nil
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
:
@[simp]
theorem
Std.ExtTreeMap.insertManyIfNewUnit_list_singleton
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{k : α}
:
theorem
Std.ExtTreeMap.insertManyIfNewUnit_cons
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
{k : α}
:
@[simp]
theorem
Std.ExtTreeMap.contains_insertManyIfNewUnit_list
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List α}
{k : α}
:
@[simp]
theorem
Std.ExtTreeMap.mem_insertManyIfNewUnit_list
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List α}
{k : α}
:
theorem
Std.ExtTreeMap.mem_of_mem_insertManyIfNewUnit_list
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List α}
{k : α}
(contains_eq_false : l.contains k = false)
:
k ∈ t.insertManyIfNewUnit l → k ∈ t
theorem
Std.ExtTreeMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List α}
{k : α}
(not_mem : ¬k ∈ t)
(contains_eq_false : l.contains k = false)
:
theorem
Std.ExtTreeMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(not_mem : ¬k ∈ t)
(distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l)
(mem : k ∈ l)
:
theorem
Std.ExtTreeMap.getKey?_insertManyIfNewUnit_list_of_mem
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
{k : α}
(mem : k ∈ t)
:
theorem
Std.ExtTreeMap.getKey_insertManyIfNewUnit_list_of_mem
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
{k : α}
{h' : k ∈ t.insertManyIfNewUnit l}
(contains : k ∈ t)
:
theorem
Std.ExtTreeMap.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
{h' : k' ∈ t.insertManyIfNewUnit l}
(not_mem : ¬k ∈ t)
(distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l)
(mem : k ∈ l)
:
theorem
Std.ExtTreeMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
[Inhabited α]
{l : List α}
{k : α}
(not_mem : ¬k ∈ t)
(contains_eq_false : l.contains k = false)
:
theorem
Std.ExtTreeMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
[Inhabited α]
{l : List α}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(not_mem : ¬k ∈ t)
(distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l)
(mem : k ∈ l)
:
theorem
Std.ExtTreeMap.getKey!_insertManyIfNewUnit_list_of_mem
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
[Inhabited α]
{l : List α}
{k : α}
(mem : k ∈ t)
:
theorem
Std.ExtTreeMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List α}
{k fallback : α}
(not_mem : ¬k ∈ t)
(contains_eq_false : l.contains k = false)
:
theorem
Std.ExtTreeMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
{k k' fallback : α}
(k_eq : cmp k k' = Ordering.eq)
(not_mem : ¬k ∈ t)
(distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l)
(mem : k ∈ l)
:
theorem
Std.ExtTreeMap.getKeyD_insertManyIfNewUnit_list_of_mem
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
{k fallback : α}
(mem : k ∈ t)
:
theorem
Std.ExtTreeMap.size_insertManyIfNewUnit_list
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List α}
(distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l)
:
theorem
Std.ExtTreeMap.size_le_size_insertManyIfNewUnit_list
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
:
theorem
Std.ExtTreeMap.size_insertManyIfNewUnit_list_le
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
:
@[simp]
theorem
Std.ExtTreeMap.isEmpty_insertManyIfNewUnit_list
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
:
@[simp]
theorem
Std.ExtTreeMap.getElem_insertManyIfNewUnit_list
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
{k : α}
{h' : k ∈ t.insertManyIfNewUnit l}
:
@[simp]
theorem
Std.ExtTreeMap.getElem!_insertManyIfNewUnit_list
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
{k : α}
:
@[simp]
theorem
Std.ExtTreeMap.getD_insertManyIfNewUnit_list
{α : Type u}
{cmp : α → α → Ordering}
{t : ExtTreeMap α Unit cmp}
[TransCmp cmp]
{l : List α}
{k : α}
{fallback : Unit}
:
theorem
Std.ExtTreeMap.getElem?_ofList_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
{v : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.ExtTreeMap.getElem_ofList_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
{v : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
{h : k' ∈ ofList l cmp}
:
theorem
Std.ExtTreeMap.getD_ofList_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
{v fallback : β}
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : (k, v) ∈ l)
:
theorem
Std.ExtTreeMap.getKey?_ofList_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.ExtTreeMap.getKey_ofList_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
{h' : k' ∈ ofList l cmp}
:
theorem
Std.ExtTreeMap.getKey!_ofList_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[TransCmp cmp]
[Inhabited α]
{l : List (α × β)}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
theorem
Std.ExtTreeMap.getKeyD_ofList_of_mem
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List (α × β)}
{k k' fallback : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l)
(mem : k ∈ List.map Prod.fst l)
:
@[simp]
@[simp]
theorem
Std.ExtTreeMap.unitOfList_singleton
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{k : α}
:
theorem
Std.ExtTreeMap.unitOfList_cons
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{hd : α}
{tl : List α}
:
@[simp]
theorem
Std.ExtTreeMap.contains_unitOfList
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List α}
{k : α}
:
@[simp]
theorem
Std.ExtTreeMap.mem_unitOfList
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List α}
{k : α}
:
theorem
Std.ExtTreeMap.getKey?_unitOfList_of_contains_eq_false
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List α}
{k : α}
(contains_eq_false : l.contains k = false)
:
theorem
Std.ExtTreeMap.getKey?_unitOfList_of_mem
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List α}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l)
(mem : k ∈ l)
:
theorem
Std.ExtTreeMap.getKey_unitOfList_of_mem
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List α}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l)
(mem : k ∈ l)
{h' : k' ∈ unitOfList l cmp}
:
theorem
Std.ExtTreeMap.getKey!_unitOfList_of_mem
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
[Inhabited α]
{l : List α}
{k k' : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l)
(mem : k ∈ l)
:
theorem
Std.ExtTreeMap.getKeyD_unitOfList_of_contains_eq_false
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
[BEq α]
[LawfulBEqCmp cmp]
{l : List α}
{k fallback : α}
(contains_eq_false : l.contains k = false)
:
theorem
Std.ExtTreeMap.getKeyD_unitOfList_of_mem
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List α}
{k k' fallback : α}
(k_eq : cmp k k' = Ordering.eq)
(distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l)
(mem : k ∈ l)
:
theorem
Std.ExtTreeMap.size_unitOfList
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List α}
(distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l)
:
theorem
Std.ExtTreeMap.size_unitOfList_le
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List α}
:
@[simp]
theorem
Std.ExtTreeMap.getElem_unitOfList
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List α}
{k : α}
{h : k ∈ unitOfList l cmp}
:
theorem
Std.ExtTreeMap.size_alter
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{f : Option β → Option β}
:
theorem
Std.ExtTreeMap.getKey!_alter
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[Inhabited α]
{k k' : α}
{f : Option β → Option β}
:
theorem
Std.ExtTreeMap.getKeyD_alter
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k k' fallback : α}
{f : Option β → Option β}
:
@[simp]
theorem
Std.ExtTreeMap.getD_modify_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{fallback : β}
{f : β → β}
:
theorem
Std.ExtTreeMap.minKey?_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.isSome_minKey?_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.minKey?_insertIfNew_le_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
{kmi : α}
(hkmi : (t.insertIfNew k v).minKey?.get ⋯ = kmi)
:
theorem
Std.ExtTreeMap.minKey?_modify
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{f : β → β}
:
(t.modify k f).minKey? = Option.map (fun (km : α) => if cmp km k = Ordering.eq then k else km) t.minKey?
@[simp]
theorem
Std.ExtTreeMap.minKey?_modify_eq_minKey?
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k : α}
{f : β → β}
:
theorem
Std.ExtTreeMap.minKey_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
(t.insertIfNew k v).minKey ⋯ = t.minKey?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'
theorem
Std.ExtTreeMap.minKey_insertIfNew_le_minKey
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
{he : t ≠ ∅}
:
theorem
Std.ExtTreeMap.minKey_insertIfNew_le_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.minKey_modify_eq_minKey
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k : α}
{f : β → β}
{he : t.modify k f ≠ ∅}
:
theorem
Std.ExtTreeMap.compare_minKey_modify_eq
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{f : β → β}
{he : t.modify k f ≠ ∅}
:
theorem
Std.ExtTreeMap.minKey!_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[Inhabited α]
{k : α}
{v : β}
:
(t.insertIfNew k v).minKey! = t.minKey?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'
theorem
Std.ExtTreeMap.minKey!_insertIfNew_le_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[Inhabited α]
{k : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.minKey!_modify_eq_minKey!
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
[Inhabited α]
{k : α}
{f : β → β}
:
theorem
Std.ExtTreeMap.compare_minKey!_modify_eq
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[Inhabited α]
{k : α}
{f : β → β}
:
@[simp]
theorem
Std.ExtTreeMap.ordCompare_minKey!_modify_eq
{α : Type u}
{β : Type v}
[Ord α]
[TransOrd α]
{t : ExtTreeMap α β compare}
[Inhabited α]
{k : α}
{f : β → β}
:
theorem
Std.ExtTreeMap.minKeyD_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
{fallback : α}
:
(t.insertIfNew k v).minKeyD fallback = t.minKey?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'
theorem
Std.ExtTreeMap.minKeyD_insertIfNew_le_minKeyD
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
(he : t ≠ ∅)
{k : α}
{v : β}
{fallback : α}
:
theorem
Std.ExtTreeMap.minKeyD_insertIfNew_le_self
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
{fallback : α}
:
@[simp]
theorem
Std.ExtTreeMap.minKeyD_modify_eq_minKeyD
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k : α}
{f : β → β}
{fallback : α}
:
theorem
Std.ExtTreeMap.compare_minKeyD_modify_eq
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{f : β → β}
{fallback : α}
:
@[simp]
theorem
Std.ExtTreeMap.ordCompare_minKeyD_modify_eq
{α : Type u}
{β : Type v}
[Ord α]
[TransOrd α]
{t : ExtTreeMap α β compare}
{k : α}
{f : β → β}
{fallback : α}
:
theorem
Std.ExtTreeMap.maxKey?_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.isSome_maxKey?_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
theorem
Std.ExtTreeMap.self_le_maxKey?_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
{kmi : α}
(hkmi : (t.insertIfNew k v).maxKey?.get ⋯ = kmi)
:
theorem
Std.ExtTreeMap.maxKey?_modify
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{f : β → β}
:
(t.modify k f).maxKey? = Option.map (fun (km : α) => if cmp km k = Ordering.eq then k else km) t.maxKey?
@[simp]
theorem
Std.ExtTreeMap.maxKey?_modify_eq_maxKey?
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k : α}
{f : β → β}
:
theorem
Std.ExtTreeMap.maxKey_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
(t.insertIfNew k v).maxKey ⋯ = t.maxKey?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'
theorem
Std.ExtTreeMap.maxKey_le_maxKey_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
{he : t ≠ ∅}
:
theorem
Std.ExtTreeMap.self_le_maxKey_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.maxKey_modify_eq_maxKey
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k : α}
{f : β → β}
{he : t.modify k f ≠ ∅}
:
theorem
Std.ExtTreeMap.compare_maxKey_modify_eq
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{f : β → β}
{he : t.modify k f ≠ ∅}
:
theorem
Std.ExtTreeMap.maxKey!_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[Inhabited α]
{k : α}
{v : β}
:
(t.insertIfNew k v).maxKey! = t.maxKey?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'
theorem
Std.ExtTreeMap.self_le_maxKey!_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[Inhabited α]
{k : α}
{v : β}
:
@[simp]
theorem
Std.ExtTreeMap.maxKey!_modify_eq_maxKey!
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
[Inhabited α]
{k : α}
{f : β → β}
:
theorem
Std.ExtTreeMap.compare_maxKey!_modify_eq
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[Inhabited α]
{k : α}
{f : β → β}
:
@[simp]
theorem
Std.ExtTreeMap.ordCompare_maxKey!_modify_eq
{α : Type u}
{β : Type v}
[Ord α]
[TransOrd α]
{t : ExtTreeMap α β compare}
[Inhabited α]
{k : α}
{f : β → β}
:
theorem
Std.ExtTreeMap.maxKeyD_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
{fallback : α}
:
(t.insertIfNew k v).maxKeyD fallback = t.maxKey?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'
theorem
Std.ExtTreeMap.maxKeyD_le_maxKeyD_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
(he : t ≠ ∅)
{k : α}
{v : β}
{fallback : α}
:
theorem
Std.ExtTreeMap.self_le_maxKeyD_insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{v : β}
{fallback : α}
:
@[simp]
theorem
Std.ExtTreeMap.maxKeyD_modify_eq_maxKeyD
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
[LawfulEqCmp cmp]
{k : α}
{f : β → β}
{fallback : α}
:
theorem
Std.ExtTreeMap.compare_maxKeyD_modify_eq
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : ExtTreeMap α β cmp}
[TransCmp cmp]
{k : α}
{f : β → β}
{fallback : α}
:
@[simp]
theorem
Std.ExtTreeMap.ordCompare_maxKeyD_modify_eq
{α : Type u}
{β : Type v}
[Ord α]
[TransOrd α]
{t : ExtTreeMap α β compare}
{k : α}
{f : β → β}
{fallback : α}
:
theorem
Std.ExtTreeMap.ext_contains_unit
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
[LawfulEqCmp cmp]
{t₁ t₂ : ExtTreeMap α Unit cmp}
(h : ∀ (k : α), t₁.contains k = t₂.contains k)
:
theorem
Std.ExtTreeMap.ext_mem_unit
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
[LawfulEqCmp cmp]
{t₁ t₂ : ExtTreeMap α Unit cmp}
(h : ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂)
: