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 α.

@[simp]

theorem Std.HashMap.isEmpty_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {c : Nat} : (empty c).isEmpty = true

@[simp]

theorem Std.HashMap.isEmpty_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} : ∅.isEmpty = true

@[simp]

theorem Std.HashMap.isEmpty_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insert k v).isEmpty = false

theorem Std.HashMap.mem_iff_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {a : α} : a ∈ m ↔ m.contains a = true

theorem Std.HashMap.contains_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) : m.contains a = m.contains b

theorem Std.HashMap.mem_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) : a ∈ m ↔ b ∈ m

@[simp]

theorem Std.HashMap.contains_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} : (empty c).contains a = false

@[simp]

theorem Std.HashMap.get_eq_getElem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {a : α} {h : a ∈ m} : m.get a h = m[a]

@[simp]

theorem Std.HashMap.get?_eq_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {a : α} : m.get? a = m[a]?

@[simp]

theorem Std.HashMap.get!_eq_getElem! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [Inhabited β] {a : α} : m.get! a = m[a]!

@[simp]

theorem Std.HashMap.not_mem_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} : ¬a ∈ empty c

@[simp]

theorem Std.HashMap.contains_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅.contains a = false

@[simp]

theorem Std.HashMap.not_mem_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ¬a ∈ ∅

theorem Std.HashMap.contains_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m.contains a = false

theorem Std.HashMap.not_mem_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → ¬a ∈ m

theorem Std.HashMap.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] : m.isEmpty = false ↔ ∃ (a : α), m.contains a = true

theorem Std.HashMap.isEmpty_eq_false_iff_exists_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] : m.isEmpty = false ↔ ∃ (a : α), a ∈ m

theorem Std.HashMap.isEmpty_iff_forall_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] : m.isEmpty = true ↔ ∀ (a : α), m.contains a = false

theorem Std.HashMap.isEmpty_iff_forall_not_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] : m.isEmpty = true ↔ ∀ (a : α), ¬a ∈ m

@[simp]

theorem Std.HashMap.insert_eq_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {p : α × β} : Insert.insert p m = m.insert p.fst p.snd

@[simp]

theorem Std.HashMap.singleton_eq_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {p : α × β} : {p} = ∅.insert p.fst p.snd

@[simp]

theorem Std.HashMap.contains_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : (m.insert k v).contains a = (k == a || m.contains a)

@[simp]

theorem Std.HashMap.mem_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m

theorem Std.HashMap.contains_of_contains_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : (m.insert k v).contains a = true → (k == a) = false → m.contains a = true

theorem Std.HashMap.mem_of_mem_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : a ∈ m.insert k v → (k == a) = false → a ∈ m

theorem Std.HashMap.contains_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insert k v).contains k = true

theorem Std.HashMap.mem_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k ∈ m.insert k v

@[simp]

theorem Std.HashMap.size_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {c : Nat} : (empty c).size = 0

@[simp]

theorem Std.HashMap.size_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} : ∅.size = 0

theorem Std.HashMap.isEmpty_eq_size_eq_zero {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} : m.isEmpty = (m.size == 0)

theorem Std.HashMap.size_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insert k v).size = if k ∈ m then m.size else m.size + 1

theorem Std.HashMap.size_le_size_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : m.size ≤ (m.insert k v).size

theorem Std.HashMap.size_insert_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insert k v).size ≤ m.size + 1

@[simp]

theorem Std.HashMap.erase_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} : (empty c).erase a = empty c

@[simp]

theorem Std.HashMap.erase_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅.erase a = ∅

@[simp]

theorem Std.HashMap.isEmpty_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)

@[simp]

theorem Std.HashMap.contains_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).contains a = (!k == a && m.contains a)

@[simp]

theorem Std.HashMap.mem_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m

theorem Std.HashMap.contains_of_contains_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).contains a = true → m.contains a = true

theorem Std.HashMap.mem_of_mem_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k → a ∈ m

theorem Std.HashMap.size_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size = if k ∈ m then m.size - 1 else m.size

theorem Std.HashMap.size_erase_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size

theorem Std.HashMap.size_le_size_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} : m.size ≤ (m.erase k).size + 1

@[simp]

theorem Std.HashMap.containsThenInsert_fst {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {k : α} {v : β} : (m.containsThenInsert k v).fst = m.contains k

@[simp]

theorem Std.HashMap.containsThenInsert_snd {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {k : α} {v : β} : (m.containsThenInsert k v).snd = m.insert k v

@[simp]

theorem Std.HashMap.containsThenInsertIfNew_fst {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {k : α} {v : β} : (m.containsThenInsertIfNew k v).fst = m.contains k

@[simp]

theorem Std.HashMap.containsThenInsertIfNew_snd {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {k : α} {v : β} : (m.containsThenInsertIfNew k v).snd = m.insertIfNew k v

@[simp]

theorem Std.HashMap.getElem?_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} : (empty c)[a]? = none

@[simp]

theorem Std.HashMap.getElem?_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅[a]? = none

theorem Std.HashMap.getElem?_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m[a]? = none

theorem Std.HashMap.getElem?_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : (m.insert k v)[a]? = if (k == a) = true then some v else m[a]?

@[simp]

theorem Std.HashMap.getElem?_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insert k v)[k]? = some v

theorem Std.HashMap.contains_eq_isSome_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = m[a]?.isSome

theorem Std.HashMap.getElem?_eq_none_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → m[a]? = none

theorem Std.HashMap.getElem?_eq_none {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m[a]? = none

theorem Std.HashMap.getElem?_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k)[a]? = if (k == a) = true then none else m[a]?

@[simp]

theorem Std.HashMap.getElem?_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k)[k]? = none

theorem Std.HashMap.getElem?_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) : m[a]? = m[b]?

theorem Std.HashMap.getElem_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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]

@[simp]

theorem Std.HashMap.getElem_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insert k v)[k] = v

@[simp]

theorem Std.HashMap.getElem_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {h' : a ∈ m.erase k} : (m.erase k)[a] = m[a]

theorem Std.HashMap.getElem?_eq_some_getElem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h' : a ∈ m} : m[a]? = some m[a]

theorem Std.HashMap.getElem_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [LawfulBEq α] {a b : α} (hab : (a == b) = true) {h' : a ∈ m} : m[a] = m[b]

@[simp]

theorem Std.HashMap.getElem!_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited β] {a : α} {c : Nat} : (empty c)[a]! = default

@[simp]

theorem Std.HashMap.getElem!_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited β] {a : α} : ∅[a]! = default

theorem Std.HashMap.getElem!_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m.isEmpty = true → m[a]! = default

theorem Std.HashMap.getElem!_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : (m.insert k v)[a]! = if (k == a) = true then v else m[a]!

@[simp]

theorem Std.HashMap.getElem!_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} : (m.insert k v)[k]! = v

theorem Std.HashMap.getElem!_eq_default_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m.contains a = false → m[a]! = default

theorem Std.HashMap.getElem!_eq_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : ¬a ∈ m → m[a]! = default

theorem Std.HashMap.getElem!_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : (m.erase k)[a]! = if (k == a) = true then default else m[a]!

@[simp]

theorem Std.HashMap.getElem!_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} : (m.erase k)[k]! = default

theorem Std.HashMap.getElem?_eq_some_getElem!_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m.contains a = true → m[a]? = some m[a]!

theorem Std.HashMap.getElem?_eq_some_getElem! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : a ∈ m → m[a]? = some m[a]!

theorem Std.HashMap.getElem!_eq_get!_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m[a]! = m[a]?.get!

theorem Std.HashMap.getElem_eq_getElem! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {h' : a ∈ m} : m[a] = m[a]!

theorem Std.HashMap.getElem!_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : α} (hab : (a == b) = true) : m[a]! = m[b]!

@[simp]

theorem Std.HashMap.getD_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {fallback : β} {c : Nat} : (empty c).getD a fallback = fallback

@[simp]

theorem Std.HashMap.getD_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {fallback : β} : ∅.getD a fallback = fallback

theorem Std.HashMap.getD_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : m.isEmpty = true → m.getD a fallback = fallback

theorem Std.HashMap.getD_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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

@[simp]

theorem Std.HashMap.getD_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} : (m.insert k v).getD k fallback = v

theorem Std.HashMap.getD_eq_fallback_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : m.contains a = false → m.getD a fallback = fallback

theorem Std.HashMap.getD_eq_fallback {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : ¬a ∈ m → m.getD a fallback = fallback

theorem Std.HashMap.getD_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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.getD_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} : (m.erase k).getD k fallback = fallback

theorem Std.HashMap.getElem?_eq_some_getD_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : m.contains a = true → m[a]? = some (m.getD a fallback)

theorem Std.HashMap.getElem?_eq_some_getD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : a ∈ m → m[a]? = some (m.getD a fallback)

theorem Std.HashMap.getD_eq_getD_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} : m.getD a fallback = m[a]?.getD fallback

theorem Std.HashMap.getElem_eq_getD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} {h' : a ∈ m} : m[a] = m.getD a fallback

theorem Std.HashMap.getElem!_eq_getD_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : m[a]! = m.getD a default

theorem Std.HashMap.getD_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β} (hab : (a == b) = true) : m.getD a fallback = m.getD b fallback

@[simp]

theorem Std.HashMap.getKey?_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} {c : Nat} : (empty c).getKey? a = none

@[simp]

theorem Std.HashMap.getKey?_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a : α} : ∅.getKey? a = none

theorem Std.HashMap.getKey?_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} : m.isEmpty = true → m.getKey? a = none

theorem Std.HashMap.getKey?_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : (m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a

@[simp]

theorem Std.HashMap.getKey?_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insert k v).getKey? k = some k

theorem Std.HashMap.contains_eq_isSome_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = (m.getKey? a).isSome

theorem Std.HashMap.getKey?_eq_none_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a = false → m.getKey? a = none

theorem Std.HashMap.getKey?_eq_none {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.getKey? a = none

theorem Std.HashMap.getKey?_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} : (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a

@[simp]

theorem Std.HashMap.getKey?_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).getKey? k = none

theorem Std.HashMap.getKey_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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]

@[simp]

theorem Std.HashMap.getKey_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insert k v).getKey k ⋯ = k

@[simp]

theorem Std.HashMap.getKey_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {h' : a ∈ m.erase k} : (m.erase k).getKey a h' = m.getKey a ⋯

theorem Std.HashMap.getKey?_eq_some_getKey {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h' : a ∈ m} : m.getKey? a = some (m.getKey a h')

@[simp]

theorem Std.HashMap.getKey!_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited α] {a : α} {c : Nat} : (empty c).getKey! a = default

@[simp]

theorem Std.HashMap.getKey!_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [Inhabited α] {a : α} : ∅.getKey! a = default

theorem Std.HashMap.getKey!_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.isEmpty = true → m.getKey! a = default

theorem Std.HashMap.getKey!_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} : (m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a

@[simp]

theorem Std.HashMap.getKey!_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {v : β} : (m.insert k v).getKey! k = k

theorem Std.HashMap.getKey!_eq_default_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.contains a = false → m.getKey! a = default

theorem Std.HashMap.getKey!_eq_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : ¬a ∈ m → m.getKey! a = default

theorem Std.HashMap.getKey!_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} : (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a

@[simp]

theorem Std.HashMap.getKey!_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : (m.erase k).getKey! k = default

theorem Std.HashMap.getKey?_eq_some_getKey!_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.contains a = true → m.getKey? a = some (m.getKey! a)

theorem Std.HashMap.getKey?_eq_some_getKey! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : a ∈ m → m.getKey? a = some (m.getKey! a)

theorem Std.HashMap.getKey!_eq_get!_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.getKey! a = (m.getKey? a).get!

theorem Std.HashMap.getKey_eq_getKey! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h' : a ∈ m} : m.getKey a h' = m.getKey! a

@[simp]

theorem Std.HashMap.getKeyD_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a fallback : α} {c : Nat} : (empty c).getKeyD a fallback = fallback

@[simp]

theorem Std.HashMap.getKeyD_emptyc {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {a fallback : α} : ∅.getKeyD a fallback = fallback

theorem Std.HashMap.getKeyD_of_isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.isEmpty = true → m.getKeyD a fallback = fallback

theorem Std.HashMap.getKeyD_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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

@[simp]

theorem Std.HashMap.getKeyD_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k fallback : α} {v : β} : (m.insert k v).getKeyD k fallback = k

theorem Std.HashMap.getKeyD_eq_fallback_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.contains a = false → m.getKeyD a fallback = fallback

theorem Std.HashMap.getKeyD_eq_fallback {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} : ¬a ∈ m → m.getKeyD a fallback = fallback

theorem Std.HashMap.getKeyD_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a fallback : α} : (m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback

@[simp]

theorem Std.HashMap.getKeyD_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k fallback : α} : (m.erase k).getKeyD k fallback = fallback

theorem Std.HashMap.getKey?_eq_some_getKeyD_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)

theorem Std.HashMap.getKey?_eq_some_getKeyD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} : a ∈ m → m.getKey? a = some (m.getKeyD a fallback)

theorem Std.HashMap.getKeyD_eq_getD_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} : m.getKeyD a fallback = (m.getKey? a).getD fallback

theorem Std.HashMap.getKey_eq_getKeyD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} {h' : a ∈ m} : m.getKey a h' = m.getKeyD a fallback

theorem Std.HashMap.getKey!_eq_getKeyD_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} : m.getKey! a = m.getKeyD a default

@[simp]

theorem Std.HashMap.isEmpty_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insertIfNew k v).isEmpty = false

@[simp]

theorem Std.HashMap.contains_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : (m.insertIfNew k v).contains a = (k == a || m.contains a)

@[simp]

theorem Std.HashMap.mem_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m

theorem Std.HashMap.contains_insertIfNew_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insertIfNew k v).contains k = true

theorem Std.HashMap.mem_insertIfNew_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k ∈ m.insertIfNew k v

theorem Std.HashMap.contains_of_contains_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true

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

theorem Std.HashMap.contains_of_contains_insertIfNew' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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.

theorem Std.HashMap.mem_of_mem_insertIfNew' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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.

theorem Std.HashMap.size_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1

theorem Std.HashMap.size_le_size_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : m.size ≤ (m.insertIfNew k v).size

theorem Std.HashMap.size_insertIfNew_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insertIfNew k v).size ≤ m.size + 1

theorem Std.HashMap.getElem?_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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.getElem_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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]

theorem Std.HashMap.getElem!_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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.getD_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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

theorem Std.HashMap.getKey?_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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

theorem Std.HashMap.getKey_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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 ⋯

theorem Std.HashMap.getKey!_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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

theorem Std.HashMap.getKeyD_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : 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

@[simp]

theorem Std.HashMap.getThenInsertIfNew?_fst {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {k : α} {v : β} : (m.getThenInsertIfNew? k v).fst = m.get? k

@[simp]

theorem Std.HashMap.getThenInsertIfNew?_snd {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {k : α} {v : β} : (m.getThenInsertIfNew? k v).snd = m.insertIfNew k v

instance Std.HashMap.instLawfulGetElemMemOfEquivBEqOfLawfulHashable {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β fun (m : HashMap α β) (a : α) => a ∈ m

@[simp]

theorem Std.HashMap.length_keys {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] : m.keys.length = m.size

@[simp]

theorem Std.HashMap.isEmpty_keys {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] : m.keys.isEmpty = m.isEmpty

@[simp]

theorem Std.HashMap.contains_keys {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} : m.keys.contains k = m.contains k

@[simp]

theorem Std.HashMap.mem_keys {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [LawfulBEq α] [LawfulHashable α] {k : α} : k ∈ m.keys ↔ k ∈ m

theorem Std.HashMap.distinct_keys {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] : List.Pairwise (fun (a b : α) => (a == b) = false) m.keys

@[simp]

theorem Std.HashMap.insertMany_nil {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} : m.insertMany [] = m

@[simp]

theorem Std.HashMap.insertMany_list_singleton {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {k : α} {v : β} : m.insertMany [(k, v)] = m.insert k v

theorem Std.HashMap.insertMany_cons {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} {l : List (α × β)} {k : α} {v : β} : m.insertMany ((k, v) :: l) = (m.insert k v).insertMany l

@[simp]

theorem Std.HashMap.contains_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} : (m.insertMany l).contains k = (m.contains k || (List.map Prod.fst l).contains k)

@[simp]

theorem Std.HashMap.mem_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} : k ∈ m.insertMany l ↔ k ∈ m ∨ (List.map Prod.fst l).contains k = true

theorem Std.HashMap.mem_of_mem_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (mem : k ∈ m.insertMany l) (contains_eq_false : (List.map Prod.fst l).contains k = false) : k ∈ m

theorem Std.HashMap.getElem?_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (m.insertMany l)[k]? = m[k]?

theorem Std.HashMap.getElem?_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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) : (m.insertMany l)[k']? = some v

theorem Std.HashMap.getElem_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h : k ∈ m.insertMany l} : (m.insertMany l)[k] = m[k]

theorem Std.HashMap.getElem_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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' ∈ m.insertMany l} : (m.insertMany l)[k'] = v

theorem Std.HashMap.getElem!_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (m.insertMany l)[k]! = m[k]!

theorem Std.HashMap.getElem!_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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) : (m.insertMany l)[k']! = v

theorem Std.HashMap.getD_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (m.insertMany l).getD k fallback = m.getD k fallback

theorem Std.HashMap.getD_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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) : (m.insertMany l).getD k' fallback = v

theorem Std.HashMap.getKey?_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (m.insertMany l).getKey? k = m.getKey? k

theorem Std.HashMap.getKey?_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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) : (m.insertMany l).getKey? k' = some k

theorem Std.HashMap.getKey_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h : k ∈ m.insertMany l} : (m.insertMany l).getKey k h = m.getKey k ⋯

theorem Std.HashMap.getKey_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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' ∈ m.insertMany l} : (m.insertMany l).getKey k' h = k

theorem Std.HashMap.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (m.insertMany l).getKey! k = m.getKey! k

theorem Std.HashMap.getKey!_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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) : (m.insertMany l).getKey! k' = k

theorem Std.HashMap.getKeyD_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (m.insertMany l).getKeyD k fallback = m.getKeyD k fallback

theorem Std.HashMap.getKeyD_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [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) : (m.insertMany l).getKeyD k' fallback = k

theorem Std.HashMap.size_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) : (∀ (a : α), a ∈ m → (List.map Prod.fst l).contains a = false) → (m.insertMany l).size = m.size + l.length

theorem Std.HashMap.size_le_size_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : m.size ≤ (m.insertMany l).size

theorem Std.HashMap.size_insertMany_list_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (m.insertMany l).size ≤ m.size + l.length

@[simp]

theorem Std.HashMap.isEmpty_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)

@[simp]

theorem Std.HashMap.insertManyIfNewUnit_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} : m.insertManyIfNewUnit [] = m

@[simp]

theorem Std.HashMap.insertManyIfNewUnit_list_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} {k : α} : m.insertManyIfNewUnit [k] = m.insertIfNew k ()

theorem Std.HashMap.insertManyIfNewUnit_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} {l : List α} {k : α} : m.insertManyIfNewUnit (k :: l) = (m.insertIfNew k ()).insertManyIfNewUnit l

@[simp]

theorem Std.HashMap.contains_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : (m.insertManyIfNewUnit l).contains k = (m.contains k || l.contains k)

@[simp]

theorem Std.HashMap.mem_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : k ∈ m.insertManyIfNewUnit l ↔ k ∈ m ∨ l.contains k = true

theorem Std.HashMap.mem_of_mem_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) : k ∈ m.insertManyIfNewUnit l → k ∈ m

theorem Std.HashMap.getElem?_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : (m.insertManyIfNewUnit l)[k]? = if k ∈ m ∨ l.contains k = true then some () else none

theorem Std.HashMap.getElem_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} {l : List α} {k : α} {h : k ∈ m.insertManyIfNewUnit l} : (m.insertManyIfNewUnit l)[k] = ()

theorem Std.HashMap.getElem!_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} {l : List α} {k : α} : (m.insertManyIfNewUnit l)[k]! = ()

theorem Std.HashMap.getD_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} {l : List α} {k : α} {fallback : Unit} : (m.insertManyIfNewUnit l).getD k fallback = ()

theorem Std.HashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) : (m.insertManyIfNewUnit l).getKey? k = none

theorem Std.HashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α 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) : (m.insertManyIfNewUnit l).getKey? k' = some k

theorem Std.HashMap.getKey?_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (mem : k ∈ m) : (m.insertManyIfNewUnit l).getKey? k = m.getKey? k

theorem Std.HashMap.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α 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' ∈ m.insertManyIfNewUnit l} : (m.insertManyIfNewUnit l).getKey k' h = k

theorem Std.HashMap.getKey_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (mem : k ∈ m) {h : k ∈ m.insertManyIfNewUnit l} : (m.insertManyIfNewUnit l).getKey k h = m.getKey k mem

theorem Std.HashMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) : (m.insertManyIfNewUnit l).getKey! k = default

theorem Std.HashMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α 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) : (m.insertManyIfNewUnit l).getKey! k' = k

theorem Std.HashMap.getKey!_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (mem : k ∈ m) : (m.insertManyIfNewUnit l).getKey! k = m.getKey! k

theorem Std.HashMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) : (m.insertManyIfNewUnit l).getKeyD k fallback = fallback

theorem Std.HashMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α 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) : (m.insertManyIfNewUnit l).getKeyD k' fallback = k

theorem Std.HashMap.getKeyD_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (mem : k ∈ m) : (m.insertManyIfNewUnit l).getKeyD k fallback = m.getKeyD k fallback

theorem Std.HashMap.size_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) : (∀ (a : α), a ∈ m → l.contains a = false) → (m.insertManyIfNewUnit l).size = m.size + l.length

theorem Std.HashMap.size_le_size_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} : m.size ≤ (m.insertManyIfNewUnit l).size

theorem Std.HashMap.size_insertManyIfNewUnit_list_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} : (m.insertManyIfNewUnit l).size ≤ m.size + l.length

@[simp]

theorem Std.HashMap.isEmpty_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} : (m.insertManyIfNewUnit l).isEmpty = (m.isEmpty && l.isEmpty)

@[simp]

theorem Std.HashMap.ofList_nil {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} : ofList [] = ∅

@[simp]

theorem Std.HashMap.ofList_singleton {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {k : α} {v : β} : ofList [(k, v)] = ∅.insert k v

theorem Std.HashMap.ofList_cons {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {k : α} {v : β} {tl : List (α × β)} : ofList ((k, v) :: tl) = (∅.insert k v).insertMany tl

@[simp]

theorem Std.HashMap.contains_ofList {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} : (ofList l).contains k = (List.map Prod.fst l).contains k

@[simp]

theorem Std.HashMap.mem_ofList {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} : k ∈ ofList l ↔ (List.map Prod.fst l).contains k = true

theorem Std.HashMap.getElem?_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (ofList l)[k]? = none

theorem Std.HashMap.getElem?_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {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) : (ofList l)[k']? = some v

theorem Std.HashMap.getElem_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) {h : k' ∈ ofList l} : (ofList l)[k'] = v

theorem Std.HashMap.getElem!_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {l : List (α × β)} {k : α} [Inhabited β] (contains_eq_false : (List.map Prod.fst l).contains k = false) : (ofList l)[k]! = default

theorem Std.HashMap.getElem!_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} [Inhabited β] (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) : (ofList l)[k']! = v

theorem Std.HashMap.getD_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (ofList l).getD k fallback = fallback

theorem Std.HashMap.getD_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {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) : (ofList l).getD k' fallback = v

theorem Std.HashMap.getKey?_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (ofList l).getKey? k = none

theorem Std.HashMap.getKey?_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [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) : (ofList l).getKey? k' = some k

theorem Std.HashMap.getKey_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [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} : (ofList l).getKey k' h = k

theorem Std.HashMap.getKey!_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (ofList l).getKey! k = default

theorem Std.HashMap.getKey!_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [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) : (ofList l).getKey! k' = k

theorem Std.HashMap.getKeyD_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (ofList l).getKeyD k fallback = fallback

theorem Std.HashMap.getKeyD_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [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) : (ofList l).getKeyD k' fallback = k

theorem Std.HashMap.size_ofList {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) : (ofList l).size = l.length

theorem Std.HashMap.size_ofList_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (ofList l).size ≤ l.length

@[simp]

theorem Std.HashMap.isEmpty_ofList {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (ofList l).isEmpty = l.isEmpty

@[simp]

theorem Std.HashMap.unitOfList_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} : unitOfList [] = ∅

@[simp]

theorem Std.HashMap.unitOfList_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {k : α} : unitOfList [k] = ∅.insertIfNew k ()

theorem Std.HashMap.unitOfList_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {hd : α} {tl : List α} : unitOfList (hd :: tl) = (∅.insertIfNew hd ()).insertManyIfNewUnit tl

@[simp]

theorem Std.HashMap.contains_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : (unitOfList l).contains k = l.contains k

@[simp]

theorem Std.HashMap.mem_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : k ∈ unitOfList l ↔ l.contains k = true

@[simp]

theorem Std.HashMap.getElem?_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : (unitOfList l)[k]? = if l.contains k = true then some () else none

@[simp]

theorem Std.HashMap.getElem_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {l : List α} {k : α} {h : k ∈ unitOfList l} : (unitOfList l)[k] = ()

@[simp]

theorem Std.HashMap.getElem!_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {l : List α} {k : α} : (unitOfList l)[k]! = ()

@[simp]

theorem Std.HashMap.getD_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {l : List α} {k : α} {fallback : Unit} : (unitOfList l).getD k fallback = ()

theorem Std.HashMap.getKey?_unitOfList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) : (unitOfList l).getKey? k = none

theorem Std.HashMap.getKey?_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) : (unitOfList l).getKey? k' = some k

theorem Std.HashMap.getKey_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) {h : k' ∈ unitOfList l} : (unitOfList l).getKey k' h = k

theorem Std.HashMap.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) : (unitOfList l).getKey! k = default

theorem Std.HashMap.getKey!_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) : (unitOfList l).getKey! k' = k

theorem Std.HashMap.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) : (unitOfList l).getKeyD k fallback = fallback

theorem Std.HashMap.getKeyD_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) : (unitOfList l).getKeyD k' fallback = k

theorem Std.HashMap.size_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) : (unitOfList l).size = l.length

theorem Std.HashMap.size_unitOfList_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} : (unitOfList l).size ≤ l.length

@[simp]

theorem Std.HashMap.isEmpty_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} : (unitOfList l).isEmpty = l.isEmpty

theorem Std.HashMap.isEmpty_alter_eq_isEmpty_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : (m.alter k f).isEmpty = ((m.erase k).isEmpty && (f (m.get? k)).isNone)

@[simp]

theorem Std.HashMap.isEmpty_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : (m.alter k f).isEmpty = ((m.isEmpty || m.size == 1 && m.contains k) && (f (m.get? k)).isNone)

theorem Std.HashMap.contains_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} : (m.alter k f).contains k' = if (k == k') = true then (f (m.get? k)).isSome else m.contains k'

theorem Std.HashMap.mem_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} : k' ∈ m.alter k f ↔ if (k == k') = true then (f (m.get? k)).isSome = true else k' ∈ m

theorem Std.HashMap.mem_alter_of_beq {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : (k == k') = true) : k' ∈ m.alter k f ↔ (f (m.get? k)).isSome = true

@[simp]

theorem Std.HashMap.contains_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : (m.alter k f).contains k = (f (m.get? k)).isSome

@[simp]

theorem Std.HashMap.mem_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : k ∈ m.alter k f ↔ (f (m.get? k)).isSome = true

theorem Std.HashMap.contains_alter_of_beq_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : (k == k') = false) : (m.alter k f).contains k' = m.contains k'

theorem Std.HashMap.mem_alter_of_beq_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : (k == k') = false) : k' ∈ m.alter k f ↔ k' ∈ m

theorem Std.HashMap.size_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [LawfulBEq α] {k : α} {f : Option β → Option β} : (m.alter k f).size = if (m.contains k && (f (m.get? k)).isNone) = true then m.size - 1 else if (!m.contains k && (f (m.get? k)).isSome) = true then m.size + 1 else m.size

theorem Std.HashMap.size_alter_eq_add_one {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [LawfulBEq α] {k : α} {f : Option β → Option β} (h : ¬k ∈ m) (h' : (f (m.get? k)).isSome = true) : (m.alter k f).size = m.size + 1

theorem Std.HashMap.size_alter_eq_sub_one {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [LawfulBEq α] {k : α} {f : Option β → Option β} (h : k ∈ m) (h' : (f (m.get? k)).isNone = true) : (m.alter k f).size = m.size - 1

theorem Std.HashMap.size_alter_eq_self_of_not_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [LawfulBEq α] {k : α} {f : Option β → Option β} (h : ¬k ∈ m) (h' : (f (m.get? k)).isNone = true) : (m.alter k f).size = m.size

theorem Std.HashMap.size_alter_eq_self_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [LawfulBEq α] {k : α} {f : Option β → Option β} (h : k ∈ m) (h' : (f (m.get? k)).isSome = true) : (m.alter k f).size = m.size

theorem Std.HashMap.size_alter_le_size {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [LawfulBEq α] {k : α} {f : Option β → Option β} : (m.alter k f).size ≤ m.size + 1

theorem Std.HashMap.size_le_size_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [LawfulBEq α] {k : α} {f : Option β → Option β} : m.size - 1 ≤ (m.alter k f).size

theorem Std.HashMap.get?_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} : (m.alter k f).get? k' = if (k == k') = true then f (m.get? k) else m.get? k'

@[simp]

theorem Std.HashMap.get?_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : (m.alter k f).get? k = f (m.get? k)

theorem Std.HashMap.get_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} {h : k' ∈ m.alter k f} : (m.alter k f).get k' h = if heq : (k == k') = true then (f (m.get? k)).get ⋯ else m.get k' ⋯

@[simp]

theorem Std.HashMap.get_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} {h : k ∈ m.alter k f} : (m.alter k f).get k h = (f (m.get? k)).get ⋯

theorem Std.HashMap.get!_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : Option β → Option β} : (m.alter k f).get! k' = if (k == k') = true then (f (m.get? k)).get! else m.get! k'

@[simp]

theorem Std.HashMap.get!_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : Option β → Option β} : (m.alter k f).get! k = (f (m.get? k)).get!

theorem Std.HashMap.getD_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β} : (m.alter k f).getD k' fallback = if (k == k') = true then (f (m.get? k)).getD fallback else m.getD k' fallback

@[simp]

theorem Std.HashMap.getD_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : Option β → Option β} : (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback

theorem Std.HashMap.getKey?_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} : (m.alter k f).getKey? k' = if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k'

theorem Std.HashMap.getKey?_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : (m.alter k f).getKey? k = if (f (m.get? k)).isSome = true then some k else none

theorem Std.HashMap.getKey!_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : Option β → Option β} : (m.alter k f).getKey! k' = if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else m.getKey! k'

theorem Std.HashMap.getKey!_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : Option β → Option β} : (m.alter k f).getKey! k = if (f (m.get? k)).isSome = true then k else default

theorem Std.HashMap.getKey_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : Option β → Option β} {h : k' ∈ m.alter k f} : (m.alter k f).getKey k' h = if heq : (k == k') = true then k else m.getKey k' ⋯

@[simp]

theorem Std.HashMap.getKey_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : Option β → Option β} {h : k ∈ m.alter k f} : (m.alter k f).getKey k h = k

theorem Std.HashMap.getKeyD_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β} : (m.alter k f).getKeyD k' fallback = if (k == k') = true then if (f (m.get? k)).isSome = true then k else fallback else m.getKeyD k' fallback

theorem Std.HashMap.getKeyD_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : Option β → Option β} : (m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome = true then k else fallback

@[simp]

theorem Std.HashMap.isEmpty_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : (m.modify k f).isEmpty = m.isEmpty

@[simp]

theorem Std.HashMap.contains_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} : (m.modify k f).contains k' = m.contains k'

@[simp]

theorem Std.HashMap.mem_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} : k' ∈ m.modify k f ↔ k' ∈ m

@[simp]

theorem Std.HashMap.size_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : (m.modify k f).size = m.size

theorem Std.HashMap.get?_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} : (m.modify k f).get? k' = if (k == k') = true then Option.map f (m.get? k) else m.get? k'

@[simp]

theorem Std.HashMap.get?_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : (m.modify k f).get? k = Option.map f (m.get? k)

theorem Std.HashMap.get_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} {h : k' ∈ m.modify k f} : (m.modify k f).get k' h = if heq : (k == k') = true then f (m.get k ⋯) else m.get k' ⋯

@[simp]

theorem Std.HashMap.get_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} {h : k ∈ m.modify k f} : (m.modify k f).get k h = f (m.get k ⋯)

theorem Std.HashMap.get!_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} : (m.modify k f).get! k' = if (k == k') = true then (Option.map f (m.get? k)).get! else m.get! k'

@[simp]

theorem Std.HashMap.get!_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} : (m.modify k f).get! k = (Option.map f (m.get? k)).get!

theorem Std.HashMap.getD_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} : (m.modify k f).getD k' fallback = if (k == k') = true then (Option.map f (m.get? k)).getD fallback else m.getD k' fallback

@[simp]

theorem Std.HashMap.getD_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} : (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback

theorem Std.HashMap.getKey?_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} : (m.modify k f).getKey? k' = if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'

theorem Std.HashMap.getKey?_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : (m.modify k f).getKey? k = if k ∈ m then some k else none

theorem Std.HashMap.getKey!_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} : (m.modify k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'

theorem Std.HashMap.getKey!_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} : (m.modify k f).getKey! k = if k ∈ m then k else default

theorem Std.HashMap.getKey_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} {h : k' ∈ m.modify k f} : (m.modify k f).getKey k' h = if (k == k') = true then k else m.getKey k' ⋯

@[simp]

theorem Std.HashMap.getKey_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} {h : k ∈ m.modify k f} : (m.modify k f).getKey k h = k

theorem Std.HashMap.getKeyD_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} : (m.modify k f).getKeyD k' fallback = if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback

theorem Std.HashMap.getKeyD_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : HashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β} : (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback