Dependent hash map lemmas

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

@[simp]

theorem Std.DHashMap.isEmpty_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {c : Nat}, (Std.DHashMap.empty c).isEmpty = true

@[simp]

theorem Std.DHashMap.isEmpty_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α}, ∅.isEmpty = true

@[simp]

theorem Std.DHashMap.isEmpty_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).isEmpty = false

theorem Std.DHashMap.mem_iff_contains {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {a : α}, a ∈ m ↔ m.contains a = true

theorem Std.DHashMap.contains_congr {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a b : α}, (a == b) = true → m.contains a = m.contains b

theorem Std.DHashMap.mem_congr {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a b : α}, (a == b) = true → (a ∈ m ↔ b ∈ m)

@[simp]

theorem Std.DHashMap.contains_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α} {c : Nat}, (Std.DHashMap.empty c).contains a = false

@[simp]

theorem Std.DHashMap.not_mem_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α} {c : Nat}, ¬a ∈ Std.DHashMap.empty c

@[simp]

theorem Std.DHashMap.contains_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.contains a = false

@[simp]

theorem Std.DHashMap.not_mem_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α}, ¬a ∈ ∅

theorem Std.DHashMap.contains_of_isEmpty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, m.isEmpty = true → m.contains a = false

theorem Std.DHashMap.not_mem_of_isEmpty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, m.isEmpty = true → ¬a ∈ m

theorem Std.DHashMap.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α], m.isEmpty = false ↔ ∃ (a : α), m.contains a = true

theorem Std.DHashMap.isEmpty_eq_false_iff_exists_mem {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α], m.isEmpty = false ↔ ∃ (a : α), a ∈ m

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

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

@[simp]

theorem Std.DHashMap.insert_eq_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {p : (a : α) × β a}, insert p m = m.insert p.fst p.snd

@[simp]

theorem Std.DHashMap.singleton_eq_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {p : (a : α) × β a}, {p} = ∅.insert p.fst p.snd

@[simp]

theorem Std.DHashMap.contains_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, (m.insert k v).contains a = (k == a || m.contains a)

@[simp]

theorem Std.DHashMap.mem_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m

theorem Std.DHashMap.contains_of_contains_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, (m.insert k v).contains a = true → (k == a) = false → m.contains a = true

theorem Std.DHashMap.mem_of_mem_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, a ∈ m.insert k v → (k == a) = false → a ∈ m

@[simp]

theorem Std.DHashMap.contains_insert_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).contains k = true

@[simp]

theorem Std.DHashMap.mem_insert_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, k ∈ m.insert k v

@[simp]

theorem Std.DHashMap.size_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {c : Nat}, (Std.DHashMap.empty c).size = 0

@[simp]

theorem Std.DHashMap.size_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α}, ∅.size = 0

theorem Std.DHashMap.isEmpty_eq_size_eq_zero {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β}, m.isEmpty = (m.size == 0)

theorem Std.DHashMap.size_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).size = if k ∈ m then m.size else m.size + 1

theorem Std.DHashMap.size_le_size_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, m.size ≤ (m.insert k v).size

theorem Std.DHashMap.size_insert_le {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).size ≤ m.size + 1

@[simp]

theorem Std.DHashMap.erase_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {k : α} {c : Nat}, (Std.DHashMap.empty c).erase k = Std.DHashMap.empty c

@[simp]

theorem Std.DHashMap.erase_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {k : α}, ∅.erase k = ∅

@[simp]

theorem Std.DHashMap.isEmpty_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, (m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)

@[simp]

theorem Std.DHashMap.contains_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)

@[simp]

theorem Std.DHashMap.mem_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m

theorem Std.DHashMap.contains_of_contains_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, (m.erase k).contains a = true → m.contains a = true

theorem Std.DHashMap.mem_of_mem_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, a ∈ m.erase k → a ∈ m

theorem Std.DHashMap.size_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, (m.erase k).size = if k ∈ m then m.size - 1 else m.size

theorem Std.DHashMap.size_erase_le {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, (m.erase k).size ≤ m.size

theorem Std.DHashMap.size_le_size_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, m.size ≤ (m.erase k).size + 1

@[simp]

theorem Std.DHashMap.containsThenInsert_fst {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k}, (m.containsThenInsert k v).fst = m.contains k

@[simp]

theorem Std.DHashMap.containsThenInsert_snd {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k}, (m.containsThenInsert k v).snd = m.insert k v

@[simp]

theorem Std.DHashMap.containsThenInsertIfNew_fst {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k}, (m.containsThenInsertIfNew k v).fst = m.contains k

@[simp]

theorem Std.DHashMap.containsThenInsertIfNew_snd {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k}, (m.containsThenInsertIfNew k v).snd = m.insertIfNew k v

@[simp]

theorem Std.DHashMap.get?_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α} {c : Nat}, (Std.DHashMap.empty c).get? a = none

@[simp]

theorem Std.DHashMap.get?_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α}, ∅.get? a = none

theorem Std.DHashMap.get?_of_isEmpty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}, m.isEmpty = true → m.get? a = none

theorem Std.DHashMap.get?_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a k : α} {v : β k}, (m.insert k v).get? a = if h : (k == a) = true then some (cast ⋯ v) else m.get? a

@[simp]

theorem Std.DHashMap.get?_insert_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α} {v : β k}, (m.insert k v).get? k = some v

theorem Std.DHashMap.contains_eq_isSome_get? {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}, m.contains a = (m.get? a).isSome

theorem Std.DHashMap.get?_eq_none_of_contains_eq_false {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}, m.contains a = false → m.get? a = none

theorem Std.DHashMap.get?_eq_none {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}, ¬a ∈ m → m.get? a = none

theorem Std.DHashMap.get?_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}, (m.erase k).get? a = if (k == a) = true then none else m.get? a

@[simp]

theorem Std.DHashMap.get?_erase_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}, (m.erase k).get? k = none

@[simp]

theorem Std.DHashMap.Const.get?_empty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {a : α} {c : Nat}, Std.DHashMap.Const.get? (Std.DHashMap.empty c) a = none

@[simp]

theorem Std.DHashMap.Const.get?_emptyc {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {a : α}, Std.DHashMap.Const.get? ∅ a = none

theorem Std.DHashMap.Const.get?_of_isEmpty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, m.isEmpty = true → Std.DHashMap.Const.get? m a = none

theorem Std.DHashMap.Const.get?_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β}, Std.DHashMap.Const.get? (m.insert k v) a = if (k == a) = true then some v else Std.DHashMap.Const.get? m a

@[simp]

theorem Std.DHashMap.Const.get?_insert_self {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β}, Std.DHashMap.Const.get? (m.insert k v) k = some v

theorem Std.DHashMap.Const.contains_eq_isSome_get? {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, m.contains a = (Std.DHashMap.Const.get? m a).isSome

theorem Std.DHashMap.Const.get?_eq_none_of_contains_eq_false {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, m.contains a = false → Std.DHashMap.Const.get? m a = none

theorem Std.DHashMap.Const.get?_eq_none {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, ¬a ∈ m → Std.DHashMap.Const.get? m a = none

theorem Std.DHashMap.Const.get?_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, Std.DHashMap.Const.get? (m.erase k) a = if (k == a) = true then none else Std.DHashMap.Const.get? m a

@[simp]

theorem Std.DHashMap.Const.get?_erase_self {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, Std.DHashMap.Const.get? (m.erase k) k = none

theorem Std.DHashMap.Const.get?_eq_get? {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : LawfulBEq α] {a : α}, Std.DHashMap.Const.get? m a = m.get? a

theorem Std.DHashMap.Const.get?_congr {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a b : α}, (a == b) = true → Std.DHashMap.Const.get? m a = Std.DHashMap.Const.get? m b

theorem Std.DHashMap.get_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α} {v : β k} {h₁ : a ∈ m.insert k v}, (m.insert k v).get a h₁ = if h₂ : (k == a) = true then cast ⋯ v else m.get a ⋯

@[simp]

theorem Std.DHashMap.get_insert_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α} {v : β k}, (m.insert k v).get k ⋯ = v

@[simp]

theorem Std.DHashMap.get_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α} {h' : a ∈ m.erase k}, (m.erase k).get a h' = m.get a ⋯

theorem Std.DHashMap.get?_eq_some_get {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} {h : a ∈ m}, m.get? a = some (m.get a h)

theorem Std.DHashMap.Const.get_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v}, Std.DHashMap.Const.get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else Std.DHashMap.Const.get m a ⋯

@[simp]

theorem Std.DHashMap.Const.get_insert_self {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α} {v : β}, Std.DHashMap.Const.get (m.insert k v) k ⋯ = v

@[simp]

theorem Std.DHashMap.Const.get_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k a : α} {h' : a ∈ m.erase k}, Std.DHashMap.Const.get (m.erase k) a h' = Std.DHashMap.Const.get m a ⋯

theorem Std.DHashMap.Const.get?_eq_some_get {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α} {h : a ∈ m}, Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.get m a h)

theorem Std.DHashMap.Const.get_eq_get {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : LawfulBEq α] {a : α} {h : a ∈ m}, Std.DHashMap.Const.get m a h = m.get a h

theorem Std.DHashMap.Const.get_congr {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : LawfulBEq α] {a b : α} (hab : (a == b) = true) {h' : a ∈ m}, Std.DHashMap.Const.get m a h' = Std.DHashMap.Const.get m b ⋯

@[simp]

theorem Std.DHashMap.get!_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)] {c : Nat}, (Std.DHashMap.empty c).get! a = default

@[simp]

theorem Std.DHashMap.get!_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)], ∅.get! a = default

theorem Std.DHashMap.get!_of_isEmpty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)], m.isEmpty = true → m.get! a = default

theorem Std.DHashMap.get!_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α} [inst_1 : Inhabited (β a)] {v : β k}, (m.insert k v).get! a = if h : (k == a) = true then cast ⋯ v else m.get! a

@[simp]

theorem Std.DHashMap.get!_insert_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)] {b : β a}, (m.insert a b).get! a = b

theorem Std.DHashMap.get!_eq_default_of_contains_eq_false {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)], m.contains a = false → m.get! a = default

theorem Std.DHashMap.get!_eq_default {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)], ¬a ∈ m → m.get! a = default

theorem Std.DHashMap.get!_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α} [inst_1 : Inhabited (β a)], (m.erase k).get! a = if (k == a) = true then default else m.get! a

@[simp]

theorem Std.DHashMap.get!_erase_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α} [inst_1 : Inhabited (β k)], (m.erase k).get! k = default

theorem Std.DHashMap.get?_eq_some_get!_of_contains {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)], m.contains a = true → m.get? a = some (m.get! a)

theorem Std.DHashMap.get?_eq_some_get! {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)], a ∈ m → m.get? a = some (m.get! a)

theorem Std.DHashMap.get!_eq_get!_get? {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)], m.get! a = (m.get? a).get!

theorem Std.DHashMap.get_eq_get! {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)] {h : a ∈ m}, m.get a h = m.get! a

@[simp]

theorem Std.DHashMap.Const.get!_empty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : Inhabited β] {a : α} {c : Nat}, Std.DHashMap.Const.get! (Std.DHashMap.empty c) a = default

@[simp]

theorem Std.DHashMap.Const.get!_emptyc {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : Inhabited β] {a : α}, Std.DHashMap.Const.get! ∅ a = default

theorem Std.DHashMap.Const.get!_of_isEmpty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {a : α}, m.isEmpty = true → Std.DHashMap.Const.get! m a = default

theorem Std.DHashMap.Const.get!_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {k a : α} {v : β}, Std.DHashMap.Const.get! (m.insert k v) a = if (k == a) = true then v else Std.DHashMap.Const.get! m a

@[simp]

theorem Std.DHashMap.Const.get!_insert_self {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {k : α} {v : β}, Std.DHashMap.Const.get! (m.insert k v) k = v

theorem Std.DHashMap.Const.get!_eq_default_of_contains_eq_false {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {a : α}, m.contains a = false → Std.DHashMap.Const.get! m a = default

theorem Std.DHashMap.Const.get!_eq_default {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {a : α}, ¬a ∈ m → Std.DHashMap.Const.get! m a = default

theorem Std.DHashMap.Const.get!_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {k a : α}, Std.DHashMap.Const.get! (m.erase k) a = if (k == a) = true then default else Std.DHashMap.Const.get! m a

@[simp]

theorem Std.DHashMap.Const.get!_erase_self {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {k : α}, Std.DHashMap.Const.get! (m.erase k) k = default

theorem Std.DHashMap.Const.get?_eq_some_get!_of_contains {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {a : α}, m.contains a = true → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.get! m a)

theorem Std.DHashMap.Const.get?_eq_some_get! {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {a : α}, a ∈ m → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.get! m a)

theorem Std.DHashMap.Const.get!_eq_get!_get? {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {a : α}, Std.DHashMap.Const.get! m a = (Std.DHashMap.Const.get? m a).get!

theorem Std.DHashMap.Const.get_eq_get! {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {a : α} {h : a ∈ m}, Std.DHashMap.Const.get m a h = Std.DHashMap.Const.get! m a

theorem Std.DHashMap.Const.get!_eq_get! {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : LawfulBEq α] [inst_1 : Inhabited β] {a : α}, Std.DHashMap.Const.get! m a = m.get! a

theorem Std.DHashMap.Const.get!_congr {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {a b : α}, (a == b) = true → Std.DHashMap.Const.get! m a = Std.DHashMap.Const.get! m b

@[simp]

theorem Std.DHashMap.getD_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α} {fallback : β a} {c : Nat}, (Std.DHashMap.empty c).getD a fallback = fallback

@[simp]

theorem Std.DHashMap.getD_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {a : α} {fallback : β a}, ∅.getD a fallback = fallback

theorem Std.DHashMap.getD_of_isEmpty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} {fallback : β a}, m.isEmpty = true → m.getD a fallback = fallback

theorem Std.DHashMap.getD_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α} {fallback : β a} {v : β k}, (m.insert k v).getD a fallback = if h : (k == a) = true then cast ⋯ v else m.getD a fallback

@[simp]

theorem Std.DHashMap.getD_insert_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α} {fallback v : β k}, (m.insert k v).getD k fallback = v

theorem Std.DHashMap.getD_eq_fallback_of_contains_eq_false {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} {fallback : β a}, m.contains a = false → m.getD a fallback = fallback

theorem Std.DHashMap.getD_eq_fallback {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} {fallback : β a}, ¬a ∈ m → m.getD a fallback = fallback

theorem Std.DHashMap.getD_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α} {fallback : β a}, (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback

@[simp]

theorem Std.DHashMap.getD_erase_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α} {fallback : β k}, (m.erase k).getD k fallback = fallback

theorem Std.DHashMap.get?_eq_some_getD_of_contains {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} {fallback : β a}, m.contains a = true → m.get? a = some (m.getD a fallback)

theorem Std.DHashMap.get?_eq_some_getD {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} {fallback : β a}, a ∈ m → m.get? a = some (m.getD a fallback)

theorem Std.DHashMap.getD_eq_getD_get? {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} {fallback : β a}, m.getD a fallback = (m.get? a).getD fallback

theorem Std.DHashMap.get_eq_getD {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} {fallback : β a} {h : a ∈ m}, m.get a h = m.getD a fallback

theorem Std.DHashMap.get!_eq_getD_default {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α} [inst_1 : Inhabited (β a)], m.get! a = m.getD a default

@[simp]

theorem Std.DHashMap.Const.getD_empty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {a : α} {fallback : β} {c : Nat}, Std.DHashMap.Const.getD (Std.DHashMap.empty c) a fallback = fallback

@[simp]

theorem Std.DHashMap.Const.getD_emptyc {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {a : α} {fallback : β}, Std.DHashMap.Const.getD ∅ a fallback = fallback

theorem Std.DHashMap.Const.getD_of_isEmpty {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α} {fallback : β}, m.isEmpty = true → Std.DHashMap.Const.getD m a fallback = fallback

theorem Std.DHashMap.Const.getD_insert {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {fallback v : β}, Std.DHashMap.Const.getD (m.insert k v) a fallback = if (k == a) = true then v else Std.DHashMap.Const.getD m a fallback

@[simp]

theorem Std.DHashMap.Const.getD_insert_self {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {fallback v : β}, Std.DHashMap.Const.getD (m.insert k v) k fallback = v

theorem Std.DHashMap.Const.getD_eq_fallback_of_contains_eq_false {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α} {fallback : β}, m.contains a = false → Std.DHashMap.Const.getD m a fallback = fallback

theorem Std.DHashMap.Const.getD_eq_fallback {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α} {fallback : β}, ¬a ∈ m → Std.DHashMap.Const.getD m a fallback = fallback

theorem Std.DHashMap.Const.getD_erase {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {fallback : β}, Std.DHashMap.Const.getD (m.erase k) a fallback = if (k == a) = true then fallback else Std.DHashMap.Const.getD m a fallback

@[simp]

theorem Std.DHashMap.Const.getD_erase_self {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {fallback : β}, Std.DHashMap.Const.getD (m.erase k) k fallback = fallback

theorem Std.DHashMap.Const.get?_eq_some_getD_of_contains {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α} {fallback : β}, m.contains a = true → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.getD m a fallback)

theorem Std.DHashMap.Const.get?_eq_some_getD {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α} {fallback : β}, a ∈ m → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.getD m a fallback)

theorem Std.DHashMap.Const.getD_eq_getD_get? {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α} {fallback : β}, Std.DHashMap.Const.getD m a fallback = (Std.DHashMap.Const.get? m a).getD fallback

theorem Std.DHashMap.Const.get_eq_getD {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α} {fallback : β} {h : a ∈ m}, Std.DHashMap.Const.get m a h = Std.DHashMap.Const.getD m a fallback

theorem Std.DHashMap.Const.get!_eq_getD_default {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {a : α}, Std.DHashMap.Const.get! m a = Std.DHashMap.Const.getD m a default

theorem Std.DHashMap.Const.getD_eq_getD {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : LawfulBEq α] {a : α} {fallback : β}, Std.DHashMap.Const.getD m a fallback = m.getD a fallback

theorem Std.DHashMap.Const.getD_congr {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {a b : α} {fallback : β}, (a == b) = true → Std.DHashMap.Const.getD m a fallback = Std.DHashMap.Const.getD m b fallback

@[simp]

theorem Std.DHashMap.getKey?_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α} {c : Nat}, (Std.DHashMap.empty c).getKey? a = none

@[simp]

theorem Std.DHashMap.getKey?_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.getKey? a = none

theorem Std.DHashMap.getKey?_of_isEmpty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, m.isEmpty = true → m.getKey? a = none

theorem Std.DHashMap.getKey?_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a k : α} {v : β k}, (m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a

@[simp]

theorem Std.DHashMap.getKey?_insert_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).getKey? k = some k

theorem Std.DHashMap.contains_eq_isSome_getKey? {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, m.contains a = (m.getKey? a).isSome

theorem Std.DHashMap.getKey?_eq_none_of_contains_eq_false {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, m.contains a = false → m.getKey? a = none

theorem Std.DHashMap.getKey?_eq_none {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α}, ¬a ∈ m → m.getKey? a = none

theorem Std.DHashMap.getKey?_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α}, (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a

@[simp]

theorem Std.DHashMap.getKey?_erase_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α}, (m.erase k).getKey? k = none

theorem Std.DHashMap.getKey_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k a : α} {v : β k} {h₁ : a ∈ m.insert k v}, (m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯

@[simp]

theorem Std.DHashMap.getKey_insert_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).getKey k ⋯ = k

@[simp]

theorem Std.DHashMap.getKey_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k a : α} {h' : a ∈ m.erase k}, (m.erase k).getKey a h' = m.getKey a ⋯

theorem Std.DHashMap.getKey?_eq_some_getKey {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a : α} {h : a ∈ m}, m.getKey? a = some (m.getKey a h)

@[simp]

theorem Std.DHashMap.getKey!_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} [inst : Inhabited α] {a : α} {c : Nat}, (Std.DHashMap.empty c).getKey! a = default

@[simp]

theorem Std.DHashMap.getKey!_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} [inst : Inhabited α] {a : α}, ∅.getKey! a = default

theorem Std.DHashMap.getKey!_of_isEmpty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {a : α}, m.isEmpty = true → m.getKey! a = default

theorem Std.DHashMap.getKey!_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {k a : α} {v : β k}, (m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a

@[simp]

theorem Std.DHashMap.getKey!_insert_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {a : α} {b : β a}, (m.insert a b).getKey! a = a

theorem Std.DHashMap.getKey!_eq_default_of_contains_eq_false {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {a : α}, m.contains a = false → m.getKey! a = default

theorem Std.DHashMap.getKey!_eq_default {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {a : α}, ¬a ∈ m → m.getKey! a = default

theorem Std.DHashMap.getKey!_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {k a : α}, (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a

@[simp]

theorem Std.DHashMap.getKey!_erase_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {k : α}, (m.erase k).getKey! k = default

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

theorem Std.DHashMap.getKey?_eq_some_getKey! {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {a : α}, a ∈ m → m.getKey? a = some (m.getKey! a)

theorem Std.DHashMap.getKey!_eq_get!_getKey? {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {a : α}, m.getKey! a = (m.getKey? a).get!

theorem Std.DHashMap.getKey_eq_getKey! {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {a : α} {h : a ∈ m}, m.getKey a h = m.getKey! a

@[simp]

theorem Std.DHashMap.getKeyD_empty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {a fallback : α} {c : Nat}, (Std.DHashMap.empty c).getKeyD a fallback = fallback

@[simp]

theorem Std.DHashMap.getKeyD_emptyc {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {a fallback : α}, ∅.getKeyD a fallback = fallback

theorem Std.DHashMap.getKeyD_of_isEmpty {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a fallback : α}, m.isEmpty = true → m.getKeyD a fallback = fallback

theorem Std.DHashMap.getKeyD_insert {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a fallback : α} {v : β k}, (m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback

@[simp]

theorem Std.DHashMap.getKeyD_insert_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k fallback : α} {v : β k}, (m.insert k v).getKeyD k fallback = k

theorem Std.DHashMap.getKeyD_eq_fallback_of_contains_eq_false {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a fallback : α}, m.contains a = false → m.getKeyD a fallback = fallback

theorem Std.DHashMap.getKeyD_eq_fallback {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a fallback : α}, ¬a ∈ m → m.getKeyD a fallback = fallback

theorem Std.DHashMap.getKeyD_erase {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a fallback : α}, (m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback

@[simp]

theorem Std.DHashMap.getKeyD_erase_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k fallback : α}, (m.erase k).getKeyD k fallback = fallback

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

theorem Std.DHashMap.getKey?_eq_some_getKeyD {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a fallback : α}, a ∈ m → m.getKey? a = some (m.getKeyD a fallback)

theorem Std.DHashMap.getKeyD_eq_getD_getKey? {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a fallback : α}, m.getKeyD a fallback = (m.getKey? a).getD fallback

theorem Std.DHashMap.getKey_eq_getKeyD {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {a fallback : α} {h : a ∈ m}, m.getKey a h = m.getKeyD a fallback

theorem Std.DHashMap.getKey!_eq_getKeyD_default {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {a : α}, m.getKey! a = m.getKeyD a default

@[simp]

theorem Std.DHashMap.isEmpty_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, (m.insertIfNew k v).isEmpty = false

@[simp]

theorem Std.DHashMap.contains_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, (m.insertIfNew k v).contains a = (k == a || m.contains a)

@[simp]

theorem Std.DHashMap.mem_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m

theorem Std.DHashMap.contains_insertIfNew_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, (m.insertIfNew k v).contains k = true

theorem Std.DHashMap.mem_insertIfNew_self {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, k ∈ m.insertIfNew k v

theorem Std.DHashMap.contains_of_contains_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true

theorem Std.DHashMap.mem_of_mem_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m

theorem Std.DHashMap.contains_of_contains_insertIfNew' {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, (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 get_insertIfNew.

theorem Std.DHashMap.mem_of_mem_insertIfNew' {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, 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 get_insertIfNew.

theorem Std.DHashMap.size_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1

theorem Std.DHashMap.size_le_size_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, m.size ≤ (m.insertIfNew k v).size

theorem Std.DHashMap.size_insertIfNew_le {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k : α} {v : β k}, (m.insertIfNew k v).size ≤ m.size + 1

theorem Std.DHashMap.get?_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α} {v : β k}, (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ ¬k ∈ m then some (cast ⋯ v) else m.get? a

theorem Std.DHashMap.get_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α} {v : β k} {h₁ : a ∈ m.insertIfNew k v}, (m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.get a ⋯

theorem Std.DHashMap.get!_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α} [inst_1 : Inhabited (β a)] {v : β k}, (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.get! a

theorem Std.DHashMap.getD_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α} {fallback : β a} {v : β k}, (m.insertIfNew k v).getD a fallback = if h : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.getD a fallback

theorem Std.DHashMap.Const.get?_insertIfNew {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β}, Std.DHashMap.Const.get? (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then some v else Std.DHashMap.Const.get? m a

theorem Std.DHashMap.Const.get_insertIfNew {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v}, Std.DHashMap.Const.get (m.insertIfNew k v) a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then v else Std.DHashMap.Const.get m a ⋯

theorem Std.DHashMap.Const.get!_insertIfNew {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited β] {k a : α} {v : β}, Std.DHashMap.Const.get! (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then v else Std.DHashMap.Const.get! m a

theorem Std.DHashMap.Const.getD_insertIfNew {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {fallback v : β}, Std.DHashMap.Const.getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ ¬k ∈ m then v else Std.DHashMap.Const.getD m a fallback

theorem Std.DHashMap.getKey?_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a : α} {v : β k}, (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ ¬k ∈ m then some k else m.getKey? a

theorem Std.DHashMap.getKey_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k a : α} {v : β k} {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.DHashMap.getKey!_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] [inst : Inhabited α] {k a : α} {v : β k}, (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ ¬k ∈ m then k else m.getKey! a

theorem Std.DHashMap.getKeyD_insertIfNew {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α] [inst : LawfulHashable α] {k a fallback : α} {v : β k}, (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ ¬k ∈ m then k else m.getKeyD a fallback

@[simp]

theorem Std.DHashMap.getThenInsertIfNew?_fst {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α} {v : β k}, (m.getThenInsertIfNew? k v).fst = m.get? k

@[simp]

theorem Std.DHashMap.getThenInsertIfNew?_snd {α : Type u} {β : α → Type v} : ∀ {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α} {v : β k}, (m.getThenInsertIfNew? k v).snd = m.insertIfNew k v

@[simp]

theorem Std.DHashMap.Const.getThenInsertIfNew?_fst {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} {k : α} {v : β}, (Std.DHashMap.Const.getThenInsertIfNew? m k v).fst = Std.DHashMap.Const.get? m k

@[simp]

theorem Std.DHashMap.Const.getThenInsertIfNew?_snd {α : Type u} : ∀ {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun (x : α) => β} {k : α} {v : β}, (Std.DHashMap.Const.getThenInsertIfNew? m k v).snd = m.insertIfNew k v