Internal lemmas about the tree map #
This file contains internal lemmas about Std.DTreeMap.Internal.Impl. Users of the tree map should
not rely on the contents of this file.
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.tacticWf_trivial = Lean.ParserDescr.node `Std.DTreeMap.Internal.Impl.tacticWf_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "wf_trivial" false)
Instances For
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.tacticEmpty = Lean.ParserDescr.node `Std.DTreeMap.Internal.Impl.tacticEmpty 1024 (Lean.ParserDescr.nonReservedSymbol "empty" false)
Instances For
Internal implementation detail of the tree map
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ (insertIfNew k v t ⋯).impl → compare k a ≠ Ordering.eq → a ∈ t
theorem Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ insertIfNew! k v t → compare k a ≠ Ordering.eq → a ∈ t
theorem Std.DTreeMap.Internal.Impl.toList_insert_perm {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
theorem Std.DTreeMap.Internal.Impl.toList_insert!_perm {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
theorem Std.DTreeMap.Internal.Impl.toArray_insert_perm {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
theorem Std.DTreeMap.Internal.Impl.toArray_insert!_perm {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
theorem Std.DTreeMap.Internal.Impl.Const.toList_insert_perm {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} :
theorem Std.DTreeMap.Internal.Impl.Const.toList_insert!_perm {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} :
theorem Std.DTreeMap.Internal.Impl.Const.toArray_insert_perm {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} :
theorem Std.DTreeMap.Internal.Impl.Const.toArray_insert!_perm {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} :
theorem Std.DTreeMap.Internal.Impl.keysArray_insertIfNew_perm {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
theorem Std.DTreeMap.Internal.Impl.getD_empty {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] [LawfulEqOrd α] {a : α} {fallback : β a} :
theorem Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew' {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
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.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew!' {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
a ∈ insertIfNew! k v t → ¬(compare 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.DTreeMap.Internal.Impl.get_insertIfNew {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} {h₁ : a ∈ (insertIfNew k v t ⋯).impl} :
theorem Std.DTreeMap.Internal.Impl.get_insertIfNew! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} {h₁ : a ∈ insertIfNew! k v t} :
theorem Std.DTreeMap.Internal.Impl.get!_insertIfNew! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [Inhabited (β a)] {v : β k} :
theorem Std.DTreeMap.Internal.Impl.getD_insertIfNew {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} {v : β k} :
theorem Std.DTreeMap.Internal.Impl.getD_insertIfNew! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} {v : β k} :
theorem Std.DTreeMap.Internal.Impl.getKey_insertIfNew! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {k a : α} {v : β k} {h₁ : contains a (insertIfNew! k v t) = true} :
(insertIfNew! k v t).getKey a h₁ = if h₂ : compare k a = Ordering.eq ∧ ¬k ∈ t then k else t.getKey a ⋯
getThenInsertIfNew? #
theorem Std.DTreeMap.Internal.Impl.getThenInsertIfNew?_fst {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} :
theorem Std.DTreeMap.Internal.Impl.getThenInsertIfNew?_snd {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} :
getThenInsertIfNew?! #
theorem Std.DTreeMap.Internal.Impl.getThenInsertIfNew?!_fst {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} :
theorem Std.DTreeMap.Internal.Impl.getThenInsertIfNew?!_snd {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} :
getThenInsertIfNew? #
getThenInsertIfNew?! #
theorem Std.DTreeMap.Internal.Impl.distinct_keys {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) :
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) t.keys
theorem Std.DTreeMap.Internal.Impl.ordered_keys {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) :
List.Pairwise (fun (a b : α) => compare a b = Ordering.lt) t.keys
theorem Std.DTreeMap.Internal.Impl.find?_toList_eq_some_iff_get?_eq_some {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.find?_toArray_eq_some_iff_get?_eq_some {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.ordered_keys_toList {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) :
List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) t.toList
theorem Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_toList {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_toArray {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM_toList {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM_toArray {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_keys {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_keysArray {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldl_eq_foldl_keys {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {f : δ → α → δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldl_eq_foldl_keysArray {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {f : δ → α → δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM_keys {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM_keysArray {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldr_eq_foldr_keys {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {f : α → δ → δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.foldr_eq_foldr_keysArray {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {f : α → δ → δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.forM_eq_forM_keysArray {α : Type u} {β : α → Type v} {t : Impl α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → m PUnit} :
theorem Std.DTreeMap.Internal.Impl.forIn_eq_forIn_keys {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.forIn_eq_forIn_keysArray {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.Const.foldlM_eq_foldlM_toList {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Impl α fun (x : α) => β} [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.Const.foldlM_eq_foldlM_toArray {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Impl α fun (x : α) => β} [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.Const.foldrM_eq_foldrM_toList {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Impl α fun (x : α) => β} [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.Const.foldrM_eq_foldrM_toArray {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Impl α fun (x : α) => β} [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.Const.forIn_eq_forIn_toList {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Impl α fun (x : α) => β} [Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ} :
theorem Std.DTreeMap.Internal.Impl.Const.forIn_eq_forIn_toArray {α : Type u} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : Impl α fun (x : α) => β} [Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ} :
@[simp]
@[simp]
theorem Std.DTreeMap.Internal.Impl.contains_of_contains_insertMany_list {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} :
theorem Std.DTreeMap.Internal.Impl.contains_of_contains_insertMany!_list {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} :
theorem Std.DTreeMap.Internal.Impl.get?_insertMany_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.Internal.Impl.get?_insertMany!_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.Internal.Impl.get_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} (contains : (List.map Sigma.fst l).contains k = false) {h' : k ∈ (t.insertMany l ⋯).val} :
theorem Std.DTreeMap.Internal.Impl.get_insertMany!_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} (contains : (List.map Sigma.fst l).contains k = false) {h' : k ∈ (t.insertMany! l).val} :
theorem Std.DTreeMap.Internal.Impl.get_insertMany_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) {h' : k' ∈ (t.insertMany l ⋯).val} :
theorem Std.DTreeMap.Internal.Impl.get_insertMany!_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) {h' : k' ∈ (t.insertMany! l).val} :
theorem Std.DTreeMap.Internal.Impl.get!_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (h' : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.Internal.Impl.get!_insertMany!_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (h' : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.Internal.Impl.get!_insertMany_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.Internal.Impl.get!_insertMany!_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.Internal.Impl.getD_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.Internal.Impl.getD_insertMany!_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.Internal.Impl.getD_insertMany_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.Internal.Impl.getD_insertMany!_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.Internal.Impl.getKey?_insertMany_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.Internal.Impl.getKey?_insertMany!_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.Internal.Impl.getKey_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} (h₁ : (List.map Sigma.fst l).contains k = false) {h' : contains k (t.insertMany l ⋯).val = true} :
theorem Std.DTreeMap.Internal.Impl.getKey_insertMany!_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} (h₁ : (List.map Sigma.fst l).contains k = false) {h' : contains k (t.insertMany! l).val = true} :
theorem Std.DTreeMap.Internal.Impl.getKey_insertMany_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) {h' : contains k' (t.insertMany l ⋯).val = true} :
theorem Std.DTreeMap.Internal.Impl.getKey_insertMany!_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) {h' : contains k' (t.insertMany! l).val = true} :
theorem Std.DTreeMap.Internal.Impl.getKey!_insertMany_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [Inhabited α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.Internal.Impl.getKey!_insertMany!_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [Inhabited α] (h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.Internal.Impl.getKeyD_insertMany_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' fallback : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.Internal.Impl.getKeyD_insertMany!_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k k' fallback : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.Internal.Impl.size_insertMany_list {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) :
theorem Std.DTreeMap.Internal.Impl.size_insertMany!_list {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) :
@[simp]
@[simp]
theorem Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany!_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKey_insertMany_list_of_contains_eq_false {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α} (h₁ : (List.map Prod.fst l).contains k = false) {h' : contains k (insertMany t l ⋯).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.getKey_insertMany!_list_of_contains_eq_false {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α} (h₁ : (List.map Prod.fst l).contains k = false) {h' : contains k (insertMany! t l).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.getKey_insertMany_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) {h' : contains k' (insertMany t l ⋯).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.getKey_insertMany!_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) {h' : contains k' (insertMany! t l).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany!_list_of_contains_eq_false {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] (h : t.WF) {l : List (α × β)} {k : α} (h' : (List.map Prod.fst l).contains k = false) :
theorem Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [Inhabited α] (h : t.WF) {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany!_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [Inhabited α] (h : t.WF) {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' fallback : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany!_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' fallback : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Internal.Impl.Const.size_insertMany_list {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) :
theorem Std.DTreeMap.Internal.Impl.Const.size_insertMany!_list {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) :
theorem Std.DTreeMap.Internal.Impl.Const.get?_insertMany_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.get?_insertMany!_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.get_insertMany_list_of_contains_eq_false {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α} (h₁ : (List.map Prod.fst l).contains k = false) {h' : contains k (insertMany t l ⋯).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.get_insertMany!_list_of_contains_eq_false {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α} (h₁ : (List.map Prod.fst l).contains k = false) {h' : contains k (insertMany! t l).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.get_insertMany_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) {h' : contains k' (insertMany t l ⋯).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.get_insertMany!_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) {h' : contains k' (insertMany! t l).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.contains_of_contains_insertMany_list' {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α} (h' : contains k (insertMany t l ⋯).val = true) (w :
List.findSomeRev?
(fun (x : α × β) =>
match x with
| (a, b) => if compare a k = Ordering.eq then some b else none)
l = none) :
A variant of contains_of_contains_insertMany_list used in get_insertMany_list.
theorem Std.DTreeMap.Internal.Impl.Const.get!_insertMany_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [Inhabited β] (h : t.WF) {l : List (α × β)} {k k' : α} {v : β} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.get!_insertMany!_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] [Inhabited β] (h : t.WF) {l : List (α × β)} {k k' : α} {v : β} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.getD_insertMany_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' : α} {v fallback : β} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.getD_insertMany!_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} [TransOrd α] (h : t.WF) {l : List (α × β)} {k k' : α} {v fallback : β} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α} :
theorem Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α} :
theorem Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] (h : t.WF) {l : List α} {k k' : α} (k_beq : compare k k' = Ordering.eq) :
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit t l ⋯).val.getKey? k' = some k
theorem Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit!_list_of_not_mem_of_mem {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] (h : t.WF) {l : List α} {k k' : α} (k_beq : compare k k' = Ordering.eq) :
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit! t l).val.getKey? k' = some k
theorem Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] (h : t.WF) {l : List α} {k k' : α} (k_beq : compare k k' = Ordering.eq) {h' : contains k' (insertManyIfNewUnit t l ⋯).val = true} :
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit t l ⋯).val.getKey k' h' = k
theorem Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit!_list_of_not_mem_of_mem {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] (h : t.WF) {l : List α} {k k' : α} (k_beq : compare k k' = Ordering.eq) {h' : contains k' (insertManyIfNewUnit! t l).val = true} :
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit! t l).val.getKey k' h' = k
theorem Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] [Inhabited α] (h : t.WF) {l : List α} {k k' : α} (k_beq : compare k k' = Ordering.eq) :
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l → k ∈ l → (insertManyIfNewUnit t l ⋯).val.getKey! k' = k
theorem Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit!_list_of_not_mem_of_mem {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] [Inhabited α] (h : t.WF) {l : List α} {k k' : α} (k_beq : compare k k' = Ordering.eq) :
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l → k ∈ l → (insertManyIfNewUnit! t l).val.getKey! k' = k
theorem Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [BEq α] [LawfulBEqOrd α] [TransOrd α] (h : t.WF) {l : List α} {k fallback : α} :
theorem Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [BEq α] [LawfulBEqOrd α] [TransOrd α] (h : t.WF) {l : List α} {k fallback : α} :
theorem Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] (h : t.WF) {l : List α} {k k' fallback : α} (k_beq : compare k k' = Ordering.eq) :
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit t l ⋯).val.getKeyD k' fallback = k
theorem Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit!_list_of_not_mem_of_mem {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] (h : t.WF) {l : List α} {k k' fallback : α} (k_beq : compare k k' = Ordering.eq) :
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l →
k ∈ l → (insertManyIfNewUnit! t l).val.getKeyD k' fallback = k
theorem Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit_list {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l) :
theorem Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit!_list {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l) :
theorem Std.DTreeMap.Internal.Impl.Const.get?_insertManyIfNewUnit_list {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α} :
theorem Std.DTreeMap.Internal.Impl.Const.get?_insertManyIfNewUnit!_list {α : Type u} {instOrd : Ord α} {t : Impl α fun (x : α) => Unit} [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α} :
theorem Std.DTreeMap.Internal.Impl.Const.unitOfList_eq_insertManyIfNewUnit {α : Type u} {instOrd : Ord α} {l : List α} :
theorem Std.DTreeMap.Internal.Impl.Const.unitOfList_eq_insertManyIfNewUnit! {α : Type u} {instOrd : Ord α} {l : List α} :
theorem Std.DTreeMap.Internal.Impl.get?_insertMany_empty_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} {k : α} (h : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.Internal.Impl.get?_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.Internal.Impl.get_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) {h : k' ∈ (empty.insertMany l ⋯).val} :
theorem Std.DTreeMap.Internal.Impl.get!_insertMany_empty_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (h : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.Internal.Impl.get!_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.Internal.Impl.getD_insertMany_empty_list_of_contains_eq_false {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.Internal.Impl.getD_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] [LawfulEqOrd α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.Internal.Impl.getKey?_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.Internal.Impl.getKey_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) {h' : contains k' (empty.insertMany l ⋯).val = true} :
theorem Std.DTreeMap.Internal.Impl.getKey!_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.Internal.Impl.getKeyD_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] {l : List ((a : α) × β a)} {k k' fallback : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.Internal.Impl.size_insertMany_empty_list {α : Type u} {β : α → Type v} {instOrd : Ord α} [TransOrd α] {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬compare a.fst b.fst = Ordering.eq) l) :
theorem Std.DTreeMap.Internal.Impl.Const.get?_insertMany_empty_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} [TransOrd α] {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.get_insertMany_empty_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} [TransOrd α] {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) {h : contains k' (insertMany empty l ⋯).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.get!_insertMany_empty_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} [TransOrd α] {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β} [Inhabited β] (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.getD_insertMany_empty_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} [TransOrd α] {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v fallback : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany_empty_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} [TransOrd α] {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKey_insertMany_empty_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} [TransOrd α] {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) {h' : contains k' (insertMany empty l ⋯).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany_empty_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} [TransOrd α] [Inhabited α] {l : List (α × β)} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany_empty_list_of_mem {α : Type u} {instOrd : Ord α} {β : Type v} [TransOrd α] {l : List (α × β)} {k k' fallback : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬compare a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
@[simp]
theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_empty_list_singleton {α : Type u} {instOrd : Ord α} {k : α} :
theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_empty_list_cons {α : Type u} {instOrd : Ord α} {hd : α} {tl : List α} :
(insertManyIfNewUnit empty (hd :: tl) ⋯).val = (insertManyIfNewUnit (insertIfNew hd () empty ⋯).impl tl ⋯).val
theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_empty_list_cons_eq_insertManyIfNewUnit! {α : Type u} {instOrd : Ord α} {hd : α} {tl : List α} :
(insertManyIfNewUnit empty (hd :: tl) ⋯).val = (insertManyIfNewUnit! (insertIfNew! hd () empty) tl).val
theorem Std.DTreeMap.Internal.Impl.Const.contains_insertManyIfNewUnit_empty_list {α : Type u} {instOrd : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List α} {k : α} :
theorem Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem {α : Type u} {instOrd : Ord α} [TransOrd α] {l : List α} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l) (mem : k ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKey_insertManyIfNewUnit_empty_list_of_mem {α : Type u} {instOrd : Ord α} [TransOrd α] {l : List α} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l) (mem : k ∈ l) {h' : contains k' (insertManyIfNewUnit empty l ⋯).val = true} :
theorem Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem {α : Type u} {instOrd : Ord α} [TransOrd α] [Inhabited α] {l : List α} {k k' : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l) (mem : k ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false {α : Type u} {instOrd : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List α} {k fallback : α} (h' : l.contains k = false) :
theorem Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem {α : Type u} {instOrd : Ord α} [TransOrd α] {l : List α} {k k' fallback : α} (k_beq : compare k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l) (mem : k ∈ l) :
theorem Std.DTreeMap.Internal.Impl.Const.size_insertManyIfNewUnit_empty_list {α : Type u} {instOrd : Ord α} [TransOrd α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬compare a b = Ordering.eq) l) :
@[simp]
@[simp]
theorem Std.DTreeMap.Internal.Impl.contains_alter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.contains_alter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.contains_alter_of_not_compare_eq {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)} (he : ¬compare k k' = Ordering.eq) :
theorem Std.DTreeMap.Internal.Impl.size_alter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.size_alter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.get?_alter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.getD_alter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.getD_alter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.getKey?_alter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.getKey?_alter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.getKeyD_alter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' fallback : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.getKeyD_alter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' fallback : α} {f : Option (β k) → Option (β k)} :
@[simp]
theorem Std.DTreeMap.Internal.Impl.get?_modify {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {f : β k → β k} :
(modify k f t).get? k' = if h : compare k k' = Ordering.eq then cast ⋯ (Option.map f (t.get? k)) else t.get? k'
@[simp]
theorem Std.DTreeMap.Internal.Impl.get?_modify_self {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {f : β k → β k} :
theorem Std.DTreeMap.Internal.Impl.get_modify {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {f : β k → β k} {hc : k' ∈ modify k f t} :
theorem Std.DTreeMap.Internal.Impl.get!_modify {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
(modify k f t).get! k' = if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).get! else t.get! k'
theorem Std.DTreeMap.Internal.Impl.getD_modify {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' : α} {fallback : β k'} {f : β k → β k} :
(modify k f t).getD k' fallback = if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).getD fallback
else t.getD k' fallback
@[simp]
theorem Std.DTreeMap.Internal.Impl.getD_modify_self {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {fallback : β k} {f : β k → β k} :
theorem Std.DTreeMap.Internal.Impl.getKey!_modify {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) [Inhabited α] {k k' : α} {f : β k → β k} :
theorem Std.DTreeMap.Internal.Impl.getKeyD_modify {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k k' fallback : α} {f : β k → β k} :
theorem Std.DTreeMap.Internal.Impl.min?_keys {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [Min α] [LE α] [LawfulOrderOrd α] [LawfulOrderMin α] [LawfulOrderLeftLeaningMin α] [LawfulEqOrd α] (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.head?_keys {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [Min α] [LE α] [LawfulOrderOrd α] [LawfulOrderMin α] [LawfulOrderLeftLeaningMin α] [LawfulEqOrd α] (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.minKey?_alter_eq_self {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.minKey?_alter!_eq_self {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.maxKey?_alter_eq_self {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.maxKey?_alter!_eq_self {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Internal.Impl.Equiv.insert {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {v : β k} :
(Impl.insert k v t₁ ⋯).impl.Equiv (Impl.insert k v t₂ ⋯).impl
theorem Std.DTreeMap.Internal.Impl.Equiv.insert! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {v : β k} :
(Impl.insert! k v t₁).Equiv (Impl.insert! k v t₂)
theorem Std.DTreeMap.Internal.Impl.Equiv.erase {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} :
(Impl.erase k t₁ ⋯).impl.Equiv (Impl.erase k t₂ ⋯).impl
theorem Std.DTreeMap.Internal.Impl.Equiv.erase! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} :
(Impl.erase! k t₁).Equiv (Impl.erase! k t₂)
theorem Std.DTreeMap.Internal.Impl.Equiv.insertIfNew {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {v : β k} :
(Impl.insertIfNew k v t₁ ⋯).impl.Equiv (Impl.insertIfNew k v t₂ ⋯).impl
theorem Std.DTreeMap.Internal.Impl.Equiv.insertIfNew! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {v : β k} :
(Impl.insertIfNew! k v t₁).Equiv (Impl.insertIfNew! k v t₂)
theorem Std.DTreeMap.Internal.Impl.Equiv.alter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} [TransOrd α] [LawfulEqOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {f : Option (β k) → Option (β k)} :
(Impl.alter k f t₁ ⋯).impl.Equiv (Impl.alter k f t₂ ⋯).impl
theorem Std.DTreeMap.Internal.Impl.Equiv.alter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} [TransOrd α] [LawfulEqOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {f : Option (β k) → Option (β k)} :
(Impl.alter! k f t₁).Equiv (Impl.alter! k f t₂)
theorem Std.DTreeMap.Internal.Impl.Equiv.modify {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} [TransOrd α] [LawfulEqOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {f : β k → β k} :
(Impl.modify k f t₁).Equiv (Impl.modify k f t₂)
theorem Std.DTreeMap.Internal.Impl.Equiv.filter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {f : (a : α) → β a → Bool} :
(Impl.filter f t₁ ⋯).impl.Equiv (Impl.filter f t₂ ⋯).impl
theorem Std.DTreeMap.Internal.Impl.Equiv.filter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {f : (a : α) → β a → Bool} :
(Impl.filter! f t₁).Equiv (Impl.filter! f t₂)
theorem Std.DTreeMap.Internal.Impl.Equiv.filterMap! {α : Type u} {β : α → Type v} {γ : α → Type w} {instOrd : Ord α} {t₁ t₂ : Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {f : (a : α) → β a → Option (γ a)} :
(Impl.filterMap! f t₁).Equiv (Impl.filterMap! f t₂)
theorem Std.DTreeMap.Internal.Impl.Equiv.mergeWith {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ t₃ t₄ : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t₁.Equiv t₂) (h' : t₃.Equiv t₄) (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) {f : (a : α) → β a → β a → β a} :
(Impl.mergeWith f t₁ t₃ ⋯).impl.Equiv (Impl.mergeWith f t₂ t₄ ⋯).impl
theorem Std.DTreeMap.Internal.Impl.Equiv.mergeWith! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ t₃ t₄ : Impl α β} [TransOrd α] [LawfulEqOrd α] (h : t₁.Equiv t₂) (h' : t₃.Equiv t₄) (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) {f : (a : α) → β a → β a → β a} :
(Impl.mergeWith! f t₁ t₃).Equiv (Impl.mergeWith! f t₂ t₄)
theorem Std.DTreeMap.Internal.Impl.Equiv.constAlter! {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Impl α fun (x : α) => β} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {f : Option β → Option β} :
(Const.alter! k f t₁).Equiv (Const.alter! k f t₂)
theorem Std.DTreeMap.Internal.Impl.Equiv.constModify {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Impl α fun (x : α) => β} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {f : β → β} :
(Const.modify k f t₁).Equiv (Const.modify k f t₂)
theorem Std.DTreeMap.Internal.Impl.Equiv.constMergeWith {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ t₃ t₄ : Impl α fun (x : α) => β} [TransOrd α] (h : t₁.Equiv t₂) (h' : t₃.Equiv t₄) (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) {f : α → β → β → β} :
(Const.mergeWith f t₁ t₃ ⋯).impl.Equiv (Const.mergeWith f t₂ t₄ ⋯).impl
theorem Std.DTreeMap.Internal.Impl.Equiv.constMergeWith! {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ t₃ t₄ : Impl α fun (x : α) => β} [TransOrd α] (h : t₁.Equiv t₂) (h' : t₃.Equiv t₄) (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) {f : α → β → β → β} :
(Const.mergeWith! f t₁ t₃).Equiv (Const.mergeWith! f t₂ t₄)
theorem Std.DTreeMap.Internal.Impl.Equiv.of_forall_constGet?_eq {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Impl α fun (x : α) => β} [TransOrd α] [LawfulEqOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) :
(∀ (k : α), Const.get? t₁ k = Const.get? t₂ k) → t₁.Equiv t₂
theorem Std.DTreeMap.Internal.Impl.insertMany!_list_equiv_foldl {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ : Impl α β} {l : List ((a : α) × β a)} :
(t₁.insertMany! l).val.Equiv (List.foldl (fun (acc : Impl α β) (p : (a : α) × β a) => insert! p.fst p.snd acc) t₁ l)
theorem Std.DTreeMap.Internal.Impl.insertManyIfNew_list_equiv_foldl {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ : Impl α β} {l : List ((a : α) × β a)} (h : t₁.WF) :
(t₁.insertManyIfNew l ⋯).val.Equiv
(List.foldl (fun (acc : Impl α β) (p : (a : α) × β a) => insertIfNew! p.fst p.snd acc) t₁ l)
theorem Std.DTreeMap.Internal.Impl.insertManyIfNew!_list_equiv_foldl {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ : Impl α β} {l : List ((a : α) × β a)} :
(t₁.insertManyIfNew! l).val.Equiv
(List.foldl (fun (acc : Impl α β) (p : (a : α) × β a) => insertIfNew! p.fst p.snd acc) t₁ l)
theorem Std.DTreeMap.Internal.Impl.Const.insertMany_list_equiv_foldl {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ : Impl α fun (x : α) => β} {l : List (α × β)} (h : t₁.WF) :
(insertMany t₁ l ⋯).val.Equiv
(List.foldl (fun (acc : Impl α fun (x : α) => β) (p : α × β) => insert! p.fst p.snd acc) t₁ l)
theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_list_equiv_foldl {α : Type u} {instOrd : Ord α} {t₁ : Impl α fun (x : α) => Unit} {l : List α} (h : t₁.WF) :
(insertManyIfNewUnit t₁ l ⋯).val.Equiv
(List.foldl (fun (acc : Impl α fun (a : α) => Unit) (a : α) => insertIfNew! a () acc) t₁ l)
theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit!_list_equiv_foldl {α : Type u} {instOrd : Ord α} {t₁ : Impl α fun (x : α) => Unit} {l : List α} :
(insertManyIfNewUnit! t₁ l).val.Equiv
(List.foldl (fun (acc : Impl α fun (a : α) => Unit) (a : α) => insertIfNew! a () acc) t₁ l)
theorem Std.DTreeMap.Internal.Impl.toList_filterMap! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
(filterMap! f t).toList = List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
theorem Std.DTreeMap.Internal.Impl.toArray_filterMap! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
(filterMap! f t).toArray = Array.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : γ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toArray
theorem Std.DTreeMap.Internal.Impl.isEmpty_filterMap_iff {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.isEmpty_filterMap!_iff {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.isEmpty_filterMap_eq_false_iff {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.isEmpty_filterMap!_eq_false_iff {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.contains_filterMap {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.contains_filterMap! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.size_filterMap_eq_size_iff {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.size_filterMap!_eq_size_iff {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.isSome_apply_of_contains_filterMap! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF) (h' : contains k (filterMap! f t) = true) :
theorem Std.DTreeMap.Internal.Impl.get_filterMap! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF) {h' : k ∈ filterMap! f t} :
theorem Std.DTreeMap.Internal.Impl.getD_filterMap {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.getD_filterMap! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} {fallback : γ k} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.getKey?_filterMap {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.getKey?_filterMap! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.getKeyD_filterMap {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k fallback : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.getKeyD_filterMap! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k fallback : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.Const.toList_filterMap! {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Impl α fun (x : α) => β} {f : α → β → Option γ} (h : t.WF) :
toList (filterMap! f t) = List.filterMap (fun (p : α × β) => Option.map (fun (x : γ) => (p.fst, x)) (f p.fst p.snd)) (toList t)
theorem Std.DTreeMap.Internal.Impl.Const.toArray_filterMap! {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Impl α fun (x : α) => β} {f : α → β → Option γ} (h : t.WF) :
toArray (filterMap! f t) = Array.filterMap (fun (p : α × β) => Option.map (fun (x : γ) => (p.fst, x)) (f p.fst p.snd)) (toArray t)
theorem Std.DTreeMap.Internal.Impl.filterMap!_equiv_filter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {f : (a : α) → β a → Bool} (h : t.WF) :
(filterMap! (fun (k : α) => Option.guard fun (v : β k) => f k v) t).Equiv (filter! f t)
theorem Std.DTreeMap.Internal.Impl.contains_filter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.get?_filter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.keys_filter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.keysArray_filter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.keys_filter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.keysArray_filter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.getKey?_filter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.getKey!_filter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] [Inhabited α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.getKey!_filter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] [Inhabited α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.getKeyD_filter {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} {k fallback : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.getKeyD_filter! {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} {k fallback : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.get?_map {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} {γ : α → Type w} [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → γ a} {k : α} (h : t.WF) :
theorem Std.DTreeMap.Internal.Impl.Const.get?_map {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Impl α fun (x : α) => β} [TransOrd α] [LawfulEqOrd α] {f : α → β → γ} {k : α} (h : t.WF) :
def Std.DTreeMap.Internal.Impl.decidableEquiv {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [(k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)] (t₁ t₂ : Impl α β) (h₁ : t₁.WF) (h₂ : t₂.WF) :
Internal implementation detail
Equations
- t₁.decidableEquiv t₂ h₁ h₂ = decidable_of_iff (t₁.beq t₂ = true) ⋯