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_empty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{c : Nat}
:
(Std.DHashMap.empty c).isEmpty = true
@[simp]
theorem
Std.DHashMap.isEmpty_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.DHashMap.contains_congr
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a b : α}
(hab : (a == b) = true)
:
m.contains a = m.contains b
theorem
Std.DHashMap.mem_congr
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a b : α}
(hab : (a == b) = true)
:
@[simp]
theorem
Std.DHashMap.contains_empty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a : α}
{c : Nat}
:
(Std.DHashMap.empty c).contains a = false
@[simp]
theorem
Std.DHashMap.not_mem_empty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a : α}
{c : Nat}
:
¬a ∈ Std.DHashMap.empty c
theorem
Std.DHashMap.contains_of_isEmpty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.DHashMap.not_mem_of_isEmpty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.DHashMap.isEmpty_eq_false_iff_exists_contains_eq_true
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
theorem
Std.DHashMap.isEmpty_eq_false_iff_exists_mem
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
theorem
Std.DHashMap.isEmpty_iff_forall_contains
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
theorem
Std.DHashMap.isEmpty_iff_forall_not_mem
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
@[simp]
theorem
Std.DHashMap.insert_eq_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
{p : (a : α) × β a}
:
@[simp]
theorem
Std.DHashMap.contains_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β k}
:
theorem
Std.DHashMap.mem_of_mem_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β k}
:
@[simp]
theorem
Std.DHashMap.contains_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
@[simp]
theorem
Std.DHashMap.mem_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
k ∈ m.insert k v
@[simp]
theorem
Std.DHashMap.size_empty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{c : Nat}
:
(Std.DHashMap.empty c).size = 0
theorem
Std.DHashMap.isEmpty_eq_size_eq_zero
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
:
theorem
Std.DHashMap.size_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.DHashMap.size_le_size_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
m.size ≤ (m.insert k v).size
theorem
Std.DHashMap.size_insert_le
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
@[simp]
theorem
Std.DHashMap.erase_empty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{k : α}
{c : Nat}
:
(Std.DHashMap.empty c).erase k = Std.DHashMap.empty c
@[simp]
theorem
Std.DHashMap.isEmpty_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.DHashMap.contains_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.DHashMap.contains_of_contains_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.DHashMap.mem_of_mem_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.DHashMap.size_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.DHashMap.size_erase_le
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
(m.erase k).size ≤ m.size
theorem
Std.DHashMap.size_le_size_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[simp]
theorem
Std.DHashMap.containsThenInsert_fst
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
{k : α}
{v : β k}
:
(m.containsThenInsert k v).fst = m.contains k
@[simp]
theorem
Std.DHashMap.containsThenInsert_snd
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
{k : α}
{v : β k}
:
(m.containsThenInsert k v).snd = m.insert k v
@[simp]
theorem
Std.DHashMap.containsThenInsertIfNew_fst
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
{k : α}
{v : β k}
:
(m.containsThenInsertIfNew k v).fst = m.contains k
@[simp]
theorem
Std.DHashMap.containsThenInsertIfNew_snd
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
{k : α}
{v : β k}
:
(m.containsThenInsertIfNew k v).snd = m.insertIfNew k v
@[simp]
theorem
Std.DHashMap.get?_empty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[LawfulBEq α]
{a : α}
{c : Nat}
:
(Std.DHashMap.empty c).get? a = none
@[simp]
theorem
Std.DHashMap.get?_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{k : α}
{v : β k}
:
theorem
Std.DHashMap.contains_eq_isSome_get?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{a : α}
:
m.contains a = (m.get? a).isSome
@[simp]
theorem
Std.DHashMap.get?_erase_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{k : α}
:
(m.erase k).get? k = none
@[simp]
theorem
Std.DHashMap.Const.get?_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{a : α}
{c : Nat}
:
Std.DHashMap.Const.get? (Std.DHashMap.empty c) a = none
@[simp]
theorem
Std.DHashMap.Const.get?_emptyc
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{a : α}
:
Std.DHashMap.Const.get? ∅ a = none
theorem
Std.DHashMap.Const.get?_of_isEmpty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
m.isEmpty = true → Std.DHashMap.Const.get? m a = none
theorem
Std.DHashMap.Const.get?_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β}
:
Std.DHashMap.Const.get? (m.insert k v) a = if (k == a) = true then some v else Std.DHashMap.Const.get? m a
@[simp]
theorem
Std.DHashMap.Const.get?_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
Std.DHashMap.Const.get? (m.insert k v) k = some v
theorem
Std.DHashMap.Const.contains_eq_isSome_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
m.contains a = (Std.DHashMap.Const.get? m a).isSome
theorem
Std.DHashMap.Const.get?_eq_none_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
m.contains a = false → Std.DHashMap.Const.get? m a = none
theorem
Std.DHashMap.Const.get?_eq_none
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
¬a ∈ m → Std.DHashMap.Const.get? m a = none
theorem
Std.DHashMap.Const.get?_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
Std.DHashMap.Const.get? (m.erase k) a = if (k == a) = true then none else Std.DHashMap.Const.get? m a
@[simp]
theorem
Std.DHashMap.Const.get?_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
Std.DHashMap.Const.get? (m.erase k) k = none
theorem
Std.DHashMap.Const.get?_eq_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[LawfulBEq α]
{a : α}
:
Std.DHashMap.Const.get? m a = m.get? a
theorem
Std.DHashMap.Const.get?_congr
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a b : α}
(hab : (a == b) = true)
:
@[simp]
theorem
Std.DHashMap.get_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{k : α}
{v : β k}
:
(m.insert k v).get k ⋯ = v
@[simp]
theorem
Std.DHashMap.get_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{k a : α}
{h' : a ∈ m.erase k}
:
(m.erase k).get a h' = m.get a ⋯
theorem
Std.DHashMap.Const.get_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β}
{h₁ : a ∈ m.insert k v}
:
Std.DHashMap.Const.get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else Std.DHashMap.Const.get m a ⋯
@[simp]
theorem
Std.DHashMap.Const.get_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
Std.DHashMap.Const.get (m.insert k v) k ⋯ = v
@[simp]
theorem
Std.DHashMap.Const.get_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{h' : a ∈ m.erase k}
:
Std.DHashMap.Const.get (m.erase k) a h' = Std.DHashMap.Const.get m a ⋯
theorem
Std.DHashMap.Const.get?_eq_some_get
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{h : a ∈ m}
:
Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.get m a h)
theorem
Std.DHashMap.Const.get_eq_get
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[LawfulBEq α]
{a : α}
{h : a ∈ m}
:
Std.DHashMap.Const.get m a h = m.get a h
theorem
Std.DHashMap.Const.get_congr
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[LawfulBEq α]
{a b : α}
(hab : (a == b) = true)
{h' : a ∈ m}
:
Std.DHashMap.Const.get m a h' = Std.DHashMap.Const.get m b ⋯
@[simp]
theorem
Std.DHashMap.get!_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{a : α}
[Inhabited (β a)]
{b : β a}
:
(m.insert a b).get! a = b
@[simp]
theorem
Std.DHashMap.get!_erase_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{k : α}
[Inhabited (β k)]
:
(m.erase k).get! k = default
theorem
Std.DHashMap.get!_eq_get!_get?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{a : α}
[Inhabited (β a)]
:
m.get! a = (m.get? a).get!
@[simp]
theorem
Std.DHashMap.Const.get!_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
[Inhabited β]
{a : α}
{c : Nat}
:
Std.DHashMap.Const.get! (Std.DHashMap.empty c) a = default
@[simp]
theorem
Std.DHashMap.Const.get!_emptyc
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
[Inhabited β]
{a : α}
:
Std.DHashMap.Const.get! ∅ a = default
theorem
Std.DHashMap.Const.get!_of_isEmpty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{a : α}
:
m.isEmpty = true → Std.DHashMap.Const.get! m a = default
theorem
Std.DHashMap.Const.get!_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{k a : α}
{v : β}
:
Std.DHashMap.Const.get! (m.insert k v) a = if (k == a) = true then v else Std.DHashMap.Const.get! m a
@[simp]
theorem
Std.DHashMap.Const.get!_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{k : α}
{v : β}
:
Std.DHashMap.Const.get! (m.insert k v) k = v
theorem
Std.DHashMap.Const.get!_eq_default_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{a : α}
:
m.contains a = false → Std.DHashMap.Const.get! m a = default
theorem
Std.DHashMap.Const.get!_eq_default
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{a : α}
:
¬a ∈ m → Std.DHashMap.Const.get! m a = default
theorem
Std.DHashMap.Const.get!_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{k a : α}
:
Std.DHashMap.Const.get! (m.erase k) a = if (k == a) = true then default else Std.DHashMap.Const.get! m a
@[simp]
theorem
Std.DHashMap.Const.get!_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{k : α}
:
Std.DHashMap.Const.get! (m.erase k) k = default
theorem
Std.DHashMap.Const.get?_eq_some_get!_of_contains
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{a : α}
:
m.contains a = true → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.get! m a)
theorem
Std.DHashMap.Const.get?_eq_some_get!
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{a : α}
:
a ∈ m → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.get! m a)
theorem
Std.DHashMap.Const.get!_eq_get!_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{a : α}
:
Std.DHashMap.Const.get! m a = (Std.DHashMap.Const.get? m a).get!
theorem
Std.DHashMap.Const.get_eq_get!
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{a : α}
{h : a ∈ m}
:
Std.DHashMap.Const.get m a h = Std.DHashMap.Const.get! m a
theorem
Std.DHashMap.Const.get!_eq_get!
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[LawfulBEq α]
[Inhabited β]
{a : α}
:
Std.DHashMap.Const.get! m a = m.get! a
theorem
Std.DHashMap.Const.get!_congr
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{a b : α}
(hab : (a == b) = true)
:
@[simp]
theorem
Std.DHashMap.getD_empty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[LawfulBEq α]
{a : α}
{fallback : β a}
{c : Nat}
:
(Std.DHashMap.empty c).getD a fallback = fallback
@[simp]
theorem
Std.DHashMap.getD_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{k : α}
{fallback v : β k}
:
(m.insert k v).getD k fallback = v
@[simp]
theorem
Std.DHashMap.getD_erase_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{k : α}
{fallback : β k}
:
(m.erase k).getD k fallback = fallback
theorem
Std.DHashMap.getD_eq_getD_get?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{a : α}
{fallback : β a}
:
m.getD a fallback = (m.get? a).getD fallback
theorem
Std.DHashMap.get_eq_getD
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{a : α}
{fallback : β a}
{h : a ∈ m}
:
m.get a h = m.getD a fallback
theorem
Std.DHashMap.get!_eq_getD_default
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{a : α}
[Inhabited (β a)]
:
m.get! a = m.getD a default
@[simp]
theorem
Std.DHashMap.Const.getD_empty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{a : α}
{fallback : β}
{c : Nat}
:
Std.DHashMap.Const.getD (Std.DHashMap.empty c) a fallback = fallback
@[simp]
theorem
Std.DHashMap.Const.getD_emptyc
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{a : α}
{fallback : β}
:
Std.DHashMap.Const.getD ∅ a fallback = fallback
theorem
Std.DHashMap.Const.getD_of_isEmpty
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
:
m.isEmpty = true → Std.DHashMap.Const.getD m a fallback = fallback
theorem
Std.DHashMap.Const.getD_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{fallback v : β}
:
Std.DHashMap.Const.getD (m.insert k v) a fallback = if (k == a) = true then v else Std.DHashMap.Const.getD m a fallback
@[simp]
theorem
Std.DHashMap.Const.getD_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{fallback v : β}
:
Std.DHashMap.Const.getD (m.insert k v) k fallback = v
theorem
Std.DHashMap.Const.getD_eq_fallback_of_contains_eq_false
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
:
m.contains a = false → Std.DHashMap.Const.getD m a fallback = fallback
theorem
Std.DHashMap.Const.getD_eq_fallback
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
:
¬a ∈ m → Std.DHashMap.Const.getD m a fallback = fallback
theorem
Std.DHashMap.Const.getD_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{fallback : β}
:
Std.DHashMap.Const.getD (m.erase k) a fallback = if (k == a) = true then fallback else Std.DHashMap.Const.getD m a fallback
@[simp]
theorem
Std.DHashMap.Const.getD_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{fallback : β}
:
Std.DHashMap.Const.getD (m.erase k) k fallback = fallback
theorem
Std.DHashMap.Const.get?_eq_some_getD_of_contains
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
:
m.contains a = true → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.getD m a fallback)
theorem
Std.DHashMap.Const.get?_eq_some_getD
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
:
a ∈ m → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.getD m a fallback)
theorem
Std.DHashMap.Const.getD_eq_getD_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
:
Std.DHashMap.Const.getD m a fallback = (Std.DHashMap.Const.get? m a).getD fallback
theorem
Std.DHashMap.Const.get_eq_getD
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{fallback : β}
{h : a ∈ m}
:
Std.DHashMap.Const.get m a h = Std.DHashMap.Const.getD m a fallback
theorem
Std.DHashMap.Const.get!_eq_getD_default
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{a : α}
:
Std.DHashMap.Const.get! m a = Std.DHashMap.Const.getD m a default
theorem
Std.DHashMap.Const.getD_eq_getD
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[LawfulBEq α]
{a : α}
{fallback : β}
:
Std.DHashMap.Const.getD m a fallback = m.getD a fallback
theorem
Std.DHashMap.Const.getD_congr
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a b : α}
{fallback : β}
(hab : (a == b) = true)
:
Std.DHashMap.Const.getD m a fallback = Std.DHashMap.Const.getD m b fallback
@[simp]
theorem
Std.DHashMap.getKey?_empty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a : α}
{c : Nat}
:
(Std.DHashMap.empty c).getKey? a = none
theorem
Std.DHashMap.getKey?_of_isEmpty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.DHashMap.getKey?_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a k : α}
{v : β k}
:
@[simp]
theorem
Std.DHashMap.getKey?_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.DHashMap.contains_eq_isSome_getKey?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
m.contains a = (m.getKey? a).isSome
theorem
Std.DHashMap.getKey?_eq_none_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.DHashMap.getKey?_eq_none
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.DHashMap.getKey?_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
@[simp]
theorem
Std.DHashMap.getKey?_erase_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
(m.erase k).getKey? k = none
theorem
Std.DHashMap.getKey_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β k}
{h₁ : a ∈ m.insert k v}
:
@[simp]
theorem
Std.DHashMap.getKey_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
(m.insert k v).getKey k ⋯ = k
@[simp]
theorem
Std.DHashMap.getKey_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{h' : a ∈ m.erase k}
:
(m.erase k).getKey a h' = m.getKey a ⋯
theorem
Std.DHashMap.getKey?_eq_some_getKey
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{h : a ∈ m}
:
@[simp]
theorem
Std.DHashMap.getKey!_empty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
[Inhabited α]
{a : α}
{c : Nat}
:
(Std.DHashMap.empty c).getKey! a = default
theorem
Std.DHashMap.getKey!_of_isEmpty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
theorem
Std.DHashMap.getKey!_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{k a : α}
{v : β k}
:
@[simp]
theorem
Std.DHashMap.getKey!_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
{b : β a}
:
(m.insert a b).getKey! a = a
theorem
Std.DHashMap.getKey!_eq_default_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
theorem
Std.DHashMap.getKey!_eq_default
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
theorem
Std.DHashMap.getKey!_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{k a : α}
:
@[simp]
theorem
Std.DHashMap.getKey!_erase_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{k : α}
:
(m.erase k).getKey! k = default
theorem
Std.DHashMap.getKey?_eq_some_getKey!_of_contains
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
theorem
Std.DHashMap.getKey?_eq_some_getKey!
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
theorem
Std.DHashMap.getKey!_eq_get!_getKey?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
m.getKey! a = (m.getKey? a).get!
theorem
Std.DHashMap.getKey_eq_getKey!
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
{h : a ∈ m}
:
m.getKey a h = m.getKey! a
@[simp]
theorem
Std.DHashMap.getKeyD_empty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{a fallback : α}
{c : Nat}
:
(Std.DHashMap.empty c).getKeyD a fallback = fallback
theorem
Std.DHashMap.getKeyD_of_isEmpty
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.DHashMap.getKeyD_insert
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a fallback : α}
{v : β k}
:
@[simp]
theorem
Std.DHashMap.getKeyD_insert_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
{v : β k}
:
(m.insert k v).getKeyD k fallback = k
theorem
Std.DHashMap.getKeyD_eq_fallback_of_contains_eq_false
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.DHashMap.getKeyD_eq_fallback
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.DHashMap.getKeyD_erase
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a fallback : α}
:
@[simp]
theorem
Std.DHashMap.getKeyD_erase_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
:
(m.erase k).getKeyD k fallback = fallback
theorem
Std.DHashMap.getKey?_eq_some_getKeyD_of_contains
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.DHashMap.getKey?_eq_some_getKeyD
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.DHashMap.getKeyD_eq_getD_getKey?
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
m.getKeyD a fallback = (m.getKey? a).getD fallback
theorem
Std.DHashMap.getKey_eq_getKeyD
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
{h : a ∈ m}
:
m.getKey a h = m.getKeyD a fallback
theorem
Std.DHashMap.getKey!_eq_getKeyD_default
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
m.getKey! a = m.getKeyD a default
@[simp]
theorem
Std.DHashMap.isEmpty_insertIfNew
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
@[simp]
theorem
Std.DHashMap.contains_insertIfNew
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β k}
:
theorem
Std.DHashMap.contains_insertIfNew_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.DHashMap.mem_insertIfNew_self
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
k ∈ m.insertIfNew k v
theorem
Std.DHashMap.mem_of_mem_insertIfNew
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β k}
:
theorem
Std.DHashMap.contains_of_contains_insertIfNew'
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.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 : Std.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_insertIfNew
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.DHashMap.size_le_size_insertIfNew
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
m.size ≤ (m.insertIfNew k v).size
theorem
Std.DHashMap.size_insertIfNew_le
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.DHashMap.Const.get?_insertIfNew
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β}
:
Std.DHashMap.Const.get? (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then some v else Std.DHashMap.Const.get? m a
theorem
Std.DHashMap.Const.get_insertIfNew
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β}
{h₁ : a ∈ m.insertIfNew k v}
:
Std.DHashMap.Const.get (m.insertIfNew k v) a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then v else Std.DHashMap.Const.get m a ⋯
theorem
Std.DHashMap.Const.get!_insertIfNew
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{k a : α}
{v : β}
:
Std.DHashMap.Const.get! (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then v else Std.DHashMap.Const.get! m a
theorem
Std.DHashMap.Const.getD_insertIfNew
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{fallback v : β}
:
Std.DHashMap.Const.getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ ¬k ∈ m then v else Std.DHashMap.Const.getD m a fallback
@[simp]
theorem
Std.DHashMap.getThenInsertIfNew?_fst
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{k : α}
{v : β k}
:
(m.getThenInsertIfNew? k v).fst = m.get? k
@[simp]
theorem
Std.DHashMap.getThenInsertIfNew?_snd
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
{k : α}
{v : β k}
:
(m.getThenInsertIfNew? k v).snd = m.insertIfNew k v
@[simp]
theorem
Std.DHashMap.Const.getThenInsertIfNew?_fst
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
{k : α}
{v : β}
:
(Std.DHashMap.Const.getThenInsertIfNew? m k v).fst = Std.DHashMap.Const.get? m k
@[simp]
theorem
Std.DHashMap.Const.getThenInsertIfNew?_snd
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : Std.DHashMap α fun (x : α) => β}
{k : α}
{v : β}
:
(Std.DHashMap.Const.getThenInsertIfNew? m k v).snd = m.insertIfNew k v
@[simp]
theorem
Std.DHashMap.length_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
m.keys.length = m.size
@[simp]
theorem
Std.DHashMap.isEmpty_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
m.keys.isEmpty = m.isEmpty
@[simp]
theorem
Std.DHashMap.contains_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
m.keys.contains k = m.contains k
@[simp]
theorem
Std.DHashMap.mem_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[LawfulBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.DHashMap.distinct_keys
{α : Type u}
{β : α → Type v}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{m : Std.DHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
List.Pairwise (fun (a b : α) => (a == b) = false) m.keys