Dependent hash map lemmas #
This file contains lemmas about Std.Data.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 α
.
@[simp]
theorem
Std.DHashMap.isEmpty_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.DHashMap.contains_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.DHashMap.contains_of_contains_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.DHashMap.size_erase_le
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.DHashMap.Const.get?_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
theorem
Std.DHashMap.Const.contains_eq_isSome_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
@[simp]
theorem
Std.DHashMap.Const.get?_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.DHashMap.Const.get_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
@[simp]
theorem
Std.DHashMap.Const.get!_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{k : α}
{v : β}
:
@[simp]
theorem
Std.DHashMap.Const.get!_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{k : α}
:
@[simp]
theorem
Std.DHashMap.Const.getD_emptyc
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{a : α}
{fallback : β}
:
@[simp]
theorem
Std.DHashMap.Const.getD_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{fallback v : β}
:
theorem
Std.DHashMap.Const.getD_eq_fallback_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
:
theorem
Std.DHashMap.Const.getD_eq_fallback
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
:
@[simp]
theorem
Std.DHashMap.Const.getD_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{fallback : β}
:
theorem
Std.DHashMap.Const.getD_eq_getD_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
:
@[simp]
theorem
Std.DHashMap.getKey?_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.DHashMap.contains_eq_isSome_getKey?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.DHashMap.getKey?_eq_none_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
@[simp]
theorem
Std.DHashMap.getKey?_erase_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.DHashMap.getKey_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
@[simp]
theorem
Std.DHashMap.getKey!_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
{b : β a}
:
theorem
Std.DHashMap.getKey!_eq_default_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
@[simp]
theorem
Std.DHashMap.getKey!_erase_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{k : α}
:
theorem
Std.DHashMap.getKey?_eq_some_getKey!_of_contains
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
theorem
Std.DHashMap.getKey!_eq_get!_getKey?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
@[simp]
theorem
Std.DHashMap.getKeyD_emptyc
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a fallback : α}
:
@[simp]
theorem
Std.DHashMap.getKeyD_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
{v : β k}
:
theorem
Std.DHashMap.getKeyD_eq_fallback_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.DHashMap.getKeyD_eq_fallback
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
@[simp]
theorem
Std.DHashMap.getKeyD_erase_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
:
theorem
Std.DHashMap.getKey?_eq_some_getKeyD_of_contains
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.DHashMap.getKeyD_eq_getD_getKey?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.DHashMap.getKey_eq_getKeyD
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
{h : a ∈ m}
:
theorem
Std.DHashMap.getKey!_eq_getKeyD_default
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
@[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.contains_of_contains_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_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_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}
:
@[simp]
theorem
Std.DHashMap.length_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
@[simp]
theorem
Std.DHashMap.isEmpty_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
@[simp]
theorem
Std.DHashMap.contains_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.DHashMap.distinct_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
@[simp]
theorem
Std.DHashMap.contains_insertMany_list
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
{k : α}
:
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_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)
:
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_contains_eq_false
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
{k fallback : α}
(contains_eq_false : (List.map Sigma.fst l).contains k = false)
:
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_le_size_insertMany_list
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
:
theorem
Std.DHashMap.size_insertMany_list_le
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
:
@[simp]
theorem
Std.DHashMap.isEmpty_insertMany_list
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
:
theorem
Std.DHashMap.Const.mem_of_mem_insertMany_list
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
{k : α}
(mem : k ∈ insertMany m l)
(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 α]
{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.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_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)
:
@[simp]
theorem
Std.DHashMap.Const.contains_insertManyIfNewUnit_list
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α fun (x : α) => Unit}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
:
theorem
Std.DHashMap.Const.mem_of_mem_insertManyIfNewUnit_list
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α fun (x : α) => Unit}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
(contains_eq_false : l.contains k = false)
:
k ∈ insertManyIfNewUnit m l → 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)
:
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.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.size_insertManyIfNewUnit_list_le
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α fun (x : α) => Unit}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
:
@[simp]
theorem
Std.DHashMap.Const.isEmpty_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_contains_eq_false
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
{k : α}
(contains_eq_false : (List.map Sigma.fst l).contains k = false)
:
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_contains_eq_false
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{l : List ((a : α) × β a)}
{k : α}
(contains_eq_false : (List.map Sigma.fst l).contains k = false)
:
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_contains_eq_false
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
{k fallback : α}
(contains_eq_false : (List.map Sigma.fst l).contains k = false)
:
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.size_ofList_le
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
:
@[simp]
theorem
Std.DHashMap.isEmpty_ofList
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
:
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]
@[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 α}
:
@[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_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{l : List α}
{k : α}
(contains_eq_false : l.contains k = false)
:
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.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 α}
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
:
@[simp]
theorem
Std.DHashMap.Const.get_unitOfList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{l : List α}
{k : α}
{h : k ∈ unitOfList l}
:
@[simp]
theorem
Std.DHashMap.Const.get!_unitOfList
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{l : List α}
{k : α}
:
@[simp]
@[simp]
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 β}
:
theorem
Std.DHashMap.get!_modify
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[LawfulBEq α]
{k k' : α}
[hi : Inhabited (β k')]
{f : β k → β k}
:
(m.modify k f).get! k' = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).get! else m.get! k'
theorem
Std.DHashMap.getD_modify
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : DHashMap α β}
[LawfulBEq α]
{k k' : α}
{fallback : β k'}
{f : β k → β k}
:
(m.modify k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).getD fallback else m.getD k' fallback
@[simp]
theorem
Std.DHashMap.Const.isEmpty_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{f : β → β}
:
@[simp]
theorem
Std.DHashMap.Const.contains_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k k' : α}
{f : β → β}
:
@[simp]
theorem
Std.DHashMap.Const.size_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{f : β → β}
:
@[simp]
theorem
Std.DHashMap.Const.get?_modify_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{f : β → β}
:
@[simp]
theorem
Std.DHashMap.Const.get!_modify_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
[Inhabited β]
{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 : β → β}
: