Dependent hash map lemmas #
This file contains lemmas about Std.DHashMap. 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 α.
theorem Std.DHashMap.getKey?_beq {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
@[simp]
theorem Std.DHashMap.isEmpty_insertIfNew {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@[simp]
theorem Std.DHashMap.contains_insertIfNew {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
theorem Std.DHashMap.contains_insertIfNew_self {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
theorem Std.DHashMap.mem_insertIfNew_self {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
theorem Std.DHashMap.mem_of_mem_insertIfNew {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
theorem Std.DHashMap.contains_of_contains_insertIfNew' {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {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.mem_of_mem_insertIfNew' {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {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.size_le_size_insertIfNew {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
theorem Std.DHashMap.size_insertIfNew_le {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
theorem Std.DHashMap.Const.get_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v} :
theorem Std.DHashMap.getKey_insertIfNew {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {h₁ : a ∈ m.insertIfNew k v} :
theorem Std.DHashMap.distinct_keys {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] :
List.Pairwise (fun (a b : α) => (a == b) = false) m.keys
theorem Std.DHashMap.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
theorem Std.DHashMap.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
instance Std.DHashMap.instPureForInSigmaOfLawfulMonad {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] :
Internal.PureForIn m' (DHashMap α β) ((a : α) × β a)
theorem Std.DHashMap.insertMany_ind {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {motive : DHashMap α β → Prop} (m : DHashMap α β) (l : ρ) (init : motive m) (insert : ∀ (m : DHashMap α β) (a : α) (b : β a), motive m → motive (m.insert a b)) :
motive (m.insertMany l)
theorem Std.DHashMap.get?_insertMany_list_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [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) :
theorem Std.DHashMap.get_insertMany_list_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [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' ∈ m.insertMany l} :
theorem Std.DHashMap.get!_insertMany_list_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [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.getD_insertMany_list_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [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.getKey?_insertMany_list_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [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.getKey_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h : k ∈ m.insertMany l} :
theorem Std.DHashMap.getKey_insertMany_list_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [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' ∈ m.insertMany l} :
theorem Std.DHashMap.getKey!_insertMany_list_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [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.getKeyD_insertMany_list_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [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.size_insertMany_list {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) :
theorem Std.DHashMap.size_le_size_insertMany_list {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
@[deprecated Std.DHashMap.union_insert_right_equiv_insert_union (since := "2025-11-03")]
theorem Std.DHashMap.Const.insertMany_ind {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {ρ : Type w} [ForIn Id ρ (α × β)] {motive : (DHashMap α fun (x : α) => β) → Prop} (m : DHashMap α fun (x : α) => β) (l : ρ) (init : motive m) (insert : ∀ (m : DHashMap α fun (x : α) => β) (a : α) (b : β), motive m → motive (m.insert a b)) :
motive (insertMany m l)
theorem Std.DHashMap.Const.getKey?_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [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) :
theorem Std.DHashMap.Const.getKey_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h : k ∈ insertMany m l} :
theorem Std.DHashMap.Const.getKey_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [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' ∈ insertMany m l} :
theorem Std.DHashMap.Const.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.DHashMap.Const.getKey!_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [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.Const.getKeyD_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [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) :
theorem Std.DHashMap.Const.size_le_size_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
theorem Std.DHashMap.Const.get?_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [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) :
theorem Std.DHashMap.Const.get?_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
theorem Std.DHashMap.Const.get_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h : k ∈ insertMany m l} :
theorem Std.DHashMap.Const.get_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [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' ∈ insertMany m l} :
theorem Std.DHashMap.Const.get!_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {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.Const.getD_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [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.Const.insertManyIfNewUnit_ind {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {ρ : Type w} [ForIn Id ρ α] {motive : (DHashMap α fun (x : α) => Unit) → Prop} (m : DHashMap α fun (x : α) => Unit) (l : ρ) (init : motive m) (insert : ∀ (m : DHashMap α fun (x : α) => Unit) (a : α), motive m → motive (m.insertIfNew a ())) :
motive (insertManyIfNewUnit m l)
theorem Std.DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :
theorem Std.DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (h' : k ∈ m) :
theorem Std.DHashMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) {h : k' ∈ insertManyIfNewUnit m l} :
theorem Std.DHashMap.Const.getKey_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (mem : k ∈ m) {h : k ∈ insertManyIfNewUnit m l} :
theorem Std.DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) :
theorem Std.DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :
theorem Std.DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :
theorem Std.DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (mem : k ∈ m) :
theorem Std.DHashMap.Const.size_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :
theorem Std.DHashMap.Const.size_le_size_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} :
theorem Std.DHashMap.Const.get_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} {l : List α} {k : α} {h : k ∈ insertManyIfNewUnit m l} :
theorem Std.DHashMap.get_ofList_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : 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.get!_ofList_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : 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.getD_ofList_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : 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.getKey?_ofList_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : 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.getKey_ofList_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : 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.getKey!_ofList_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : 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.getKeyD_ofList_of_mem {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : 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.Const.get_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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.Const.get!_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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.Const.getD_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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.Const.getKey?_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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) :
theorem Std.DHashMap.Const.getKey_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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.Const.getKey!_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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.Const.getKeyD_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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.Const.unitOfArray_eq_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (a : Array α) :
@[simp]
@[simp]
theorem Std.DHashMap.Const.unitOfList_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {k : α} :
theorem Std.DHashMap.Const.unitOfList_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {hd : α} {tl : List α} :
theorem Std.DHashMap.Const.unitOfList_eq_insertManyIfNewUnit_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {l : List α} :
@[simp]
theorem Std.DHashMap.Const.contains_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
@[simp]
theorem Std.DHashMap.Const.mem_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
theorem Std.DHashMap.Const.getKey?_unitOfList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
theorem Std.DHashMap.Const.getKey?_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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.Const.getKey_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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.Const.getKeyD_unitOfList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (contains_eq_false : l.contains k = false) :
theorem Std.DHashMap.Const.getKeyD_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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.Const.size_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :
theorem Std.DHashMap.Const.size_unitOfList_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} :
@[simp]
theorem Std.DHashMap.Const.isEmpty_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} :
@[simp]
theorem Std.DHashMap.Const.get_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {l : List α} {k : α} {h : k ∈ unitOfList l} :
@[simp]
@[simp]
theorem Std.DHashMap.Const.size_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
theorem Std.DHashMap.Const.getD_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β} :
theorem Std.DHashMap.Const.getKey?_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
theorem Std.DHashMap.Const.getKeyD_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β} :
@[simp]
theorem Std.DHashMap.Const.get?_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
theorem Std.DHashMap.Const.getD_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} :
@[simp]
theorem Std.DHashMap.Const.getD_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} :
theorem Std.DHashMap.Const.getKey!_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} :
theorem Std.DHashMap.Const.getKeyD_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} :
theorem Std.DHashMap.Equiv.insertIfNew {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : DHashMap α β} [EquivBEq α] [LawfulHashable α] (k : α) (v : β k) (h : m₁.Equiv m₂) :
(m₁.insertIfNew k v).Equiv (m₂.insertIfNew k v)
theorem Std.DHashMap.Equiv.insertMany_list {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : DHashMap α β} [EquivBEq α] [LawfulHashable α] (l : List ((a : α) × β a)) (h : m₁.Equiv m₂) :
(m₁.insertMany l).Equiv (m₂.insertMany l)
theorem Std.DHashMap.Equiv.filter {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : DHashMap α β} (f : (a : α) → β a → Bool) (h : m₁.Equiv m₂) :
(DHashMap.filter f m₁).Equiv (DHashMap.filter f m₂)
theorem Std.DHashMap.Equiv.map {α : Type u} {β : α → Type v} {γ : α → Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : DHashMap α β} (f : (a : α) → β a → γ a) (h : m₁.Equiv m₂) :
(DHashMap.map f m₁).Equiv (DHashMap.map f m₂)
theorem Std.DHashMap.Equiv.filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m₁ m₂ : DHashMap α β} (f : (a : α) → β a → Option (γ a)) (h : m₁.Equiv m₂) :
(DHashMap.filterMap f m₁).Equiv (DHashMap.filterMap f m₂)
theorem Std.DHashMap.Equiv.constToList_perm {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : DHashMap α fun (x : α) => β} (h : m₁.Equiv m₂) :
(Const.toList m₁).Perm (Const.toList m₂)
theorem Std.DHashMap.Equiv.of_constToList_perm {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : DHashMap α fun (x : α) => β} (h : (Const.toList m₁).Perm (Const.toList m₂)) :
m₁.Equiv m₂
theorem Std.DHashMap.Equiv.constGet?_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} (h : m₁.Equiv m₂) :
theorem Std.DHashMap.Equiv.constGet!_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} (h : m₁.Equiv m₂) :
theorem Std.DHashMap.Equiv.constGetD_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} (h : m₁.Equiv m₂) :
theorem Std.DHashMap.Equiv.constInsertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (l : List (α × β)) (h : m₁.Equiv m₂) :
(Const.insertMany m₁ l).Equiv (Const.insertMany m₂ l)
theorem Std.DHashMap.Equiv.constInsertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : DHashMap α fun (x : α) => Unit} (l : List α) (h : m₁.Equiv m₂) :
(Const.insertManyIfNewUnit m₁ l).Equiv (Const.insertManyIfNewUnit m₂ l)
theorem Std.DHashMap.Equiv.constAlter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (k : α) (f : Option β → Option β) (h : m₁.Equiv m₂) :
(Const.alter m₁ k f).Equiv (Const.alter m₂ k f)
theorem Std.DHashMap.Equiv.constModify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (k : α) (f : β → β) (h : m₁.Equiv m₂) :
(Const.modify m₁ k f).Equiv (Const.modify m₂ k f)
theorem Std.DHashMap.Equiv.of_forall_getKey_eq_of_forall_constGet?_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (hk : ∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') (hv : ∀ (k : α), Const.get? m₁ k = Const.get? m₂ k) :
m₁.Equiv m₂
theorem Std.DHashMap.Equiv.of_forall_constGet?_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : DHashMap α fun (x : α) => β} [LawfulBEq α] (hv : ∀ (k : α), Const.get? m₁ k = Const.get? m₂ k) :
m₁.Equiv m₂
@[instance_reducible]
Internal implementation detail of the hash map.
Equations
- Std.DHashMap.isSetoid α β = { r := Std.DHashMap.Equiv, iseqv := ⋯ }
Instances For
theorem Std.DHashMap.insertMany_list_equiv_foldl {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} {l : List ((a : α) × β a)} :
(m.insertMany l).Equiv (List.foldl (fun (acc : DHashMap α β) (p : (a : α) × β a) => acc.insert p.fst p.snd) m l)
theorem Std.DHashMap.Const.insertManyIfNewUnit_list_equiv_foldl {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α fun (x : α) => Unit} {l : List α} :
(insertManyIfNewUnit m l).Equiv
(List.foldl (fun (acc : DHashMap α fun (x : α) => Unit) (a : α) => acc.insertIfNew a ()) m l)
theorem Std.DHashMap.Const.unitOfList_equiv_foldl {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {l : List α} :
(unitOfList l).Equiv (List.foldl (fun (acc : DHashMap α fun (x : α) => Unit) (p : α) => acc.insertIfNew p ()) ∅ l)
theorem Std.DHashMap.Const.isEmpty_filterMap_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} :
theorem Std.DHashMap.Const.isEmpty_filterMap_eq_false_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} :
theorem Std.DHashMap.Const.size_filterMap_eq_size_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} :
@[simp]
theorem Std.DHashMap.Const.get?_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} :
@[simp]
theorem Std.DHashMap.Const.getD_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ} :
theorem Std.DHashMap.Const.getKey?_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} :
theorem Std.DHashMap.Const.getKeyD_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k fallback : α} :
theorem Std.DHashMap.getKey?_filter_key {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} :
theorem Std.DHashMap.getKeyD_filter_key {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k fallback : α} :
theorem Std.DHashMap.Const.get?_filter_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α} :
theorem Std.DHashMap.Const.get!_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {f : α → β → Bool} {k : α} :
theorem Std.DHashMap.Const.get!_filter_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {f : α → β → Bool} {k k' : α} :
theorem Std.DHashMap.Const.getD_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β} :
theorem Std.DHashMap.Const.getD_filter' {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [LawfulBEq α] {f : α → β → Bool} {k : α} {fallback : β} :
Simpler variant of getD_filter when LawfulBEq is available.
theorem Std.DHashMap.Const.getD_filter_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β} :
theorem Std.DHashMap.Const.keys_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} :
theorem Std.DHashMap.Const.getKey!_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : α → β → Bool} {k : α} :
theorem Std.DHashMap.Const.getKeyD_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : DHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k fallback : α} :