Documentation

Std.Data.HashMap.RawLemmas

Hash map lemmas #

This module contains lemmas about Std.Data.HashMap.Raw. Most of the lemmas require EquivBEq α and LawfulHashable α for the key type α. The easiest way to obtain these instances is to provide an instance of LawfulBEq α.

@[simp]
theorem Std.HashMap.Raw.isEmpty_empty {α : Type u} {β : Type v} [BEq α] [Hashable α] {c : Nat} :
@[simp]
theorem Std.HashMap.Raw.isEmpty_emptyc {α : Type u} {β : Type v} [BEq α] [Hashable α] :
.isEmpty = true
@[simp]
theorem Std.HashMap.Raw.isEmpty_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).isEmpty = false
theorem Std.HashMap.Raw.mem_iff_contains {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} {a : α} :
a m m.contains a = true
theorem Std.HashMap.Raw.contains_congr {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {b : α} (hab : (a == b) = true) :
m.contains a = m.contains b
theorem Std.HashMap.Raw.mem_congr {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {b : α} (hab : (a == b) = true) :
a m b m
@[simp]
theorem Std.HashMap.Raw.contains_empty {α : Type u} {β : Type v} [BEq α] [Hashable α] {a : α} {c : Nat} :
@[simp]
theorem Std.HashMap.Raw.get_eq_getElem {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} {a : α} {h : a m} :
m.get a h = m[a]
@[simp]
theorem Std.HashMap.Raw.get?_eq_getElem? {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} {a : α} :
m.get? a = m[a]?
@[simp]
theorem Std.HashMap.Raw.get!_eq_getElem! {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} [Inhabited β] {a : α} :
m.get! a = m[a]!
@[simp]
theorem Std.HashMap.Raw.not_mem_empty {α : Type u} {β : Type v} [BEq α] [Hashable α] {a : α} {c : Nat} :
@[simp]
theorem Std.HashMap.Raw.contains_emptyc {α : Type u} {β : Type v} [BEq α] [Hashable α] {a : α} :
.contains a = false
@[simp]
theorem Std.HashMap.Raw.not_mem_emptyc {α : Type u} {β : Type v} [BEq α] [Hashable α] {a : α} :
theorem Std.HashMap.Raw.contains_of_isEmpty {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = truem.contains a = false
theorem Std.HashMap.Raw.not_mem_of_isEmpty {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = true¬a m
theorem Std.HashMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] :
m.isEmpty = false ∃ (a : α), m.contains a = true
theorem Std.HashMap.Raw.isEmpty_eq_false_iff_exists_mem {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] :
m.isEmpty = false ∃ (a : α), a m
theorem Std.HashMap.Raw.isEmpty_iff_forall_contains {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] :
m.isEmpty = true ∀ (a : α), m.contains a = false
theorem Std.HashMap.Raw.isEmpty_iff_forall_not_mem {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] :
m.isEmpty = true ∀ (a : α), ¬a m
@[simp]
theorem Std.HashMap.Raw.contains_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
(m.insert k v).contains a = (k == a || m.contains a)
@[simp]
theorem Std.HashMap.Raw.mem_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
a m.insert k v (k == a) = true a m
theorem Std.HashMap.Raw.contains_of_contains_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
(m.insert k v).contains a = true(k == a) = falsem.contains a = true
theorem Std.HashMap.Raw.mem_of_mem_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
a m.insert k v(k == a) = falsea m
@[simp]
theorem Std.HashMap.Raw.contains_insert_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).contains k = true
@[simp]
theorem Std.HashMap.Raw.mem_insert_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
k m.insert k v
@[simp]
theorem Std.HashMap.Raw.size_empty {α : Type u} {β : Type v} {c : Nat} :
@[simp]
theorem Std.HashMap.Raw.size_emptyc {α : Type u} {β : Type v} :
.size = 0
theorem Std.HashMap.Raw.isEmpty_eq_size_eq_zero {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} :
m.isEmpty = (m.size == 0)
theorem Std.HashMap.Raw.size_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).size = if k m then m.size else m.size + 1
theorem Std.HashMap.Raw.size_le_size_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
m.size (m.insert k v).size
theorem Std.HashMap.Raw.size_insert_le {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).size m.size + 1
@[simp]
theorem Std.HashMap.Raw.erase_empty {α : Type u} {β : Type v} [BEq α] [Hashable α] {k : α} {c : Nat} :
@[simp]
theorem Std.HashMap.Raw.erase_emptyc {α : Type u} {β : Type v} [BEq α] [Hashable α] {k : α} :
.erase k =
@[simp]
theorem Std.HashMap.Raw.isEmpty_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)
@[simp]
theorem Std.HashMap.Raw.contains_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
(m.erase k).contains a = (!k == a && m.contains a)
@[simp]
theorem Std.HashMap.Raw.mem_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
a m.erase k (k == a) = false a m
theorem Std.HashMap.Raw.contains_of_contains_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
(m.erase k).contains a = truem.contains a = true
theorem Std.HashMap.Raw.mem_of_mem_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
a m.erase ka m
theorem Std.HashMap.Raw.size_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size = if k m then m.size - 1 else m.size
theorem Std.HashMap.Raw.size_erase_le {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size m.size
theorem Std.HashMap.Raw.size_le_size_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
m.size (m.erase k).size + 1
@[simp]
theorem Std.HashMap.Raw.containsThenInsert_fst {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) {k : α} {v : β} :
(m.containsThenInsert k v).fst = m.contains k
@[simp]
theorem Std.HashMap.Raw.containsThenInsert_snd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) {k : α} {v : β} :
(m.containsThenInsert k v).snd = m.insert k v
@[simp]
theorem Std.HashMap.Raw.containsThenInsertIfNew_fst {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) {k : α} {v : β} :
(m.containsThenInsertIfNew k v).fst = m.contains k
@[simp]
theorem Std.HashMap.Raw.containsThenInsertIfNew_snd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) {k : α} {v : β} :
(m.containsThenInsertIfNew k v).snd = m.insertIfNew k v
@[simp]
theorem Std.HashMap.Raw.getElem?_empty {α : Type u} {β : Type v} [BEq α] [Hashable α] {a : α} {c : Nat} :
@[simp]
theorem Std.HashMap.Raw.getElem?_emptyc {α : Type u} {β : Type v} [BEq α] [Hashable α] {a : α} :
[a]? = none
theorem Std.HashMap.Raw.getElem?_of_isEmpty {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
m.isEmpty = truem[a]? = none
theorem Std.HashMap.Raw.getElem?_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
(m.insert k v)[a]? = if (k == a) = true then some v else m[a]?
@[simp]
theorem Std.HashMap.Raw.getElem?_insert_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v)[k]? = some v
theorem Std.HashMap.Raw.contains_eq_isSome_getElem? {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = m[a]?.isSome
theorem Std.HashMap.Raw.getElem?_eq_none_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = falsem[a]? = none
theorem Std.HashMap.Raw.getElem?_eq_none {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
¬a mm[a]? = none
theorem Std.HashMap.Raw.getElem?_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
(m.erase k)[a]? = if (k == a) = true then none else m[a]?
@[simp]
theorem Std.HashMap.Raw.getElem?_erase_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k)[k]? = none
theorem Std.HashMap.Raw.getElem?_congr {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {b : α} (hab : (a == b) = true) :
m[a]? = m[b]?
theorem Std.HashMap.Raw.getElem_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [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]
@[simp]
theorem Std.HashMap.Raw.getElem_insert_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v)[k] = v
@[simp]
theorem Std.HashMap.Raw.getElem_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {h' : a m.erase k} :
(m.erase k)[a] = m[a]
theorem Std.HashMap.Raw.getElem?_eq_some_getElem {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {h' : a m} :
m[a]? = some m[a]
theorem Std.HashMap.Raw.getElem_congr {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [LawfulBEq α] {a : α} {b : α} (hab : (a == b) = true) {h' : a m} :
m[a] = m[b]
@[simp]
theorem Std.HashMap.Raw.getElem!_empty {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] {a : α} {c : Nat} :
(Std.HashMap.Raw.empty c)[a]! = default
@[simp]
theorem Std.HashMap.Raw.getElem!_emptyc {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] {a : α} :
[a]! = default
theorem Std.HashMap.Raw.getElem!_of_isEmpty {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m.isEmpty = truem[a]! = default
theorem Std.HashMap.Raw.getElem!_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {a : α} {v : β} :
(m.insert k v)[a]! = if (k == a) = true then v else m[a]!
@[simp]
theorem Std.HashMap.Raw.getElem!_insert_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
(m.insert k v)[k]! = v
theorem Std.HashMap.Raw.getElem!_eq_default_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m.contains a = falsem[a]! = default
theorem Std.HashMap.Raw.getElem!_eq_default {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
¬a mm[a]! = default
theorem Std.HashMap.Raw.getElem!_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {a : α} :
(m.erase k)[a]! = if (k == a) = true then default else m[a]!
@[simp]
theorem Std.HashMap.Raw.getElem!_erase_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
(m.erase k)[k]! = default
theorem Std.HashMap.Raw.getElem?_eq_some_getElem!_of_contains {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m.contains a = truem[a]? = some m[a]!
theorem Std.HashMap.Raw.getElem?_eq_some_getElem! {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
a mm[a]? = some m[a]!
theorem Std.HashMap.Raw.getElem!_eq_get!_getElem? {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m[a]! = m[a]?.get!
theorem Std.HashMap.Raw.getElem_eq_getElem! {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {h' : a m} :
m[a] = m[a]!
theorem Std.HashMap.Raw.getElem!_congr {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {b : α} (hab : (a == b) = true) :
m[a]! = m[b]!
@[simp]
theorem Std.HashMap.Raw.getD_empty {α : Type u} {β : Type v} [BEq α] [Hashable α] {a : α} {fallback : β} {c : Nat} :
(Std.HashMap.Raw.empty c).getD a fallback = fallback
@[simp]
theorem Std.HashMap.Raw.getD_emptyc {α : Type u} {β : Type v} [BEq α] [Hashable α] {a : α} {fallback : β} :
.getD a fallback = fallback
theorem Std.HashMap.Raw.getD_of_isEmpty {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.isEmpty = truem.getD a fallback = fallback
theorem Std.HashMap.Raw.getD_insert {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {fallback : β} {v : β} :
(m.insert k v).getD a fallback = if (k == a) = true then v else m.getD a fallback
@[simp]
theorem Std.HashMap.Raw.getD_insert_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {v : β} :
(m.insert k v).getD k fallback = v
theorem Std.HashMap.Raw.getD_eq_fallback_of_contains_eq_false {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.contains a = falsem.getD a fallback = fallback
theorem Std.HashMap.Raw.getD_eq_fallback {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
¬a mm.getD a fallback = fallback
theorem Std.HashMap.Raw.getD_erase {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {fallback : β} :
(m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
@[simp]
theorem Std.HashMap.Raw.getD_erase_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
(m.erase k).getD k fallback = fallback
theorem Std.HashMap.Raw.getElem?_eq_some_getD_of_contains {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.contains a = truem[a]? = some (m.getD a fallback)
theorem Std.HashMap.Raw.getElem?_eq_some_getD {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
a mm[a]? = some (m.getD a fallback)
theorem Std.HashMap.Raw.getD_eq_getD_getElem? {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.getD a fallback = m[a]?.getD fallback
theorem Std.HashMap.Raw.getElem_eq_getD {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} {h' : a m} :
m[a] = m.getD a fallback
theorem Std.HashMap.Raw.getElem!_eq_getD_default {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m[a]! = m.getD a default
theorem Std.HashMap.Raw.getD_congr {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {a : α} {b : α} {fallback : β} (hab : (a == b) = true) :
m.getD a fallback = m.getD b fallback
@[simp]
theorem Std.HashMap.Raw.isEmpty_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).isEmpty = false
@[simp]
theorem Std.HashMap.Raw.contains_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
(m.insertIfNew k v).contains a = (k == a || m.contains a)
@[simp]
theorem Std.HashMap.Raw.mem_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
a m.insertIfNew k v (k == a) = true a m
theorem Std.HashMap.Raw.contains_insertIfNew_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).contains k = true
theorem Std.HashMap.Raw.mem_insertIfNew_self {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
k m.insertIfNew k v
theorem Std.HashMap.Raw.contains_of_contains_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
(m.insertIfNew k v).contains a = true(k == a) = falsem.contains a = true
theorem Std.HashMap.Raw.mem_of_mem_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
a m.insertIfNew k v(k == a) = falsea m
theorem Std.HashMap.Raw.contains_of_contains_insertIfNew' {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [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.

theorem Std.HashMap.Raw.mem_of_mem_insertIfNew' {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [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.

theorem Std.HashMap.Raw.size_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).size = if k m then m.size else m.size + 1
theorem Std.HashMap.Raw.size_le_size_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
m.size (m.insertIfNew k v).size
theorem Std.HashMap.Raw.size_insertIfNew_le {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).size m.size + 1
theorem Std.HashMap.Raw.getElem?_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
(m.insertIfNew k v)[a]? = if (k == a) = true ¬k m then some v else m[a]?
theorem Std.HashMap.Raw.getElem_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [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]
theorem Std.HashMap.Raw.getElem!_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {a : α} {v : β} :
(m.insertIfNew k v)[a]! = if (k == a) = true ¬k m then v else m[a]!
theorem Std.HashMap.Raw.getD_insertIfNew {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) [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
@[simp]
theorem Std.HashMap.Raw.getThenInsertIfNew?_fst {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) {k : α} {v : β} :
(m.getThenInsertIfNew? k v).fst = m.get? k
@[simp]
theorem Std.HashMap.Raw.getThenInsertIfNew?_snd {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.HashMap.Raw α β} (h : m.WF) {k : α} {v : β} :
(m.getThenInsertIfNew? k v).snd = m.insertIfNew k v