Dependent hash map lemmas

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

def Std.DHashMap.Internal.Raw.tacticSimp_to_rawUsing_ : Lean.ParserDescr

Internal implementation detail of the hash map

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Std.DHashMap.Raw.size_empty {α : Type u} {β : α → Type v} {c : Nat} : (empty c).size = 0

@[simp]

theorem Std.DHashMap.Raw.size_emptyc {α : Type u} {β : α → Type v} : ∅.size = 0

theorem Std.DHashMap.Raw.isEmpty_eq_size_eq_zero {α : Type u} {β : α → Type v} {m : Raw α β} : m.isEmpty = (m.size == 0)

@[simp]

theorem Std.DHashMap.Raw.isEmpty_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c : Nat} : (empty c).isEmpty = true

@[simp]

theorem Std.DHashMap.Raw.isEmpty_emptyc {α : Type u} {β : α → Type v} [BEq α] [Hashable α] : ∅.isEmpty = true

@[simp]

theorem Std.DHashMap.Raw.isEmpty_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : (m.insert k v).isEmpty = false

theorem Std.DHashMap.Raw.mem_iff_contains {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} {a : α} : a ∈ m ↔ m.contains a = true

theorem Std.DHashMap.Raw.contains_congr {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : (a == b) = true) : m.contains a = m.contains b

theorem Std.DHashMap.Raw.mem_congr {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : (a == b) = true) : a ∈ m ↔ b ∈ m

@[simp]

theorem Std.DHashMap.Raw.contains_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a : α} {c : Nat} : (empty c).contains a = false

@[simp]

theorem Std.DHashMap.Raw.not_mem_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a : α} {c : Nat} : ¬a ∈ empty c

@[simp]

theorem Std.DHashMap.Raw.contains_emptyc {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a : α} : ∅.contains a = false

@[simp]

theorem Std.DHashMap.Raw.not_mem_emptyc {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a : α} : ¬a ∈ ∅

theorem Std.DHashMap.Raw.contains_of_isEmpty {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty = true → m.contains a = false

theorem Std.DHashMap.Raw.not_mem_of_isEmpty {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty = true → ¬a ∈ m

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

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

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

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

@[simp]

theorem Std.DHashMap.Raw.insert_eq_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] {p : (a : α) × β a} : Insert.insert p m = m.insert p.fst p.snd

@[simp]

theorem Std.DHashMap.Raw.singleton_eq_insert {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {p : (a : α) × β a} : {p} = ∅.insert p.fst p.snd

@[simp]

theorem Std.DHashMap.Raw.contains_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α} {v : β k} : (m.insert k v).contains a = (k == a || m.contains a)

@[simp]

theorem Std.DHashMap.Raw.mem_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} : a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m

theorem Std.DHashMap.Raw.contains_of_contains_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a k : α} {v : β k} : (m.insert k v).contains a = true → (k == a) = false → m.contains a = true

theorem Std.DHashMap.Raw.mem_of_mem_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} : a ∈ m.insert k v → (k == a) = false → a ∈ m

@[simp]

theorem Std.DHashMap.Raw.contains_insert_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : (m.insert k v).contains k = true

@[simp]

theorem Std.DHashMap.Raw.mem_insert_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : k ∈ m.insert k v

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

theorem Std.DHashMap.Raw.size_le_size_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : m.size ≤ (m.insert k v).size

theorem Std.DHashMap.Raw.size_insert_le {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : (m.insert k v).size ≤ m.size + 1

@[simp]

theorem Std.DHashMap.Raw.erase_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {k : α} {c : Nat} : (empty c).erase k = empty c

@[simp]

theorem Std.DHashMap.Raw.erase_emptyc {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {k : α} : ∅.erase k = ∅

@[simp]

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

@[simp]

theorem Std.DHashMap.Raw.contains_erase {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} : (m.erase k).contains a = (!k == a && m.contains a)

@[simp]

theorem Std.DHashMap.Raw.mem_erase {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} : a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m

theorem Std.DHashMap.Raw.contains_of_contains_erase {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} : (m.erase k).contains a = true → m.contains a = true

theorem Std.DHashMap.Raw.mem_of_mem_erase {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} : a ∈ m.erase k → a ∈ m

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

theorem Std.DHashMap.Raw.size_erase_le {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : (m.erase k).size ≤ m.size

theorem Std.DHashMap.Raw.size_le_size_erase {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : m.size ≤ (m.erase k).size + 1

@[simp]

theorem Std.DHashMap.Raw.containsThenInsert_fst {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] (h : m.WF) {k : α} {v : β k} : (m.containsThenInsert k v).fst = m.contains k

@[simp]

theorem Std.DHashMap.Raw.containsThenInsert_snd {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] (h : m.WF) {k : α} {v : β k} : (m.containsThenInsert k v).snd = m.insert k v

@[simp]

theorem Std.DHashMap.Raw.containsThenInsertIfNew_fst {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] (h : m.WF) {k : α} {v : β k} : (m.containsThenInsertIfNew k v).fst = m.contains k

@[simp]

theorem Std.DHashMap.Raw.containsThenInsertIfNew_snd {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] (h : m.WF) {k : α} {v : β k} : (m.containsThenInsertIfNew k v).snd = m.insertIfNew k v

@[simp]

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

@[simp]

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

theorem Std.DHashMap.Raw.get?_of_isEmpty {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} : m.isEmpty = true → m.get? a = none

theorem Std.DHashMap.Raw.get?_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {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.Raw.get?_insert_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} {v : β k} : (m.insert k v).get? k = some v

theorem Std.DHashMap.Raw.contains_eq_isSome_get? {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} : m.contains a = (m.get? a).isSome

theorem Std.DHashMap.Raw.get?_eq_none_of_contains_eq_false {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} : m.contains a = false → m.get? a = none

theorem Std.DHashMap.Raw.get?_eq_none {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} : ¬a ∈ m → m.get? a = none

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

@[simp]

theorem Std.DHashMap.Raw.get?_erase_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} : (m.erase k).get? k = none

@[simp]

theorem Std.DHashMap.Raw.Const.get?_empty {α : Type u} [BEq α] [Hashable α] {β : Type v} {a : α} {c : Nat} : get? (empty c) a = none

@[simp]

theorem Std.DHashMap.Raw.Const.get?_emptyc {α : Type u} [BEq α] [Hashable α] {β : Type v} {a : α} : get? ∅ a = none

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

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

@[simp]

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

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

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

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

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

@[simp]

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

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

theorem Std.DHashMap.Raw.Const.get?_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : (a == b) = true) : get? m a = get? m b

theorem Std.DHashMap.Raw.get_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {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.Raw.get_insert_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} {v : β k} : (m.insert k v).get k ⋯ = v

@[simp]

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

theorem Std.DHashMap.Raw.get?_eq_some_get {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {h✝ : a ∈ m} : m.get? a = some (m.get a h✝)

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

@[simp]

theorem Std.DHashMap.Raw.Const.get_insert_self {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} : get (m.insert k v) k ⋯ = v

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

theorem Std.DHashMap.Raw.get!_of_isEmpty {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] : m.isEmpty = true → m.get! a = default

theorem Std.DHashMap.Raw.get!_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k a : α} [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.Raw.get!_insert_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} [Inhabited (β k)] {v : β k} : (m.insert k v).get! k = v

theorem Std.DHashMap.Raw.get!_eq_default_of_contains_eq_false {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] : m.contains a = false → m.get! a = default

theorem Std.DHashMap.Raw.get!_eq_default {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] : ¬a ∈ m → m.get! a = default

theorem Std.DHashMap.Raw.get!_erase {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k a : α} [Inhabited (β a)] : (m.erase k).get! a = if (k == a) = true then default else m.get! a

@[simp]

theorem Std.DHashMap.Raw.get!_erase_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} [Inhabited (β k)] : (m.erase k).get! k = default

theorem Std.DHashMap.Raw.get?_eq_some_get!_of_contains {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] : m.contains a = true → m.get? a = some (m.get! a)

theorem Std.DHashMap.Raw.get?_eq_some_get! {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] : a ∈ m → m.get? a = some (m.get! a)

theorem Std.DHashMap.Raw.get!_eq_get!_get? {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] : m.get! a = (m.get? a).get!

theorem Std.DHashMap.Raw.get_eq_get! {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] {h✝ : a ∈ m} : m.get a h✝ = m.get! a

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

@[simp]

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

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

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

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

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

theorem Std.DHashMap.Raw.Const.get!_eq_get! {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [LawfulBEq α] [Inhabited β] (h : m.WF) {a : α} : get! m a = m.get! a

theorem Std.DHashMap.Raw.Const.get!_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a b : α} (hab : (a == b) = true) : get! m a = get! m b

@[simp]

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

@[simp]

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

theorem Std.DHashMap.Raw.getD_of_isEmpty {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} : m.isEmpty = true → m.getD a fallback = fallback

theorem Std.DHashMap.Raw.getD_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {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.Raw.getD_insert_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback b : β a} : (m.insert a b).getD a fallback = b

theorem Std.DHashMap.Raw.getD_eq_fallback_of_contains_eq_false {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} : m.contains a = false → m.getD a fallback = fallback

theorem Std.DHashMap.Raw.getD_eq_fallback {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} : ¬a ∈ m → m.getD a fallback = fallback

theorem Std.DHashMap.Raw.getD_erase {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {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.Raw.getD_erase_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} {fallback : β k} : (m.erase k).getD k fallback = fallback

theorem Std.DHashMap.Raw.get?_eq_some_getD_of_contains {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} : m.contains a = true → m.get? a = some (m.getD a fallback)

theorem Std.DHashMap.Raw.get?_eq_some_getD {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} : a ∈ m → m.get? a = some (m.getD a fallback)

theorem Std.DHashMap.Raw.getD_eq_getD_get? {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} : m.getD a fallback = (m.get? a).getD fallback

theorem Std.DHashMap.Raw.get_eq_getD {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} {h✝ : a ∈ m} : m.get a h✝ = m.getD a fallback

theorem Std.DHashMap.Raw.get!_eq_getD_default {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] : m.get! a = m.getD a default

@[simp]

theorem Std.DHashMap.Raw.Const.getD_empty {α : Type u} [BEq α] [Hashable α] {β : Type v} {a : α} {fallback : β} {c : Nat} : getD (empty c) a fallback = fallback

@[simp]

theorem Std.DHashMap.Raw.Const.getD_emptyc {α : Type u} [BEq α] [Hashable α] {β : Type v} {a : α} {fallback : β} : getD ∅ a fallback = fallback

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

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

@[simp]

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

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

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

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

@[simp]

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

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

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

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

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

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

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

theorem Std.DHashMap.Raw.Const.getD_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} {fallback : β} (hab : (a == b) = true) : getD m a fallback = getD m b fallback

@[simp]

theorem Std.DHashMap.Raw.getKey?_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a : α} {c : Nat} : (empty c).getKey? a = none

@[simp]

theorem Std.DHashMap.Raw.getKey?_emptyc {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a : α} : ∅.getKey? a = none

theorem Std.DHashMap.Raw.getKey?_of_isEmpty {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.isEmpty = true → m.getKey? a = none

theorem Std.DHashMap.Raw.getKey?_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {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.Raw.getKey?_insert_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : (m.insert k v).getKey? k = some k

theorem Std.DHashMap.Raw.contains_eq_isSome_getKey? {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.contains a = (m.getKey? a).isSome

theorem Std.DHashMap.Raw.getKey?_eq_none_of_contains_eq_false {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : m.contains a = false → m.getKey? a = none

theorem Std.DHashMap.Raw.getKey?_eq_none {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} : ¬a ∈ m → m.getKey? a = none

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

@[simp]

theorem Std.DHashMap.Raw.getKey?_erase_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : (m.erase k).getKey? k = none

theorem Std.DHashMap.Raw.getKey_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {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.Raw.getKey_insert_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : (m.insert k v).getKey k ⋯ = k

@[simp]

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

theorem Std.DHashMap.Raw.getKey?_eq_some_getKey {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h✝ : a ∈ m} : m.getKey? a = some (m.getKey a h✝)

@[simp]

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

@[simp]

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

theorem Std.DHashMap.Raw.getKey!_of_isEmpty {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} : m.isEmpty = true → m.getKey! a = default

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

@[simp]

theorem Std.DHashMap.Raw.getKey!_insert_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α} {v : β k} : (m.insert k v).getKey! k = k

theorem Std.DHashMap.Raw.getKey!_eq_default_of_contains_eq_false {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} : m.contains a = false → m.getKey! a = default

theorem Std.DHashMap.Raw.getKey!_eq_default {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} : ¬a ∈ m → m.getKey! a = default

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

@[simp]

theorem Std.DHashMap.Raw.getKey!_erase_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {k : α} : (m.erase k).getKey! k = default

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

theorem Std.DHashMap.Raw.getKey?_eq_some_getKey! {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} : a ∈ m → m.getKey? a = some (m.getKey! a)

theorem Std.DHashMap.Raw.getKey!_eq_get!_getKey? {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} : m.getKey! a = (m.getKey? a).get!

theorem Std.DHashMap.Raw.getKey_eq_getKey! {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} {h✝ : a ∈ m} : m.getKey a h✝ = m.getKey! a

@[simp]

theorem Std.DHashMap.Raw.getKeyD_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a fallback : α} {c : Nat} : (empty c).getKeyD a fallback = fallback

@[simp]

theorem Std.DHashMap.Raw.getKeyD_emptyc {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a fallback : α} : ∅.getKeyD a fallback = fallback

theorem Std.DHashMap.Raw.getKeyD_of_isEmpty {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} : m.isEmpty = true → m.getKeyD a fallback = fallback

theorem Std.DHashMap.Raw.getKeyD_insert {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {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.Raw.getKeyD_insert_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {b : β a} : (m.insert a b).getKeyD a fallback = a

theorem Std.DHashMap.Raw.getKeyD_eq_fallback_of_contains_eq_false {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} : m.contains a = false → m.getKeyD a fallback = fallback

theorem Std.DHashMap.Raw.getKeyD_eq_fallback {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} : ¬a ∈ m → m.getKeyD a fallback = fallback

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

@[simp]

theorem Std.DHashMap.Raw.getKeyD_erase_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k fallback : α} : (m.erase k).getKeyD k fallback = fallback

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

theorem Std.DHashMap.Raw.getKey?_eq_some_getKeyD {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} : a ∈ m → m.getKey? a = some (m.getKeyD a fallback)

theorem Std.DHashMap.Raw.getKeyD_eq_getD_getKey? {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} : m.getKeyD a fallback = (m.getKey? a).getD fallback

theorem Std.DHashMap.Raw.getKey_eq_getKeyD {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} {h✝ : a ∈ m} : m.getKey a h✝ = m.getKeyD a fallback

theorem Std.DHashMap.Raw.getKey!_eq_getKeyD_default {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} : m.getKey! a = m.getKeyD a default

@[simp]

theorem Std.DHashMap.Raw.isEmpty_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : (m.insertIfNew k v).isEmpty = false

@[simp]

theorem Std.DHashMap.Raw.contains_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} : (m.insertIfNew k v).contains a = (k == a || m.contains a)

@[simp]

theorem Std.DHashMap.Raw.mem_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} : a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m

theorem Std.DHashMap.Raw.contains_insertIfNew_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : (m.insertIfNew k v).contains k = true

theorem Std.DHashMap.Raw.mem_insertIfNew_self {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : k ∈ m.insertIfNew k v

theorem Std.DHashMap.Raw.contains_of_contains_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} : (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true

theorem Std.DHashMap.Raw.mem_of_mem_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} : a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m

theorem Std.DHashMap.Raw.contains_of_contains_insertIfNew' {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {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.Raw.mem_of_mem_insertIfNew' {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {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.Raw.size_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1

theorem Std.DHashMap.Raw.size_le_size_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : m.size ≤ (m.insertIfNew k v).size

theorem Std.DHashMap.Raw.size_insertIfNew_le {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} : (m.insertIfNew k v).size ≤ m.size + 1

theorem Std.DHashMap.Raw.get?_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {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.Raw.get_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {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.Raw.get!_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k a : α} [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.Raw.getD_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {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.Raw.Const.get?_insertIfNew {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β} : get? (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then some v else get? m a

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

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

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

theorem Std.DHashMap.Raw.getKey?_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {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.Raw.getKey_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {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.Raw.getKey!_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {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.Raw.getKeyD_insertIfNew {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {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.Raw.getThenInsertIfNew?_fst {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} {v : β k} : (m.getThenInsertIfNew? k v).fst = m.get? k

@[simp]

theorem Std.DHashMap.Raw.getThenInsertIfNew?_snd {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} {v : β k} : (m.getThenInsertIfNew? k v).snd = m.insertIfNew k v

@[simp]

theorem Std.DHashMap.Raw.Const.getThenInsertIfNew?_fst {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} (h : m.WF) {k : α} {v : β} : (getThenInsertIfNew? m k v).fst = get? m k

@[simp]

theorem Std.DHashMap.Raw.Const.getThenInsertIfNew?_snd {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Raw α fun (x : α) => β} (h : m.WF) {k : α} {v : β} : (getThenInsertIfNew? m k v).snd = m.insertIfNew k v

@[simp]

theorem Std.DHashMap.Raw.length_keys {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : m.keys.length = m.size

@[simp]

theorem Std.DHashMap.Raw.isEmpty_keys {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : m.keys.isEmpty = m.isEmpty

@[simp]

theorem Std.DHashMap.Raw.contains_keys {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : m.keys.contains k = m.contains k

@[simp]

theorem Std.DHashMap.Raw.mem_keys {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} : k ∈ m.keys ↔ k ∈ m

theorem Std.DHashMap.Raw.distinct_keys {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : List.Pairwise (fun (a b : α) => (a == b) = false) m.keys