Documentation

Std.Data.HashMap.Lemmas

Hash map lemmas #

This module contains lemmas about Std.Data.HashMap. 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 α.

source
@[simp]
theorem Std.HashMap.isEmpty_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {c : Nat} :
(Std.HashMap.empty c).isEmpty = true
source
@[simp]
theorem Std.HashMap.isEmpty_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} :
∅.isEmpty = true
source
@[simp]
theorem Std.HashMap.isEmpty_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).isEmpty = false
source
theorem Std.HashMap.mem_iff_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {a : α} :
a ∈ m ↔ m.contains a = true
source
theorem Std.HashMap.contains_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) :
m.contains a = m.contains b
source
theorem Std.HashMap.mem_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) :
a ∈ m ↔ b ∈ m
source
@[simp]
theorem Std.HashMap.contains_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} :
(Std.HashMap.empty c).contains a = false
source
@[simp]
theorem Std.HashMap.get_eq_getElem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {a : α} {h : a ∈ m} :
m.get a h = m[a]
source
@[simp]
theorem Std.HashMap.get?_eq_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {a : α} :
m.get? a = m[a]?
source
@[simp]
theorem Std.HashMap.get!_eq_getElem! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [Inhabited β] {a : α} :
m.get! a = m[a]!
source
@[simp]
theorem Std.HashMap.not_mem_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} :
¬a ∈ Std.HashMap.empty c
source
@[simp]
theorem Std.HashMap.contains_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} :
∅.contains a = false
source
@[simp]
theorem Std.HashMap.not_mem_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} :
¬a ∈ ∅
source
theorem Std.HashMap.contains_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = true → m.contains a = false
source
theorem Std.HashMap.not_mem_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = true → ¬a ∈ m
source
theorem Std.HashMap.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] :
m.isEmpty = false ↔ ∃ (a : α), m.contains a = true
source
theorem Std.HashMap.isEmpty_eq_false_iff_exists_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] :
m.isEmpty = false ↔ ∃ (a : α), a ∈ m
source
theorem Std.HashMap.isEmpty_iff_forall_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] :
m.isEmpty = true ↔ ∀ (a : α), m.contains a = false
source
theorem Std.HashMap.isEmpty_iff_forall_not_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] :
m.isEmpty = true ↔ ∀ (a : α), ¬a ∈ m
source
@[simp]
theorem Std.HashMap.insert_eq_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {p : α × β} :
insert p m = m.insert p.fst p.snd
source
@[simp]
theorem Std.HashMap.singleton_eq_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {p : α × β} :
{p} = ∅.insert p.fst p.snd
source
@[simp]
theorem Std.HashMap.contains_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).contains a = (k == a || m.contains a)
source
@[simp]
theorem Std.HashMap.mem_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m
source
theorem Std.HashMap.contains_of_contains_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).contains a = true → (k == a) = false → m.contains a = true
source
theorem Std.HashMap.mem_of_mem_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a ∈ m.insert k v → (k == a) = false → a ∈ m
source
@[simp]
theorem Std.HashMap.contains_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).contains k = true
source
@[simp]
theorem Std.HashMap.mem_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
k ∈ m.insert k v
source
@[simp]
theorem Std.HashMap.size_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {c : Nat} :
(Std.HashMap.empty c).size = 0
source
@[simp]
theorem Std.HashMap.size_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} :
∅.size = 0
source
theorem Std.HashMap.isEmpty_eq_size_eq_zero {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} :
m.isEmpty = (m.size == 0)
source
theorem Std.HashMap.size_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).size = if k ∈ m then m.size else m.size + 1
source
theorem Std.HashMap.size_le_size_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
m.size ≤ (m.insert k v).size
source
theorem Std.HashMap.size_insert_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).size ≤ m.size + 1
source
@[simp]
theorem Std.HashMap.erase_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} :
(Std.HashMap.empty c).erase a = Std.HashMap.empty c
source
@[simp]
theorem Std.HashMap.erase_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} :
∅.erase a = ∅
source
@[simp]
theorem Std.HashMap.isEmpty_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)
source
@[simp]
theorem Std.HashMap.contains_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = (!k == a && m.contains a)
source
@[simp]
theorem Std.HashMap.mem_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
source
theorem Std.HashMap.contains_of_contains_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = true → m.contains a = true
source
theorem Std.HashMap.mem_of_mem_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
a ∈ m.erase k → a ∈ m
source
theorem Std.HashMap.size_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size = if k ∈ m then m.size - 1 else m.size
source
theorem Std.HashMap.size_erase_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size ≤ m.size
source
theorem Std.HashMap.size_le_size_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
m.size ≤ (m.erase k).size + 1
source
@[simp]
theorem Std.HashMap.containsThenInsert_fst {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {k : α} {v : β} :
(m.containsThenInsert k v).fst = m.contains k
source
@[simp]
theorem Std.HashMap.containsThenInsert_snd {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {k : α} {v : β} :
(m.containsThenInsert k v).snd = m.insert k v
source
@[simp]
theorem Std.HashMap.containsThenInsertIfNew_fst {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {k : α} {v : β} :
(m.containsThenInsertIfNew k v).fst = m.contains k
source
@[simp]
theorem Std.HashMap.containsThenInsertIfNew_snd {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {k : α} {v : β} :
(m.containsThenInsertIfNew k v).snd = m.insertIfNew k v
source
@[simp]
theorem Std.HashMap.getElem?_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} :
(Std.HashMap.empty c)[a]? = none
source
@[simp]
theorem Std.HashMap.getElem?_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} :
∅[a]? = none
source
theorem Std.HashMap.getElem?_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = true → m[a]? = none
source
theorem Std.HashMap.getElem?_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v)[a]? = if (k == a) = true then some v else m[a]?
source
@[simp]
theorem Std.HashMap.getElem?_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v)[k]? = some v
source
theorem Std.HashMap.contains_eq_isSome_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = m[a]?.isSome
source
theorem Std.HashMap.getElem?_eq_none_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false → m[a]? = none
source
theorem Std.HashMap.getElem?_eq_none {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
¬a ∈ m → m[a]? = none
source
theorem Std.HashMap.getElem?_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k)[a]? = if (k == a) = true then none else m[a]?
source
@[simp]
theorem Std.HashMap.getElem?_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k)[k]? = none
source
theorem Std.HashMap.getElem?_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) :
m[a]? = m[b]?
source
theorem Std.HashMap.getElem_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v} :
(m.insert k v)[a] = if h₂ : (k == a) = true then v else m[a]
source
@[simp]
theorem Std.HashMap.getElem_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v)[k] = v
source
@[simp]
theorem Std.HashMap.getElem_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {h' : a ∈ m.erase k} :
(m.erase k)[a] = m[a]
source
theorem Std.HashMap.getElem?_eq_some_getElem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h' : a ∈ m} :
m[a]? = some m[a]
source
theorem Std.HashMap.getElem_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {a b : α} (hab : (a == b) = true) {h' : a ∈ m} :
m[a] = m[b]
source
@[simp]
theorem Std.HashMap.getElem!_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited β] {a : α} {c : Nat} :
(Std.HashMap.empty c)[a]! = default
source
@[simp]
theorem Std.HashMap.getElem!_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited β] {a : α} :
∅[a]! = default
source
theorem Std.HashMap.getElem!_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m.isEmpty = true → m[a]! = default
source
theorem Std.HashMap.getElem!_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
(m.insert k v)[a]! = if (k == a) = true then v else m[a]!
source
@[simp]
theorem Std.HashMap.getElem!_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
(m.insert k v)[k]! = v
source
theorem Std.HashMap.getElem!_eq_default_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m.contains a = false → m[a]! = default
source
theorem Std.HashMap.getElem!_eq_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
¬a ∈ m → m[a]! = default
source
theorem Std.HashMap.getElem!_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
(m.erase k)[a]! = if (k == a) = true then default else m[a]!
source
@[simp]
theorem Std.HashMap.getElem!_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
(m.erase k)[k]! = default
source
theorem Std.HashMap.getElem?_eq_some_getElem!_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m.contains a = true → m[a]? = some m[a]!
source
theorem Std.HashMap.getElem?_eq_some_getElem! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
a ∈ m → m[a]? = some m[a]!
source
theorem Std.HashMap.getElem!_eq_get!_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m[a]! = m[a]?.get!
source
theorem Std.HashMap.getElem_eq_getElem! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {h' : a ∈ m} :
m[a] = m[a]!
source
theorem Std.HashMap.getElem!_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : α} (hab : (a == b) = true) :
m[a]! = m[b]!
source
@[simp]
theorem Std.HashMap.getD_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {fallback : β} {c : Nat} :
(Std.HashMap.empty c).getD a fallback = fallback
source
@[simp]
theorem Std.HashMap.getD_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {fallback : β} :
∅.getD a fallback = fallback
source
theorem Std.HashMap.getD_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.isEmpty = true → m.getD a fallback = fallback
source
theorem Std.HashMap.getD_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
(m.insert k v).getD a fallback = if (k == a) = true then v else m.getD a fallback
source
@[simp]
theorem Std.HashMap.getD_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} :
(m.insert k v).getD k fallback = v
source
theorem Std.HashMap.getD_eq_fallback_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.contains a = false → m.getD a fallback = fallback
source
theorem Std.HashMap.getD_eq_fallback {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
¬a ∈ m → m.getD a fallback = fallback
source
theorem Std.HashMap.getD_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
(m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
source
@[simp]
theorem Std.HashMap.getD_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
(m.erase k).getD k fallback = fallback
source
theorem Std.HashMap.getElem?_eq_some_getD_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.contains a = true → m[a]? = some (m.getD a fallback)
source
theorem Std.HashMap.getElem?_eq_some_getD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
a ∈ m → m[a]? = some (m.getD a fallback)
source
theorem Std.HashMap.getD_eq_getD_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.getD a fallback = m[a]?.getD fallback
source
theorem Std.HashMap.getElem_eq_getD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} {h' : a ∈ m} :
m[a] = m.getD a fallback
source
theorem Std.HashMap.getElem!_eq_getD_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m[a]! = m.getD a default
source
theorem Std.HashMap.getD_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β} (hab : (a == b) = true) :
m.getD a fallback = m.getD b fallback
source
@[simp]
theorem Std.HashMap.getKey?_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} :
(Std.HashMap.empty c).getKey? a = none
source
@[simp]
theorem Std.HashMap.getKey?_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} :
∅.getKey? a = none
source
theorem Std.HashMap.getKey?_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = true → m.getKey? a = none
source
theorem Std.HashMap.getKey?_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a
source
@[simp]
theorem Std.HashMap.getKey?_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).getKey? k = some k
source
theorem Std.HashMap.contains_eq_isSome_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.getKey? a).isSome
source
theorem Std.HashMap.getKey?_eq_none_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false → m.getKey? a = none
source
theorem Std.HashMap.getKey?_eq_none {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
¬a ∈ m → m.getKey? a = none
source
theorem Std.HashMap.getKey?_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a
source
@[simp]
theorem Std.HashMap.getKey?_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).getKey? k = none
source
theorem Std.HashMap.getKey_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v} :
(m.insert k v)[a] = if h₂ : (k == a) = true then v else m[a]
source
@[simp]
theorem Std.HashMap.getKey_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).getKey k ⋯ = k
source
@[simp]
theorem Std.HashMap.getKey_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {h' : a ∈ m.erase k} :
(m.erase k).getKey a h' = m.getKey a ⋯
source
theorem Std.HashMap.getKey?_eq_some_getKey {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h' : a ∈ m} :
m.getKey? a = some (m.getKey a h')
source
@[simp]
theorem Std.HashMap.getKey!_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited α] {a : α} {c : Nat} :
(Std.HashMap.empty c).getKey! a = default
source
@[simp]
theorem Std.HashMap.getKey!_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited α] {a : α} :
∅.getKey! a = default
source
theorem Std.HashMap.getKey!_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.isEmpty = true → m.getKey! a = default
source
theorem Std.HashMap.getKey!_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
(m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a
source
@[simp]
theorem Std.HashMap.getKey!_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {v : β} :
(m.insert k v).getKey! k = k
source
theorem Std.HashMap.getKey!_eq_default_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.contains a = false → m.getKey! a = default
source
theorem Std.HashMap.getKey!_eq_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
¬a ∈ m → m.getKey! a = default
source
theorem Std.HashMap.getKey!_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} :
(m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a
source
@[simp]
theorem Std.HashMap.getKey!_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} :
(m.erase k).getKey! k = default
source
theorem Std.HashMap.getKey?_eq_some_getKey!_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.contains a = true → m.getKey? a = some (m.getKey! a)
source
theorem Std.HashMap.getKey?_eq_some_getKey! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
a ∈ m → m.getKey? a = some (m.getKey! a)
source
theorem Std.HashMap.getKey!_eq_get!_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.getKey! a = (m.getKey? a).get!
source
theorem Std.HashMap.getKey_eq_getKey! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h' : a ∈ m} :
m.getKey a h' = m.getKey! a
source
@[simp]
theorem Std.HashMap.getKeyD_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a fallback : α} {c : Nat} :
(Std.HashMap.empty c).getKeyD a fallback = fallback
source
@[simp]
theorem Std.HashMap.getKeyD_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a fallback : α} :
∅.getKeyD a fallback = fallback
source
theorem Std.HashMap.getKeyD_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.isEmpty = true → m.getKeyD a fallback = fallback
source
theorem Std.HashMap.getKeyD_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
(m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback
source
@[simp]
theorem Std.HashMap.getKeyD_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k fallback : α} {v : β} :
(m.insert k v).getKeyD k fallback = k
source
theorem Std.HashMap.getKeyD_eq_fallback_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.contains a = false → m.getKeyD a fallback = fallback
source
theorem Std.HashMap.getKeyD_eq_fallback {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
¬a ∈ m → m.getKeyD a fallback = fallback
source
theorem Std.HashMap.getKeyD_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
(m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback
source
@[simp]
theorem Std.HashMap.getKeyD_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k fallback : α} :
(m.erase k).getKeyD k fallback = fallback
source
theorem Std.HashMap.getKey?_eq_some_getKeyD_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)
source
theorem Std.HashMap.getKey?_eq_some_getKeyD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
a ∈ m → m.getKey? a = some (m.getKeyD a fallback)
source
theorem Std.HashMap.getKeyD_eq_getD_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.getKeyD a fallback = (m.getKey? a).getD fallback
source
theorem Std.HashMap.getKey_eq_getKeyD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} {h' : a ∈ m} :
m.getKey a h' = m.getKeyD a fallback
source
theorem Std.HashMap.getKey!_eq_getKeyD_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.getKey! a = m.getKeyD a default
source
@[simp]
theorem Std.HashMap.isEmpty_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).isEmpty = false
source
@[simp]
theorem Std.HashMap.contains_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a = (k == a || m.contains a)
source
@[simp]
theorem Std.HashMap.mem_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m
source
theorem Std.HashMap.contains_insertIfNew_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).contains k = true
source
theorem Std.HashMap.mem_insertIfNew_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
k ∈ m.insertIfNew k v
source
theorem Std.HashMap.contains_of_contains_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true
source
theorem Std.HashMap.mem_of_mem_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m
source
theorem Std.HashMap.contains_of_contains_insertIfNew' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true

This is a restatement of contains_insertIfNew that is written to exactly match the proof obligation in the statement of getElem_insertIfNew.

source
theorem Std.HashMap.mem_of_mem_insertIfNew' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ ¬k ∈ m) → a ∈ m

This is a restatement of mem_insertIfNew that is written to exactly match the proof obligation in the statement of getElem_insertIfNew.

source
theorem Std.HashMap.size_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1
source
theorem Std.HashMap.size_le_size_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
m.size ≤ (m.insertIfNew k v).size
source
theorem Std.HashMap.size_insertIfNew_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).size ≤ m.size + 1
source
theorem Std.HashMap.getElem?_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v)[a]? = if (k == a) = true ∧ ¬k ∈ m then some v else m[a]?
source
theorem Std.HashMap.getElem_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v} :
(m.insertIfNew k v)[a] = if h₂ : (k == a) = true ∧ ¬k ∈ m then v else m[a]
source
theorem Std.HashMap.getElem!_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
(m.insertIfNew k v)[a]! = if (k == a) = true ∧ ¬k ∈ m then v else m[a]!
source
theorem Std.HashMap.getD_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
(m.insertIfNew k v).getD a fallback = if (k == a) = true ∧ ¬k ∈ m then v else m.getD a fallback
source
theorem Std.HashMap.getKey?_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).getKey? a = if (k == a) = true ∧ ¬k ∈ m then some k else m.getKey? a
source
theorem Std.HashMap.getKey_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v} :
(m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then k else m.getKey a ⋯
source
theorem Std.HashMap.getKey!_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
(m.insertIfNew k v).getKey! a = if (k == a) = true ∧ ¬k ∈ m then k else m.getKey! a
source
theorem Std.HashMap.getKeyD_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
(m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ ¬k ∈ m then k else m.getKeyD a fallback
source
@[simp]
theorem Std.HashMap.getThenInsertIfNew?_fst {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {k : α} {v : β} :
(m.getThenInsertIfNew? k v).fst = m.get? k
source
@[simp]
theorem Std.HashMap.getThenInsertIfNew?_snd {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {k : α} {v : β} :
(m.getThenInsertIfNew? k v).snd = m.insertIfNew k v
source
instance Std.HashMap.instLawfulGetElemMemOfEquivBEqOfLawfulHashable {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] :
LawfulGetElem (Std.HashMap α β) α β fun (m : Std.HashMap α β) (a : α) => a ∈ m
Equations
  • ⋯ = ⋯