Documentation

Std.Data.DHashMap.Internal.RawLemmas

This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.

File contents: verification of operations on Raw₀

@[simp]
theorem Std.DHashMap.Internal.Raw₀.buckets_empty {α : Type u} {β : αType v} {c : Nat} {i : Nat} {h : i < (Std.DHashMap.Internal.Raw₀.empty c).val.buckets.size} :
(Std.DHashMap.Internal.Raw₀.empty c).val.buckets[i] = Std.DHashMap.Internal.AssocList.nil
@[simp]
theorem Std.DHashMap.Internal.Raw.buckets_empty {α : Type u} {β : αType v} {c : Nat} {i : Nat} {h : i < (Std.DHashMap.Raw.empty c).buckets.size} :
(Std.DHashMap.Raw.empty c).buckets[i] = Std.DHashMap.Internal.AssocList.nil
@[simp]
theorem Std.DHashMap.Internal.Raw.buckets_emptyc {α : Type u} {β : αType v} {i : Nat} {h : i < .buckets.size} :
.buckets[i] = Std.DHashMap.Internal.AssocList.nil
@[simp]
theorem Std.DHashMap.Internal.buckets_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] {c : Nat} {i : Nat} {h : i < (Std.DHashMap.empty c).val.buckets.size} :
(Std.DHashMap.empty c).val.buckets[i] = Std.DHashMap.Internal.AssocList.nil
@[simp]
theorem Std.DHashMap.Internal.buckets_emptyc {α : Type u} {β : αType v} [BEq α] [Hashable α] {i : Nat} {h : i < .val.buckets.size} :
.val.buckets[i] = Std.DHashMap.Internal.AssocList.nil

Internal implementation detail of the hash map

Equations
Instances For

    Internal implementation detail of the hash map

    Equations
    Instances For

      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.Internal.Raw₀.isEmpty_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] {c : Nat} :
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.isEmpty_insert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
        (m.insert k v).val.isEmpty = false
        theorem Std.DHashMap.Internal.Raw₀.contains_congr {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} {b : α} (hab : (a == b) = true) :
        m.contains a = m.contains b
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.contains_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] {a : α} {c : Nat} :
        theorem Std.DHashMap.Internal.Raw₀.contains_of_isEmpty {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
        m.val.isEmpty = truem.contains a = false
        theorem Std.DHashMap.Internal.Raw₀.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] :
        m.val.isEmpty = false ∃ (a : α), m.contains a = true
        theorem Std.DHashMap.Internal.Raw₀.isEmpty_iff_forall_contains {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] :
        m.val.isEmpty = true ∀ (a : α), m.contains a = false
        theorem Std.DHashMap.Internal.Raw₀.contains_insert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β k} :
        (m.insert k v).contains a = (k == a || m.contains a)
        theorem Std.DHashMap.Internal.Raw₀.contains_of_contains_insert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β k} :
        (m.insert k v).contains a = true(k == a) = falsem.contains a = true
        theorem Std.DHashMap.Internal.Raw₀.contains_insert_self {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
        (m.insert k v).contains k = true
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.size_empty {α : Type u} {β : αType v} {c : Nat} :
        theorem Std.DHashMap.Internal.Raw₀.isEmpty_eq_size_eq_zero {α : Type u} {β : αType v} (m : Std.DHashMap.Internal.Raw₀ α β) :
        m.val.isEmpty = (m.val.size == 0)
        theorem Std.DHashMap.Internal.Raw₀.size_insert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
        (m.insert k v).val.size = if m.contains k = true then m.val.size else m.val.size + 1
        theorem Std.DHashMap.Internal.Raw₀.size_le_size_insert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
        m.val.size (m.insert k v).val.size
        theorem Std.DHashMap.Internal.Raw₀.size_insert_le {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
        (m.insert k v).val.size m.val.size + 1
        theorem Std.DHashMap.Internal.Raw₀.isEmpty_erase {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
        (m.erase k).val.isEmpty = (m.val.isEmpty || m.val.size == 1 && m.contains k)
        theorem Std.DHashMap.Internal.Raw₀.contains_erase {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
        (m.erase k).contains a = (!k == a && m.contains a)
        theorem Std.DHashMap.Internal.Raw₀.contains_of_contains_erase {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
        (m.erase k).contains a = truem.contains a = true
        theorem Std.DHashMap.Internal.Raw₀.size_erase {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
        (m.erase k).val.size = if m.contains k = true then m.val.size - 1 else m.val.size
        theorem Std.DHashMap.Internal.Raw₀.size_erase_le {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
        (m.erase k).val.size m.val.size
        theorem Std.DHashMap.Internal.Raw₀.size_le_size_erase {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
        m.val.size (m.erase k).val.size + 1
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.containsThenInsert_fst {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) {k : α} {v : β k} :
        (m.containsThenInsert k v).fst = m.contains k
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.containsThenInsert_snd {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) {k : α} {v : β k} :
        (m.containsThenInsert k v).snd = m.insert k v
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew_fst {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) {k : α} {v : β k} :
        (m.containsThenInsertIfNew k v).fst = m.contains k
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew_snd {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) {k : α} {v : β k} :
        (m.containsThenInsertIfNew k v).snd = m.insertIfNew k v
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.get?_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] {a : α} {c : Nat} :
        theorem Std.DHashMap.Internal.Raw₀.get?_of_isEmpty {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} :
        m.val.isEmpty = truem.get? a = none
        theorem Std.DHashMap.Internal.Raw₀.get?_insert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} {k : α} {v : β k} :
        (m.insert k v).get? a = if h : (k == a) = true then some (cast v) else m.get? a
        theorem Std.DHashMap.Internal.Raw₀.get?_insert_self {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {v : β k} :
        (m.insert k v).get? k = some v
        theorem Std.DHashMap.Internal.Raw₀.contains_eq_isSome_get? {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} :
        m.contains a = (m.get? a).isSome
        theorem Std.DHashMap.Internal.Raw₀.get?_eq_none {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} :
        m.contains a = falsem.get? a = none
        theorem Std.DHashMap.Internal.Raw₀.get?_erase {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {a : α} :
        (m.erase k).get? a = if (k == a) = true then none else m.get? a
        theorem Std.DHashMap.Internal.Raw₀.get?_erase_self {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} :
        (m.erase k).get? k = none
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_of_isEmpty {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
        m.val.isEmpty = trueStd.DHashMap.Internal.Raw₀.Const.get? m a = none
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_insert {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_insert_self {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
        theorem Std.DHashMap.Internal.Raw₀.Const.contains_eq_isSome_get? {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
        m.contains a = (Std.DHashMap.Internal.Raw₀.Const.get? m a).isSome
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_eq_none {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_erase {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_erase_self {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_eq_get? {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [LawfulBEq α] {a : α} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} {b : α} (hab : (a == b) = true) :
        theorem Std.DHashMap.Internal.Raw₀.get_insert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {a : α} {v : β k} {h₁ : (m.insert k v).contains a = true} :
        (m.insert k v).get a h₁ = if h₂ : (k == a) = true then cast v else m.get a
        theorem Std.DHashMap.Internal.Raw₀.get_insert_self {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {v : β k} :
        (m.insert k v).get k = v
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.get_erase {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {a : α} {h' : (m.erase k).contains a = true} :
        (m.erase k).get a h' = m.get a
        theorem Std.DHashMap.Internal.Raw₀.get?_eq_some_get {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} {h : m.contains a = true} :
        m.get? a = some (m.get a h)
        theorem Std.DHashMap.Internal.Raw₀.Const.get_insert {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} {h₁ : (m.insert k v).contains a = true} :
        Std.DHashMap.Internal.Raw₀.Const.get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else Std.DHashMap.Internal.Raw₀.Const.get m a
        theorem Std.DHashMap.Internal.Raw₀.Const.get_insert_self {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.Const.get_erase {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {h' : (m.erase k).contains a = true} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_get {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} {h : m.contains a = true} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get_eq_get {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [LawfulBEq α] {a : α} {h : m.contains a = true} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [LawfulBEq α] {a : α} {b : α} (hab : (a == b) = true) {h' : m.contains a = true} :
        theorem Std.DHashMap.Internal.Raw₀.get!_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] {a : α} [Inhabited (β a)] {c : Nat} :
        theorem Std.DHashMap.Internal.Raw₀.get!_of_isEmpty {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} [Inhabited (β a)] :
        m.val.isEmpty = truem.get! a = default
        theorem Std.DHashMap.Internal.Raw₀.get!_insert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {a : α} [Inhabited (β a)] {v : β k} :
        (m.insert k v).get! a = if h : (k == a) = true then cast v else m.get! a
        theorem Std.DHashMap.Internal.Raw₀.get!_insert_self {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} [Inhabited (β a)] {b : β a} :
        (m.insert a b).get! a = b
        theorem Std.DHashMap.Internal.Raw₀.get!_eq_default {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} [Inhabited (β a)] :
        m.contains a = falsem.get! a = default
        theorem Std.DHashMap.Internal.Raw₀.get!_erase {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {a : α} [Inhabited (β a)] :
        (m.erase k).get! a = if (k == a) = true then default else m.get! a
        theorem Std.DHashMap.Internal.Raw₀.get!_erase_self {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} [Inhabited (β k)] :
        (m.erase k).get! k = default
        theorem Std.DHashMap.Internal.Raw₀.get?_eq_some_get! {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} [Inhabited (β a)] :
        m.contains a = truem.get? a = some (m.get! a)
        theorem Std.DHashMap.Internal.Raw₀.get!_eq_get!_get? {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} [Inhabited (β a)] :
        m.get! a = (m.get? a).get!
        theorem Std.DHashMap.Internal.Raw₀.get_eq_get! {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} [Inhabited (β a)] {h : m.contains a = true} :
        m.get a h = m.get! a
        theorem Std.DHashMap.Internal.Raw₀.Const.get!_of_isEmpty {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
        m.val.isEmpty = trueStd.DHashMap.Internal.Raw₀.Const.get! m a = default
        theorem Std.DHashMap.Internal.Raw₀.Const.get!_insert {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {a : α} {v : β} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get!_insert_self {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get!_eq_default {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
        m.contains a = falseStd.DHashMap.Internal.Raw₀.Const.get! m a = default
        theorem Std.DHashMap.Internal.Raw₀.Const.get!_erase {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {a : α} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get!_erase_self {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get_eq_get! {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {h : m.contains a = true} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get!_eq_get! {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [LawfulBEq α] [Inhabited β] {a : α} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get!_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {b : α} (hab : (a == b) = true) :
        theorem Std.DHashMap.Internal.Raw₀.getD_empty {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] {a : α} {fallback : β a} {c : Nat} :
        (Std.DHashMap.Internal.Raw₀.empty c).getD a fallback = fallback
        theorem Std.DHashMap.Internal.Raw₀.getD_of_isEmpty {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} {fallback : β a} :
        m.val.isEmpty = truem.getD a fallback = fallback
        theorem Std.DHashMap.Internal.Raw₀.getD_insert {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [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
        theorem Std.DHashMap.Internal.Raw₀.getD_insert_self {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} {fallback : β a} {b : β a} :
        (m.insert a b).getD a fallback = b
        theorem Std.DHashMap.Internal.Raw₀.getD_eq_fallback {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} {fallback : β a} :
        m.contains a = falsem.getD a fallback = fallback
        theorem Std.DHashMap.Internal.Raw₀.getD_erase {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {a : α} {fallback : β a} :
        (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
        theorem Std.DHashMap.Internal.Raw₀.getD_erase_self {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {fallback : β k} :
        (m.erase k).getD k fallback = fallback
        theorem Std.DHashMap.Internal.Raw₀.get?_eq_some_getD {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} {fallback : β a} :
        m.contains a = truem.get? a = some (m.getD a fallback)
        theorem Std.DHashMap.Internal.Raw₀.getD_eq_getD_get? {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} {fallback : β a} :
        m.getD a fallback = (m.get? a).getD fallback
        theorem Std.DHashMap.Internal.Raw₀.get_eq_getD {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} {fallback : β a} {h : m.contains a = true} :
        m.get a h = m.getD a fallback
        theorem Std.DHashMap.Internal.Raw₀.get!_eq_getD_default {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {a : α} [Inhabited (β a)] :
        m.get! a = m.getD a default
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_empty {α : Type u} [BEq α] [Hashable α] {β : Type v} {a : α} {fallback : β} {c : Nat} :
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_of_isEmpty {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
        m.val.isEmpty = trueStd.DHashMap.Internal.Raw₀.Const.getD m a fallback = fallback
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_insert {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {fallback : β} {v : β} :
        Std.DHashMap.Internal.Raw₀.Const.getD (m.insert k v) a fallback = if (k == a) = true then v else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_insert_self {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {v : β} :
        Std.DHashMap.Internal.Raw₀.Const.getD (m.insert k v) k fallback = v
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_eq_fallback {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
        m.contains a = falseStd.DHashMap.Internal.Raw₀.Const.getD m a fallback = fallback
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_erase {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {fallback : β} :
        Std.DHashMap.Internal.Raw₀.Const.getD (m.erase k) a fallback = if (k == a) = true then fallback else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_erase_self {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
        Std.DHashMap.Internal.Raw₀.Const.getD (m.erase k) k fallback = fallback
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_getD {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_eq_getD_get? {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
        theorem Std.DHashMap.Internal.Raw₀.Const.get_eq_getD {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} {h : m.contains a = true} :
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_eq_getD {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [LawfulBEq α] {a : α} {fallback : β} :
        Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = m.getD a fallback
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_congr {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {a : α} {b : α} {fallback : β} (hab : (a == b) = true) :
        theorem Std.DHashMap.Internal.Raw₀.isEmpty_insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
        (m.insertIfNew k v).val.isEmpty = false
        theorem Std.DHashMap.Internal.Raw₀.contains_insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β k} :
        (m.insertIfNew k v).contains a = (k == a || m.contains a)
        theorem Std.DHashMap.Internal.Raw₀.contains_insertIfNew_self {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
        (m.insertIfNew k v).contains k = true
        theorem Std.DHashMap.Internal.Raw₀.contains_of_contains_insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β k} :
        (m.insertIfNew k v).contains a = true(k == a) = falsem.contains a = true
        theorem Std.DHashMap.Internal.Raw₀.contains_of_contains_insertIfNew' {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [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.Internal.Raw₀.size_insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
        (m.insertIfNew k v).val.size = if m.contains k = true then m.val.size else m.val.size + 1
        theorem Std.DHashMap.Internal.Raw₀.size_le_size_insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
        m.val.size (m.insertIfNew k v).val.size
        theorem Std.DHashMap.Internal.Raw₀.size_insertIfNew_le {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
        (m.insertIfNew k v).val.size m.val.size + 1
        theorem Std.DHashMap.Internal.Raw₀.get?_insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {a : α} {v : β k} :
        (m.insertIfNew k v).get? a = if h : (k == a) = true m.contains k = false then some (cast v) else m.get? a
        theorem Std.DHashMap.Internal.Raw₀.get_insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {a : α} {v : β k} {h₁ : (m.insertIfNew k v).contains a = true} :
        (m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true m.contains k = false then cast v else m.get a
        theorem Std.DHashMap.Internal.Raw₀.get!_insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {a : α} [Inhabited (β a)] {v : β k} :
        (m.insertIfNew k v).get! a = if h : (k == a) = true m.contains k = false then cast v else m.get! a
        theorem Std.DHashMap.Internal.Raw₀.getD_insertIfNew {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (h : m.val.WF) [LawfulBEq α] {k : α} {a : α} {fallback : β a} {v : β k} :
        (m.insertIfNew k v).getD a fallback = if h : (k == a) = true m.contains k = false then cast v else m.getD a fallback
        theorem Std.DHashMap.Internal.Raw₀.Const.get?_insertIfNew {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} :
        Std.DHashMap.Internal.Raw₀.Const.get? (m.insertIfNew k v) a = if (k == a) = true m.contains k = false then some v else Std.DHashMap.Internal.Raw₀.Const.get? m a
        theorem Std.DHashMap.Internal.Raw₀.Const.get_insertIfNew {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {v : β} {h₁ : (m.insertIfNew k v).contains a = true} :
        Std.DHashMap.Internal.Raw₀.Const.get (m.insertIfNew k v) a h₁ = if h₂ : (k == a) = true m.contains k = false then v else Std.DHashMap.Internal.Raw₀.Const.get m a
        theorem Std.DHashMap.Internal.Raw₀.Const.get!_insertIfNew {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {a : α} {v : β} :
        Std.DHashMap.Internal.Raw₀.Const.get! (m.insertIfNew k v) a = if (k == a) = true m.contains k = false then v else Std.DHashMap.Internal.Raw₀.Const.get! m a
        theorem Std.DHashMap.Internal.Raw₀.Const.getD_insertIfNew {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (h : m.val.WF) [EquivBEq α] [LawfulHashable α] {k : α} {a : α} {fallback : β} {v : β} :
        Std.DHashMap.Internal.Raw₀.Const.getD (m.insertIfNew k v) a fallback = if (k == a) = true m.contains k = false then v else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?_fst {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) [LawfulBEq α] {k : α} {v : β k} :
        (m.getThenInsertIfNew? k v).fst = m.get? k
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?_snd {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) [LawfulBEq α] {k : α} {v : β k} :
        (m.getThenInsertIfNew? k v).snd = m.insertIfNew k v
        @[simp]
        theorem Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?_snd {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) {k : α} {v : β} :