Documentation

Std.Data.DHashMap.RawLemmas

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

Internal implementation detail of the hash map

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Std.DHashMap.Raw.size_empty {α : Type u} {β : αType v} {c : Nat} :
    @[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 : Std.DHashMap.Raw α β} :
    m.isEmpty = (m.size == 0)
    @[simp]
    theorem Std.DHashMap.Raw.isEmpty_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] {c : Nat} :
    @[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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} {a : α} :
    a m m.contains a = true
    theorem Std.DHashMap.Raw.contains_congr {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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} :
    @[simp]
    theorem Std.DHashMap.Raw.not_mem_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] {a : α} {c : Nat} :
    @[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 : α} :
    theorem Std.DHashMap.Raw.contains_of_isEmpty {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.isEmpty = truem.contains a = false
    theorem Std.DHashMap.Raw.not_mem_of_isEmpty {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] {p : (a : α) × β a} :
    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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {k : α} {v : β k} :
    (m.insert k v).contains a = true(k == a) = falsem.contains a = true
    theorem Std.DHashMap.Raw.mem_of_mem_insert {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {v : β k} :
    a m.insert k v(k == a) = falsea m
    @[simp]
    theorem Std.DHashMap.Raw.contains_insert_self {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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} :
    @[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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} :
    (m.erase k).contains a = truem.contains a = true
    theorem Std.DHashMap.Raw.mem_of_mem_erase {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} :
    a m.erase ka m
    theorem Std.DHashMap.Raw.size_erase {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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} :
    (Std.DHashMap.Raw.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} :
    m.isEmpty = truem.get? a = none
    theorem Std.DHashMap.Raw.get?_insert {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} :
    m.contains a = falsem.get? a = none
    theorem Std.DHashMap.Raw.get?_eq_none {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} :
    ¬a mm.get? a = none
    theorem Std.DHashMap.Raw.get?_erase {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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} :
    @[simp]
    theorem Std.DHashMap.Raw.Const.get?_emptyc {α : Type u} [BEq α] [Hashable α] {β : Type v} {a : α} :
    theorem Std.DHashMap.Raw.Const.get?_of_isEmpty {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.isEmpty = trueStd.DHashMap.Raw.Const.get? m a = none
    theorem Std.DHashMap.Raw.Const.get?_insert {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {v : β} :
    Std.DHashMap.Raw.Const.get? (m.insert k v) a = if (k == a) = true then some v else Std.DHashMap.Raw.Const.get? m a
    @[simp]
    theorem Std.DHashMap.Raw.Const.get?_insert_self {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
    theorem Std.DHashMap.Raw.Const.contains_eq_isSome_get? {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.contains a = (Std.DHashMap.Raw.Const.get? m a).isSome
    theorem Std.DHashMap.Raw.Const.get?_eq_none_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.contains a = falseStd.DHashMap.Raw.Const.get? m a = none
    theorem Std.DHashMap.Raw.Const.get?_eq_none {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    theorem Std.DHashMap.Raw.Const.get?_erase {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} :
    Std.DHashMap.Raw.Const.get? (m.erase k) a = if (k == a) = true then none else Std.DHashMap.Raw.Const.get? m a
    @[simp]
    theorem Std.DHashMap.Raw.Const.get?_erase_self {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
    Std.DHashMap.Raw.Const.get? (m.erase k) k = none
    theorem Std.DHashMap.Raw.Const.get?_eq_get? {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [LawfulBEq α] (h : m.WF) {a : α} :
    theorem Std.DHashMap.Raw.Const.get?_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {b : α} (hab : (a == b) = true) :
    theorem Std.DHashMap.Raw.get_insert {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {v : β} {h₁ : a m.insert k v} :
    Std.DHashMap.Raw.Const.get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else Std.DHashMap.Raw.Const.get m a
    @[simp]
    theorem Std.DHashMap.Raw.Const.get_insert_self {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
    Std.DHashMap.Raw.Const.get (m.insert k v) k = v
    @[simp]
    theorem Std.DHashMap.Raw.Const.get_erase {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {h' : a m.erase k} :
    theorem Std.DHashMap.Raw.Const.get?_eq_some_get {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {h : a m} :
    theorem Std.DHashMap.Raw.Const.get_eq_get {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [LawfulBEq α] (h : m.WF) {a : α} {h : a m} :
    theorem Std.DHashMap.Raw.Const.get_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [LawfulBEq α] (h : m.WF) {a : α} {b : α} (hab : (a == b) = true) {h' : a m} :
    @[simp]
    theorem Std.DHashMap.Raw.get!_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] {a : α} [Inhabited (β a)] {c : Nat} :
    (Std.DHashMap.Raw.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    m.isEmpty = truem.get! a = default
    theorem Std.DHashMap.Raw.get!_insert {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    m.contains a = falsem.get! a = default
    theorem Std.DHashMap.Raw.get!_eq_default {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    ¬a mm.get! a = default
    theorem Std.DHashMap.Raw.get!_erase {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    m.contains a = truem.get? a = some (m.get! a)
    theorem Std.DHashMap.Raw.get?_eq_some_get! {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    a mm.get? a = some (m.get! a)
    theorem Std.DHashMap.Raw.get!_eq_get!_get? {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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} :
    @[simp]
    theorem Std.DHashMap.Raw.Const.get!_emptyc {α : Type u} [BEq α] [Hashable α] {β : Type v} [Inhabited β] {a : α} :
    theorem Std.DHashMap.Raw.Const.get!_of_isEmpty {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    m.isEmpty = trueStd.DHashMap.Raw.Const.get! m a = default
    theorem Std.DHashMap.Raw.Const.get!_insert {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α} {a : α} {v : β} :
    Std.DHashMap.Raw.Const.get! (m.insert k v) a = if (k == a) = true then v else Std.DHashMap.Raw.Const.get! m a
    @[simp]
    theorem Std.DHashMap.Raw.Const.get!_insert_self {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α} {v : β} :
    Std.DHashMap.Raw.Const.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 : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    m.contains a = falseStd.DHashMap.Raw.Const.get! m a = default
    theorem Std.DHashMap.Raw.Const.get!_eq_default {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    ¬a mStd.DHashMap.Raw.Const.get! m a = default
    theorem Std.DHashMap.Raw.Const.get!_erase {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α} {a : α} :
    Std.DHashMap.Raw.Const.get! (m.erase k) a = if (k == a) = true then default else Std.DHashMap.Raw.Const.get! m a
    @[simp]
    theorem Std.DHashMap.Raw.Const.get!_erase_self {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α} :
    Std.DHashMap.Raw.Const.get! (m.erase k) k = default
    theorem Std.DHashMap.Raw.Const.get?_eq_some_get!_of_contains {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    theorem Std.DHashMap.Raw.Const.get?_eq_some_get! {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    theorem Std.DHashMap.Raw.Const.get!_eq_get!_get? {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    theorem Std.DHashMap.Raw.Const.get_eq_get! {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} {h : a m} :
    theorem Std.DHashMap.Raw.Const.get!_eq_get! {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [LawfulBEq α] [Inhabited β] (h : m.WF) {a : α} :
    theorem Std.DHashMap.Raw.Const.get!_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} {b : α} (hab : (a == b) = true) :
    @[simp]
    theorem Std.DHashMap.Raw.getD_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] {a : α} {fallback : β a} {c : Nat} :
    (Std.DHashMap.Raw.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
    m.isEmpty = truem.getD a fallback = fallback
    theorem Std.DHashMap.Raw.getD_insert {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} {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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
    m.contains a = falsem.getD a fallback = fallback
    theorem Std.DHashMap.Raw.getD_eq_fallback {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
    ¬a mm.getD a fallback = fallback
    theorem Std.DHashMap.Raw.getD_erase {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
    m.contains a = truem.get? a = some (m.getD a fallback)
    theorem Std.DHashMap.Raw.get?_eq_some_getD {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
    a mm.get? a = some (m.getD a fallback)
    theorem Std.DHashMap.Raw.getD_eq_getD_get? {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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} :
    @[simp]
    theorem Std.DHashMap.Raw.Const.getD_emptyc {α : Type u} [BEq α] [Hashable α] {β : Type v} {a : α} {fallback : β} :
    Std.DHashMap.Raw.Const.getD a fallback = fallback
    theorem Std.DHashMap.Raw.Const.getD_of_isEmpty {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
    m.isEmpty = trueStd.DHashMap.Raw.Const.getD m a fallback = fallback
    theorem Std.DHashMap.Raw.Const.getD_insert {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {fallback : β} {v : β} :
    Std.DHashMap.Raw.Const.getD (m.insert k v) a fallback = if (k == a) = true then v else Std.DHashMap.Raw.Const.getD m a fallback
    @[simp]
    theorem Std.DHashMap.Raw.Const.getD_insert_self {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {fallback : β} {v : β} :
    Std.DHashMap.Raw.Const.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 : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
    m.contains a = falseStd.DHashMap.Raw.Const.getD m a fallback = fallback
    theorem Std.DHashMap.Raw.Const.getD_eq_fallback {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
    ¬a mStd.DHashMap.Raw.Const.getD m a fallback = fallback
    theorem Std.DHashMap.Raw.Const.getD_erase {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {fallback : β} :
    Std.DHashMap.Raw.Const.getD (m.erase k) a fallback = if (k == a) = true then fallback else Std.DHashMap.Raw.Const.getD m a fallback
    @[simp]
    theorem Std.DHashMap.Raw.Const.getD_erase_self {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {fallback : β} :
    Std.DHashMap.Raw.Const.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 : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
    theorem Std.DHashMap.Raw.Const.get?_eq_some_getD {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
    theorem Std.DHashMap.Raw.Const.getD_eq_getD_get? {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
    theorem Std.DHashMap.Raw.Const.get_eq_getD {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} {h : a m} :
    theorem Std.DHashMap.Raw.Const.get!_eq_getD_default {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    theorem Std.DHashMap.Raw.Const.getD_eq_getD {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [LawfulBEq α] (h : m.WF) {a : α} {fallback : β} :
    Std.DHashMap.Raw.Const.getD m a fallback = m.getD a fallback
    theorem Std.DHashMap.Raw.Const.getD_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {b : α} {fallback : β} (hab : (a == b) = true) :
    @[simp]
    theorem Std.DHashMap.Raw.getKey?_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] {a : α} {c : Nat} :
    (Std.DHashMap.Raw.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.isEmpty = truem.getKey? a = none
    theorem Std.DHashMap.Raw.getKey?_insert {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    m.contains a = falsem.getKey? a = none
    theorem Std.DHashMap.Raw.getKey?_eq_none {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
    ¬a mm.getKey? a = none
    theorem Std.DHashMap.Raw.getKey?_erase {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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} :
    (Std.DHashMap.Raw.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
    m.isEmpty = truem.getKey! a = default
    theorem Std.DHashMap.Raw.getKey!_insert {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
    m.contains a = falsem.getKey! a = default
    theorem Std.DHashMap.Raw.getKey!_eq_default {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
    ¬a mm.getKey! a = default
    theorem Std.DHashMap.Raw.getKey!_erase {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
    m.contains a = truem.getKey? a = some (m.getKey! a)
    theorem Std.DHashMap.Raw.getKey?_eq_some_getKey! {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
    a mm.getKey? a = some (m.getKey! a)
    theorem Std.DHashMap.Raw.getKey!_eq_get!_getKey? {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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} :
    (Std.DHashMap.Raw.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} :
    m.isEmpty = truem.getKeyD a fallback = fallback
    theorem Std.DHashMap.Raw.getKeyD_insert {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} :
    m.contains a = falsem.getKeyD a fallback = fallback
    theorem Std.DHashMap.Raw.getKeyD_eq_fallback {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} :
    ¬a mm.getKeyD a fallback = fallback
    theorem Std.DHashMap.Raw.getKeyD_erase {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} :
    m.contains a = truem.getKey? a = some (m.getKeyD a fallback)
    theorem Std.DHashMap.Raw.getKey?_eq_some_getKeyD {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : α} :
    a mm.getKey? a = some (m.getKeyD a fallback)
    theorem Std.DHashMap.Raw.getKeyD_eq_getD_getKey? {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {v : β k} :
    (m.insertIfNew k v).contains a = true(k == a) = falsem.contains a = true
    theorem Std.DHashMap.Raw.mem_of_mem_insertIfNew {α : Type u} {β : αType v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {v : β k} :
    a m.insertIfNew k v(k == a) = falsea m
    theorem Std.DHashMap.Raw.contains_of_contains_insertIfNew' {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {v : β} :
    Std.DHashMap.Raw.Const.get? (m.insertIfNew k v) a = if (k == a) = true ¬k m then some v else Std.DHashMap.Raw.Const.get? m a
    theorem Std.DHashMap.Raw.Const.get_insertIfNew {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {v : β} {h₁ : a m.insertIfNew k v} :
    Std.DHashMap.Raw.Const.get (m.insertIfNew k v) a h₁ = if h₂ : (k == a) = true ¬k m then v else Std.DHashMap.Raw.Const.get m a
    theorem Std.DHashMap.Raw.Const.get!_insertIfNew {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α} {a : α} {v : β} :
    Std.DHashMap.Raw.Const.get! (m.insertIfNew k v) a = if (k == a) = true ¬k m then v else Std.DHashMap.Raw.Const.get! m a
    theorem Std.DHashMap.Raw.Const.getD_insertIfNew {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {a : α} {fallback : β} {v : β} :
    Std.DHashMap.Raw.Const.getD (m.insertIfNew k v) a fallback = if (k == a) = true ¬k m then v else Std.DHashMap.Raw.Const.getD m a fallback
    theorem Std.DHashMap.Raw.getKey?_insertIfNew {α : Type u} {β : αType v} {m : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.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 : Std.DHashMap.Raw α fun (x : α) => β} (h : m.WF) {k : α} {v : β} :
    @[simp]
    theorem Std.DHashMap.Raw.Const.getThenInsertIfNew?_snd {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun (x : α) => β} (h : m.WF) {k : α} {v : β} :
    (Std.DHashMap.Raw.Const.getThenInsertIfNew? m k v).snd = m.insertIfNew k v