Dependent hash map lemmas #
This file contains lemmas about Std.Data.DHashMap.Raw. Most of the lemmas require
EquivBEq α and LawfulHashable α for the key type α. The easiest way to obtain these instances
is to provide an instance of LawfulBEq α.
Internal implementation detail of the hash map
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem Std.DHashMap.Raw.getKey?_beq {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
@[simp]
theorem Std.DHashMap.Raw.isEmpty_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
theorem Std.DHashMap.Raw.contains_insertIfNew_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
theorem Std.DHashMap.Raw.mem_insertIfNew_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
theorem Std.DHashMap.Raw.contains_of_contains_insertIfNew' {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
This is a restatement of contains_of_contains_insertIfNew that is written to exactly match the proof
obligation in the statement of get_insertIfNew.
theorem Std.DHashMap.Raw.mem_of_mem_insertIfNew' {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.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.DHashMap.Raw.size_le_size_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
theorem Std.DHashMap.Raw.size_insertIfNew_le {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
theorem Std.DHashMap.Raw.distinct_keys {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
List.Pairwise (fun (a b : α) => (a == b) = false) m.keys
theorem Std.DHashMap.Raw.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} {v : β} :
theorem Std.DHashMap.Raw.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} {v : β} :
@[simp]
theorem Std.DHashMap.Raw.forIn_eq_forIn {α : Type u} {β : α → Type v} {m : Raw α β} {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} :
@[simp]
theorem Std.DHashMap.Raw.Const.forIn_eq_forInUncurried {α : Type u} {δ : Type w} {m' : Type w → Type w'} {β : Type v} {m : Raw α fun (x : α) => β} [Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ} :
theorem Std.DHashMap.Raw.Const.any_eq_true_iff_exists_contains_getKey_get {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [LawfulHashable α] [EquivBEq α] {p : α → β → Bool} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.any_eq_false_iff_forall_contains_getKey_get {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [LawfulHashable α] [EquivBEq α] {p : α → β → Bool} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.all_eq_true_iff_forall_contains_getKey_get {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {p : α → β → Bool} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.all_eq_false_iff_exists_contains_getKey_get {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {p : α → β → Bool} (h : m.WF) :
@[simp]
theorem Std.DHashMap.Raw.insertMany_nil {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
theorem Std.DHashMap.Raw.insertMany_cons {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] {l : List ((a : α) × β a)} {k : α} {v : β k} [EquivBEq α] [LawfulHashable α] (h : m.WF) :
theorem Std.DHashMap.Raw.insertMany_append {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l₁ l₂ : List ((a : α) × β a)} :
theorem Std.DHashMap.Raw.insertMany_ind {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {motive : Raw α β → Prop} (m : Raw α β) (l : ρ) (init : motive m) (insert : ∀ (m : Raw α β) (a : α) (b : β a), motive m → motive (m.insert a b)) :
motive (m.insertMany l)
theorem Std.DHashMap.Raw.get?_insertMany_list_of_mem {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DHashMap.Raw.get_insertMany_list_of_mem {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) {h' : k' ∈ m.insertMany l} :
theorem Std.DHashMap.Raw.get!_insertMany_list_of_mem {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DHashMap.Raw.getD_insertMany_list_of_mem {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DHashMap.Raw.getKey?_insertMany_list_of_mem {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DHashMap.Raw.getKey_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h' : k ∈ m.insertMany l} :
theorem Std.DHashMap.Raw.getKey_insertMany_list_of_mem {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) {h' : k' ∈ m.insertMany l} :
theorem Std.DHashMap.Raw.getKey!_insertMany_list_of_mem {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DHashMap.Raw.getKeyD_insertMany_list_of_mem {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List ((a : α) × β a)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DHashMap.Raw.size_le_size_insertMany_list {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List ((a : α) × β a)} :
@[deprecated Std.DHashMap.Raw.union_insert_right_equiv_insert_union (since := "2025-11-03")]
theorem Std.DHashMap.Raw.Const.insertMany_ind {α : Type u} [BEq α] [Hashable α] {β : Type v} {ρ : Type w} [ForIn Id ρ (α × β)] {motive : (Raw α fun (x : α) => β) → Prop} (m : Raw α fun (x : α) => β) (l : ρ) (init : motive m) (insert : ∀ (m : Raw α fun (x : α) => β) (a : α) (b : β), motive m → motive (m.insert a b)) :
motive (insertMany m l)
theorem Std.DHashMap.Raw.Const.getKey?_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DHashMap.Raw.Const.getKey_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ insertMany m l} :
theorem Std.DHashMap.Raw.Const.getKey_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) {h' : k' ∈ insertMany m l} :
theorem Std.DHashMap.Raw.Const.getKey!_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.DHashMap.Raw.Const.getKey!_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DHashMap.Raw.Const.getKeyD_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DHashMap.Raw.Const.get?_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) :
theorem Std.DHashMap.Raw.Const.get_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ insertMany m l} :
theorem Std.DHashMap.Raw.Const.get_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) {h' : k' ∈ insertMany m l} :
theorem Std.DHashMap.Raw.Const.get!_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) :
theorem Std.DHashMap.Raw.Const.getD_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v fallback : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) :
theorem Std.DHashMap.Raw.Const.insertManyIfNewUnit_ind {α : Type u} [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ α] {motive : (Raw α fun (x : α) => Unit) → Prop} (m : Raw α fun (x : α) => Unit) (l : ρ) (init : motive m) (insert : ∀ (m : Raw α fun (x : α) => Unit) (a : α), motive m → motive (m.insertIfNew a ())) :
motive (insertManyIfNewUnit m l)
theorem Std.DHashMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} :
theorem Std.DHashMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_mem {α : Type u} [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} {h' : k ∈ insertManyIfNewUnit m l} (mem : k ∈ m) :
theorem Std.DHashMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k k' : α} (k_beq : (k == k') = true) {h' : k' ∈ insertManyIfNewUnit m l} :
¬k ∈ m → List.Pairwise (fun (a b : α) => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey k' h' = k
theorem Std.DHashMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List α} {k k' : α} (k_beq : (k == k') = true) :
¬k ∈ m → List.Pairwise (fun (a b : α) => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey! k' = k
theorem Std.DHashMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k fallback : α} :
theorem Std.DHashMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) :
¬k ∈ m → List.Pairwise (fun (a b : α) => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKeyD k' fallback = k
theorem Std.DHashMap.Raw.Const.size_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :
theorem Std.DHashMap.Raw.Const.size_le_size_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} :
@[simp]
theorem Std.DHashMap.Raw.Const.get_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} {l : List α} {k : α} {h : k ∈ insertManyIfNewUnit m l} :
theorem Std.DHashMap.Raw.get_ofList_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) {h : k' ∈ ofList l} :
theorem Std.DHashMap.Raw.get!_ofList_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DHashMap.Raw.getD_ofList_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DHashMap.Raw.getKey?_ofList_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DHashMap.Raw.getKey_ofList_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) {h' : k' ∈ ofList l} :
theorem Std.DHashMap.Raw.getKey!_ofList_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DHashMap.Raw.getKeyD_ofList_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DHashMap.Raw.Const.get_ofList_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) {h : k' ∈ ofList l} :
theorem Std.DHashMap.Raw.Const.get!_ofList_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} [Inhabited β] (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) :
theorem Std.DHashMap.Raw.Const.getD_ofList_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v fallback : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) :
theorem Std.DHashMap.Raw.Const.getKey_ofList_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) {h' : k' ∈ ofList l} :
theorem Std.DHashMap.Raw.Const.getKey!_ofList_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DHashMap.Raw.Const.getKeyD_ofList_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) :
@[simp]
theorem Std.DHashMap.Raw.Const.unitOfArray_eq_unitOfList {α : Type u} [BEq α] [Hashable α] (a : Array α) :
@[simp]
@[simp]
theorem Std.DHashMap.Raw.Const.unitOfList_cons {α : Type u} [BEq α] [Hashable α] {hd : α} {tl : List α} :
theorem Std.DHashMap.Raw.Const.unitOfList_eq_insertManyIfNewUnit_empty {α : Type u} [BEq α] [Hashable α] {l : List α} :
@[simp]
theorem Std.DHashMap.Raw.Const.contains_unitOfList {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
@[simp]
theorem Std.DHashMap.Raw.Const.mem_unitOfList {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
theorem Std.DHashMap.Raw.Const.getKey?_unitOfList_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
theorem Std.DHashMap.Raw.Const.getKey?_unitOfList_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :
theorem Std.DHashMap.Raw.Const.getKey_unitOfList_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) {h' : k' ∈ unitOfList l} :
theorem Std.DHashMap.Raw.Const.getKeyD_unitOfList_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (contains_eq_false : l.contains k = false) :
theorem Std.DHashMap.Raw.Const.getKeyD_unitOfList_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :
theorem Std.DHashMap.Raw.Const.size_unitOfList {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :
theorem Std.DHashMap.Raw.Const.size_unitOfList_le {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} :
@[simp]
theorem Std.DHashMap.Raw.Const.isEmpty_unitOfList {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} :
@[simp]
theorem Std.DHashMap.Raw.Const.get_unitOfList {α : Type u} [BEq α] [Hashable α] {l : List α} {k : α} {h : k ∈ unitOfList l} :
@[simp]
@[simp]
@[simp]
theorem Std.DHashMap.Raw.Const.get?_modify_self {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.getD_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.getKey!_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.getKeyD_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} (h : m.WF) :
theorem Std.DHashMap.Raw.Equiv.constToList_perm {α : Type u} {β : Type v} {m₁ m₂ : Raw α fun (x : α) => β} (h : m₁.Equiv m₂) :
(Const.toList m₁).Perm (Const.toList m₂)
theorem Std.DHashMap.Raw.Equiv.of_constToList_perm {α : Type u} {β : Type v} {m₁ m₂ : Raw α fun (x : α) => β} (h : (Const.toList m₁).Perm (Const.toList m₂)) :
m₁.Equiv m₂
theorem Std.DHashMap.Raw.Equiv.insertIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m₁ m₂ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (k : α) (v : β k) (h : m₁.Equiv m₂) :
(m₁.insertIfNew k v).Equiv (m₂.insertIfNew k v)
theorem Std.DHashMap.Raw.Equiv.insertMany_list {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m₁ m₂ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (l : List ((a : α) × β a)) (h : m₁.Equiv m₂) :
(m₁.insertMany l).Equiv (m₂.insertMany l)
theorem Std.DHashMap.Raw.Equiv.filter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (f : (a : α) → β a → Bool) (h : m₁.Equiv m₂) :
(Raw.filter f m₁).Equiv (Raw.filter f m₂)
theorem Std.DHashMap.Raw.Equiv.filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (f : (a : α) → β a → Option (γ a)) (h : m₁.Equiv m₂) :
(Raw.filterMap f m₁).Equiv (Raw.filterMap f m₂)
theorem Std.DHashMap.Raw.Equiv.constInsertMany_list {α : Type u} [BEq α] [Hashable α] {β : Type v} {m₁ m₂ : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (l : List (α × β)) (h : m₁.Equiv m₂) :
(Const.insertMany m₁ l).Equiv (Const.insertMany m₂ l)
theorem Std.DHashMap.Raw.Equiv.constInsertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw α fun (x : α) => Unit} (h₁ : m₁.WF) (h₂ : m₂.WF) (l : List α) (h : m₁.Equiv m₂) :
(Const.insertManyIfNewUnit m₁ l).Equiv (Const.insertManyIfNewUnit m₂ l)
theorem Std.DHashMap.Raw.Equiv.constAlter {α : Type u} [BEq α] [Hashable α] {β : Type v} {m₁ m₂ : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (k : α) (f : Option β → Option β) (h : m₁.Equiv m₂) :
(Const.alter m₁ k f).Equiv (Const.alter m₂ k f)
theorem Std.DHashMap.Raw.Equiv.constModify {α : Type u} [BEq α] [Hashable α] {β : Type v} {m₁ m₂ : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (k : α) (f : β → β) (h : m₁.Equiv m₂) :
(Const.modify m₁ k f).Equiv (Const.modify m₂ k f)
theorem Std.DHashMap.Raw.Equiv.of_forall_getKey_eq_of_forall_constGet?_eq {α : Type u} [BEq α] [Hashable α] {β : Type v} {m₁ m₂ : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) :
(∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') →
(∀ (k : α), Const.get? m₁ k = Const.get? m₂ k) → m₁.Equiv m₂
theorem Std.DHashMap.Raw.Equiv.of_forall_constGet?_eq {α : Type u} [BEq α] [Hashable α] {β : Type v} {m₁ m₂ : Raw α fun (x : α) => β} [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) :
(∀ (k : α), Const.get? m₁ k = Const.get? m₂ k) → m₁.Equiv m₂
theorem Std.DHashMap.Raw.Const.insertManyIfNewUnit_list_equiv_foldl {α : Type u} [BEq α] [Hashable α] {m : Raw α fun (x : α) => Unit} {l : List α} (h : m.WF) :
(insertManyIfNewUnit m l).Equiv (List.foldl (fun (acc : Raw α fun (x : α) => Unit) (a : α) => acc.insertIfNew a ()) m l)
theorem Std.DHashMap.Raw.Const.unitOfList_equiv_foldl {α : Type u} [BEq α] [Hashable α] {l : List α} :
(unitOfList l).Equiv (List.foldl (fun (acc : Raw α fun (x : α) => Unit) (a : α) => acc.insertIfNew a ()) ∅ l)
@[simp]
@[simp]
theorem Std.DHashMap.Raw.Const.get?_filter_of_getKey?_eq_some {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.getD_filter {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.getD_filter_of_getKey?_eq_some {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.keys_filter {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.getKeyD_filter {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k fallback : α} (h : m.WF) :
theorem Std.DHashMap.Raw.Const.getD_map_of_getKey?_eq_some {α : Type u} [BEq α] [Hashable α] {β : Type v} {γ : Type w} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k k' : α} {fallback : γ} (h : m.WF) :