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 i : Nat} {h : i < (empty c).val.buckets.size} : (empty c).val.buckets[i] = AssocList.nil

@[simp]

theorem Std.DHashMap.Internal.Raw.buckets_empty {α : Type u} {β : α → Type v} {c i : Nat} {h : i < (Raw.empty c).buckets.size} : (Raw.empty c).buckets[i] = AssocList.nil

@[simp]

theorem Std.DHashMap.Internal.Raw.buckets_emptyc {α : Type u} {β : α → Type v} {i : Nat} {h : i < ∅.buckets.size} : ∅.buckets[i] = AssocList.nil

@[simp]

theorem Std.DHashMap.Internal.buckets_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c i : Nat} {h : i < (empty c).val.buckets.size} : (empty c).val.buckets[i] = 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] = AssocList.nil

@[simp]

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

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

def Std.DHashMap.Internal.Raw₀.tacticWf_trivial : Lean.ParserDescr

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.Raw₀.tacticWf_trivial = Lean.ParserDescr.node `Std.DHashMap.Internal.Raw₀.tacticWf_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "wf_trivial" false)

def Std.DHashMap.Internal.Raw₀.tacticEmpty : Lean.ParserDescr

Internal implementation detail of the hash map

Equations

• Std.DHashMap.Internal.Raw₀.tacticEmpty = Lean.ParserDescr.node `Std.DHashMap.Internal.Raw₀.tacticEmpty 1024 (Lean.ParserDescr.nonReservedSymbol "empty" false)

def Std.DHashMap.Internal.Raw₀.«tacticSimp_to_model[_]Using_» : 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.Internal.Raw₀.isEmpty_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c : Nat} : (empty c).val.isEmpty = true

@[simp]

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

theorem Std.DHashMap.Internal.Raw₀.contains_congr {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {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} : (empty c).contains a = false

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

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

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

theorem Std.DHashMap.Internal.Raw₀.contains_insert {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k a : α} {v : β k} : (m.insert k v).contains a = true → (k == a) = false → m.contains a = true

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

theorem Std.DHashMap.Internal.Raw₀.size_insert {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k : α} {v : β k} : m.val.size ≤ (m.insert k v).val.size

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

@[simp]

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

theorem Std.DHashMap.Internal.Raw₀.isEmpty_erase {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k a : α} : (m.erase k).contains a = true → m.contains a = true

theorem Std.DHashMap.Internal.Raw₀.size_erase {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k : α} : (m.erase k).val.size ≤ m.val.size

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew_snd {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] {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} : (empty c).get? a = none

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

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

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

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

theorem Std.DHashMap.Internal.Raw₀.get?_erase {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} : (m.erase k).get? k = none

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem Std.DHashMap.Internal.Raw₀.get_erase {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {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 : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k a : α} {v : β} {h₁ : (m.insert k v).contains a = true} : get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else get m a ⋯

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

@[simp]

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

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

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

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

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

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

theorem Std.DHashMap.Internal.Raw₀.get!_insert {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.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

theorem Std.DHashMap.Internal.Raw₀.get!_insert_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {a : α} [Inhabited (β a)] {b : β a} : (m.insert a b).get! a = b

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

theorem Std.DHashMap.Internal.Raw₀.get!_erase {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} [Inhabited (β k)] : (m.erase k).get! k = default

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Std.DHashMap.Internal.Raw₀.getD_insert {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.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

theorem Std.DHashMap.Internal.Raw₀.getD_insert_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {a : α} {fallback b : β a} : (m.insert a b).getD a fallback = b

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

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

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

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

theorem Std.DHashMap.Internal.Raw₀.get_eq_getD {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {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} : getD (empty c) a fallback = fallback

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

theorem Std.DHashMap.Internal.Raw₀.getKey_insert {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k a : α} {v : β k} {h₁ : (m.insert k v).contains a = true} : (m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯

theorem Std.DHashMap.Internal.Raw₀.getKey_insert_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k : α} {v : β k} : (m.insert k v).getKey k ⋯ = k

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Std.DHashMap.Internal.Raw₀.getKeyD_insert_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {a fallback : α} {b : β a} : (m.insert a b).getKeyD a fallback = a

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

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

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

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

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

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

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

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

theorem Std.DHashMap.Internal.Raw₀.contains_insertIfNew {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k : α} {v : β k} : (m.insertIfNew k v).contains k = true

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

theorem Std.DHashMap.Internal.Raw₀.contains_of_contains_insertIfNew' {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.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.Internal.Raw₀.size_insertIfNew {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {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} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k : α} {v : β k} : m.val.size ≤ (m.insertIfNew k v).val.size

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

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

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

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

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

theorem Std.DHashMap.Internal.Raw₀.getKey?_insertIfNew {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k a : α} {v : β k} : (m.insertIfNew k v).getKey? a = if (k == a) = true ∧ m.contains k = false then some k else m.getKey? a

theorem Std.DHashMap.Internal.Raw₀.getKey_insertIfNew {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k a : α} {v : β k} {h₁ : (m.insertIfNew k v).contains a = true} : (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ m.contains k = false then k else m.getKey a ⋯

theorem Std.DHashMap.Internal.Raw₀.getKey!_insertIfNew {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.val.WF) {k a : α} {v : β k} : (m.insertIfNew k v).getKey! a = if (k == a) = true ∧ m.contains k = false then k else m.getKey! a

theorem Std.DHashMap.Internal.Raw₀.getKeyD_insertIfNew {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k a fallback : α} {v : β k} : (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ m.contains k = false then k else m.getKeyD a fallback

@[simp]

theorem Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?_fst {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {k : α} {v : β k} : (m.getThenInsertIfNew? k v).fst = m.get? k

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Std.DHashMap.Internal.Raw₀.insertMany_nil {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] : (m.insertMany []).val = m

@[simp]

theorem Std.DHashMap.Internal.Raw₀.insertMany_list_singleton {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] {k : α} {v : β k} : (m.insertMany [⟨k, v⟩]).val = m.insert k v

theorem Std.DHashMap.Internal.Raw₀.insertMany_cons {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] {l : List ((a : α) × β a)} {k : α} {v : β k} : (m.insertMany (⟨k, v⟩ :: l)).val = ((m.insert k v).insertMany l).val

@[simp]

theorem Std.DHashMap.Internal.Raw₀.contains_insertMany_list {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} {k : α} : (m.insertMany l).val.contains k = (m.contains k || (List.map Sigma.fst l).contains k)

theorem Std.DHashMap.Internal.Raw₀.contains_of_contains_insertMany_list {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} {k : α} : (m.insertMany l).val.contains k = true → (List.map Sigma.fst l).contains k = false → m.contains k = true

theorem Std.DHashMap.Internal.Raw₀.get?_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {l : List ((a : α) × β a)} {k : α} (h' : (List.map Sigma.fst l).contains k = false) : (m.insertMany l).val.get? k = m.get? k

theorem Std.DHashMap.Internal.Raw₀.get?_insertMany_list_of_mem {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (m.insertMany l).val.get? k' = some (cast ⋯ v)

theorem Std.DHashMap.Internal.Raw₀.get_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {l : List ((a : α) × β a)} {k : α} (contains : (List.map Sigma.fst l).contains k = false) {h' : (m.insertMany l).val.contains k = true} : (m.insertMany l).val.get k h' = m.get k ⋯

theorem Std.DHashMap.Internal.Raw₀.get_insertMany_list_of_mem {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) {h' : (m.insertMany l).val.contains k' = true} : (m.insertMany l).val.get k' h' = cast ⋯ v

theorem Std.DHashMap.Internal.Raw₀.get!_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (h' : (List.map Sigma.fst l).contains k = false) : (m.insertMany l).val.get! k = m.get! k

theorem Std.DHashMap.Internal.Raw₀.get!_insertMany_list_of_mem {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (m.insertMany l).val.get! k' = cast ⋯ v

theorem Std.DHashMap.Internal.Raw₀.getD_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (m.insertMany l).val.getD k fallback = m.getD k fallback

theorem Std.DHashMap.Internal.Raw₀.getD_insertMany_list_of_mem {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (m.insertMany l).val.getD k' fallback = cast ⋯ v

theorem Std.DHashMap.Internal.Raw₀.getKey?_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} {k : α} (h' : (List.map Sigma.fst l).contains k = false) : (m.insertMany l).val.getKey? k = m.getKey? k

theorem Std.DHashMap.Internal.Raw₀.getKey?_insertMany_list_of_mem {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) : (m.insertMany l).val.getKey? k' = some k

theorem Std.DHashMap.Internal.Raw₀.getKey_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} {k : α} (h₁ : (List.map Sigma.fst l).contains k = false) {h' : (m.insertMany l).val.contains k = true} : (m.insertMany l).val.getKey k h' = m.getKey k ⋯

theorem Std.DHashMap.Internal.Raw₀.getKey_insertMany_list_of_mem {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) {h' : (m.insertMany l).val.contains k' = true} : (m.insertMany l).val.getKey k' h' = k

theorem Std.DHashMap.Internal.Raw₀.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.val.WF) {l : List ((a : α) × β a)} {k : α} (h' : (List.map Sigma.fst l).contains k = false) : (m.insertMany l).val.getKey! k = m.getKey! k

theorem Std.DHashMap.Internal.Raw₀.getKey!_insertMany_list_of_mem {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.val.WF) {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) : (m.insertMany l).val.getKey! k' = k

theorem Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} {k fallback : α} (h' : (List.map Sigma.fst l).contains k = false) : (m.insertMany l).val.getKeyD k fallback = m.getKeyD k fallback

theorem Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_list_of_mem {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) : (m.insertMany l).val.getKeyD k' fallback = k

theorem Std.DHashMap.Internal.Raw₀.size_insertMany_list {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) : (∀ (a : α), m.contains a = true → (List.map Sigma.fst l).contains a = false) → (m.insertMany l).val.val.size = m.val.size + l.length

theorem Std.DHashMap.Internal.Raw₀.size_le_size_insertMany_list {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} : m.val.size ≤ (m.insertMany l).val.val.size

theorem Std.DHashMap.Internal.Raw₀.size_insertMany_list_le {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} : (m.insertMany l).val.val.size ≤ m.val.size + l.length

@[simp]

theorem Std.DHashMap.Internal.Raw₀.isEmpty_insertMany_list {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List ((a : α) × β a)} : (m.insertMany l).val.val.isEmpty = (m.val.isEmpty && l.isEmpty)

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.insertMany_nil {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) : (insertMany m []).val = m

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.insertMany_list_singleton {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) {k : α} {v : β} : (insertMany m [(k, v)]).val = m.insert k v

theorem Std.DHashMap.Internal.Raw₀.Const.insertMany_cons {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) {l : List (α × β)} {k : α} {v : β} : (insertMany m ((k, v) :: l)).val = (insertMany (m.insert k v) l).val

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_list {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k : α} : (insertMany m l).val.contains k = (m.contains k || (List.map Prod.fst l).contains k)

theorem Std.DHashMap.Internal.Raw₀.Const.contains_of_contains_insertMany_list {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k : α} : (insertMany m l).val.contains k = true → (List.map Prod.fst l).contains k = false → m.contains k = true

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k : α} (h' : (List.map Prod.fst l).contains k = false) : (insertMany m l).val.getKey? k = m.getKey? k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) : (insertMany m l).val.getKey? k' = some k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k : α} (h₁ : (List.map Prod.fst l).contains k = false) {h' : (insertMany m l).val.contains k = true} : (insertMany m l).val.getKey k h' = m.getKey k ⋯

theorem Std.DHashMap.Internal.Raw₀.Const.getKey_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) {h' : (insertMany m l).val.contains k' = true} : (insertMany m l).val.getKey k' h' = k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.val.WF) {l : List (α × β)} {k : α} (h' : (List.map Prod.fst l).contains k = false) : (insertMany m l).val.getKey! k = m.getKey! k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.val.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) : (insertMany m l).val.getKey! k' = k

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k fallback : α} (h' : (List.map Prod.fst l).contains k = false) : (insertMany m l).val.getKeyD k fallback = m.getKeyD k fallback

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) : (insertMany m l).val.getKeyD k' fallback = k

theorem Std.DHashMap.Internal.Raw₀.Const.size_insertMany_list {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) : (∀ (a : α), m.contains a = true → (List.map Prod.fst l).contains a = false) → (insertMany m l).val.val.size = m.val.size + l.length

theorem Std.DHashMap.Internal.Raw₀.Const.size_le_size_insertMany_list {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} : m.val.size ≤ (insertMany m l).val.val.size

theorem Std.DHashMap.Internal.Raw₀.Const.size_insertMany_list_le {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} : (insertMany m l).val.val.size ≤ m.val.size + l.length

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertMany_list {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} : (insertMany m l).val.val.isEmpty = (m.val.isEmpty && l.isEmpty)

theorem Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k : α} (h' : (List.map Prod.fst l).contains k = false) : get? (insertMany m l).val k = get? m k

theorem Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) : get? (insertMany m l).val k' = some v

theorem Std.DHashMap.Internal.Raw₀.Const.get_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k : α} (h₁ : (List.map Prod.fst l).contains k = false) {h' : (insertMany m l).val.contains k = true} : get (insertMany m l).val k h' = get m k ⋯

theorem Std.DHashMap.Internal.Raw₀.Const.get_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) {h' : (insertMany m l).val.contains k' = true} : get (insertMany m l).val k' h' = v

theorem Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.val.WF) {l : List (α × β)} {k : α} (h' : (List.map Prod.fst l).contains k = false) : get! (insertMany m l).val k = get! m k

theorem Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.val.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) : get! (insertMany m l).val k' = v

theorem Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k : α} {fallback : β} (h' : (List.map Prod.fst l).contains k = false) : getD (insertMany m l).val k fallback = getD m k fallback

theorem Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v fallback : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) : getD (insertMany m l).val k' fallback = v

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_nil {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) : (insertManyIfNewUnit m []).val = m

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_list_singleton {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) {k : α} : (insertManyIfNewUnit m [k]).val = m.insertIfNew k ()

theorem Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_cons {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) {l : List α} {k : α} : (insertManyIfNewUnit m (k :: l)).val = (insertManyIfNewUnit (m.insertIfNew k ()) l).val

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k : α} : (insertManyIfNewUnit m l).val.contains k = (m.contains k || l.contains k)

theorem Std.DHashMap.Internal.Raw₀.Const.contains_of_contains_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k : α} (h₂ : l.contains k = false) : (insertManyIfNewUnit m l).val.contains k = true → m.contains k = true

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k : α} : m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).val.getKey? k = none

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k k' : α} (k_beq : (k == k') = true) : m.contains k = false → List.Pairwise (fun (a b : α) => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).val.getKey? k' = some k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k : α} : m.contains k = true → (insertManyIfNewUnit m l).val.getKey? k = m.getKey? k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k : α} {h' : (insertManyIfNewUnit m l).val.contains k = true} (contains : m.contains k = true) : (insertManyIfNewUnit m l).val.getKey k h' = m.getKey k contains

theorem Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k k' : α} (k_beq : (k == k') = true) {h' : (insertManyIfNewUnit m l).val.contains k' = true} : m.contains k = false → List.Pairwise (fun (a b : α) => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).val.getKey k' h' = k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_list_mem_of_contains {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k : α} (contains : m.contains k = true) {h' : (insertManyIfNewUnit m l).val.contains k = true} : (insertManyIfNewUnit m l).val.getKey k h' = m.getKey k contains

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.val.WF) {l : List α} {k : α} : m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).val.getKey! k = default

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.val.WF) {l : List α} {k k' : α} (k_beq : (k == k') = true) : m.contains k = false → List.Pairwise (fun (a b : α) => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).val.getKey! k' = k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.val.WF) {l : List α} {k : α} : m.contains k = true → (insertManyIfNewUnit m l).val.getKey! k = m.getKey! k

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k fallback : α} : m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).val.getKeyD k fallback = fallback

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) : m.contains k = false → List.Pairwise (fun (a b : α) => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).val.getKeyD k' fallback = k

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k fallback : α} : m.contains k = true → (insertManyIfNewUnit m l).val.getKeyD k fallback = m.getKeyD k fallback

theorem Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) : (∀ (a : α), m.contains a = true → l.contains a = false) → (insertManyIfNewUnit m l).val.val.size = m.val.size + l.length

theorem Std.DHashMap.Internal.Raw₀.Const.size_le_size_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} : m.val.size ≤ (insertManyIfNewUnit m l).val.val.size

theorem Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_list_le {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} : (insertManyIfNewUnit m l).val.val.size ≤ m.val.size + l.length

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} : (insertManyIfNewUnit m l).val.val.isEmpty = (m.val.isEmpty && l.isEmpty)

theorem Std.DHashMap.Internal.Raw₀.Const.get?_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {l : List α} {k : α} : get? (insertManyIfNewUnit m l).val k = if m.contains k = true ∨ l.contains k = true then some () else none

theorem Std.DHashMap.Internal.Raw₀.Const.get_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) {l : List α} {k : α} {h : (insertManyIfNewUnit m l).val.contains k = true} : get (insertManyIfNewUnit m l).val k h = ()

theorem Std.DHashMap.Internal.Raw₀.Const.get!_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) {l : List α} {k : α} : get! (insertManyIfNewUnit m l).val k = ()

theorem Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] (m : Raw₀ α fun (x : α) => Unit) {l : List α} {k : α} {fallback : Unit} : getD (insertManyIfNewUnit m l).val k fallback = ()

@[simp]

theorem Std.DHashMap.Internal.Raw₀.insertMany_empty_list_nil {α : Type u} {β : α → Type v} [BEq α] [Hashable α] : (empty.insertMany []).val = empty

@[simp]

theorem Std.DHashMap.Internal.Raw₀.insertMany_empty_list_singleton {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {k : α} {v : β k} : (empty.insertMany [⟨k, v⟩]).val = empty.insert k v

theorem Std.DHashMap.Internal.Raw₀.insertMany_empty_list_cons {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {k : α} {v : β k} {tl : List ((a : α) × β a)} : (empty.insertMany (⟨k, v⟩ :: tl)).val = ((empty.insert k v).insertMany tl).val

theorem Std.DHashMap.Internal.Raw₀.contains_insertMany_empty_list {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} : (empty.insertMany l).val.contains k = (List.map Sigma.fst l).contains k

theorem Std.DHashMap.Internal.Raw₀.get?_insertMany_empty_list_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (h : (List.map Sigma.fst l).contains k = false) : (empty.insertMany l).val.get? k = none

theorem Std.DHashMap.Internal.Raw₀.get?_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (empty.insertMany l).val.get? k' = some (cast ⋯ v)

theorem Std.DHashMap.Internal.Raw₀.get_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) {h : (empty.insertMany l).val.contains k' = true} : (empty.insertMany l).val.get k' h = cast ⋯ v

theorem Std.DHashMap.Internal.Raw₀.get!_insertMany_empty_list_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (h : (List.map Sigma.fst l).contains k = false) : (empty.insertMany l).val.get! k = default

theorem Std.DHashMap.Internal.Raw₀.get!_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (empty.insertMany l).val.get! k' = cast ⋯ v

theorem Std.DHashMap.Internal.Raw₀.getD_insertMany_empty_list_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (empty.insertMany l).val.getD k fallback = fallback

theorem Std.DHashMap.Internal.Raw₀.getD_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : ⟨k, v⟩ ∈ l) : (empty.insertMany l).val.getD k' fallback = cast ⋯ v

theorem Std.DHashMap.Internal.Raw₀.getKey?_insertMany_empty_list_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} (h : (List.map Sigma.fst l).contains k = false) : (empty.insertMany l).val.getKey? k = none

theorem Std.DHashMap.Internal.Raw₀.getKey?_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) : (empty.insertMany l).val.getKey? k' = some k

theorem Std.DHashMap.Internal.Raw₀.getKey_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) {h' : (empty.insertMany l).val.contains k' = true} : (empty.insertMany l).val.getKey k' h' = k

theorem Std.DHashMap.Internal.Raw₀.getKey!_insertMany_empty_list_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (h : (List.map Sigma.fst l).contains k = false) : (empty.insertMany l).val.getKey! k = default

theorem Std.DHashMap.Internal.Raw₀.getKey!_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) : (empty.insertMany l).val.getKey! k' = k

theorem Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_empty_list_of_contains_eq_false {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k fallback : α} (h : (List.map Sigma.fst l).contains k = false) : (empty.insertMany l).val.getKeyD k fallback = fallback

theorem Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_empty_list_of_mem {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Sigma.fst l) : (empty.insertMany l).val.getKeyD k' fallback = k

theorem Std.DHashMap.Internal.Raw₀.size_insertMany_empty_list {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) : (empty.insertMany l).val.val.size = l.length

theorem Std.DHashMap.Internal.Raw₀.size_insertMany_empty_list_le {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : (empty.insertMany l).val.val.size ≤ l.length

theorem Std.DHashMap.Internal.Raw₀.isEmpty_insertMany_empty_list {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : (empty.insertMany l).val.val.isEmpty = l.isEmpty

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.insertMany_empty_list_nil {α : Type u} [BEq α] [Hashable α] {β : Type v} : (insertMany empty []).val = empty

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.insertMany_empty_list_singleton {α : Type u} [BEq α] [Hashable α] {β : Type v} {k : α} {v : β} : (insertMany empty [(k, v)]).val = empty.insert k v

theorem Std.DHashMap.Internal.Raw₀.Const.insertMany_empty_list_cons {α : Type u} [BEq α] [Hashable α] {β : Type v} {k : α} {v : β} {tl : List (α × β)} : (insertMany empty ((k, v) :: tl)).val = (insertMany (empty.insert k v) tl).val

theorem Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_empty_list {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} : (insertMany empty l).val.contains k = (List.map Prod.fst l).contains k

theorem Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_empty_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} [LawfulBEq α] {l : List (α × β)} {k : α} (h : (List.map Prod.fst l).contains k = false) : get? (insertMany empty l).val k = none

theorem Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) : get? (insertMany empty l).val k' = some v

theorem Std.DHashMap.Internal.Raw₀.Const.get_insertMany_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) {h : (insertMany empty l).val.contains k' = true} : get (insertMany empty l).val k' h = v

theorem Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_empty_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} [LawfulBEq α] {l : List (α × β)} {k : α} [Inhabited β] (h : (List.map Prod.fst l).contains k = false) : get! (insertMany empty l).val k = default

theorem Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v : β} [Inhabited β] (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) : get! (insertMany empty l).val k' = v

theorem Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_empty_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} [LawfulBEq α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) : getD (insertMany empty l).val k fallback = fallback

theorem Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [LawfulBEq α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) {v fallback : β} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : (k, v) ∈ l) : getD (insertMany empty l).val k' fallback = v

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_empty_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (h : (List.map Prod.fst l).contains k = false) : (insertMany empty l).val.getKey? k = none

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) : (insertMany empty l).val.getKey? k' = some k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey_insertMany_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) {h' : (insertMany empty l).val.contains k' = true} : (insertMany empty l).val.getKey k' h' = k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_empty_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (h : (List.map Prod.fst l).contains k = false) : (insertMany empty l).val.getKey! k = default

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) : (insertMany empty l).val.getKey! k' = k

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_empty_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (h : (List.map Prod.fst l).contains k = false) : (insertMany empty l).val.getKeyD k fallback = fallback

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k ∈ List.map Prod.fst l) : (insertMany empty l).val.getKeyD k' fallback = k

theorem Std.DHashMap.Internal.Raw₀.Const.size_insertMany_empty_list {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) : (insertMany empty l).val.val.size = l.length

theorem Std.DHashMap.Internal.Raw₀.Const.size_insertMany_empty_list_le {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (insertMany empty l).val.val.size ≤ l.length

theorem Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertMany_empty_list {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (insertMany empty l).val.val.isEmpty = l.isEmpty

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_empty_list_nil {α : Type u} [BEq α] [Hashable α] : (insertManyIfNewUnit empty []).val = empty

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_empty_list_singleton {α : Type u} [BEq α] [Hashable α] {k : α} : (insertManyIfNewUnit empty [k]).val = empty.insertIfNew k ()

theorem Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_empty_list_cons {α : Type u} [BEq α] [Hashable α] {hd : α} {tl : List α} : (insertManyIfNewUnit empty (hd :: tl)).val = (insertManyIfNewUnit (empty.insertIfNew hd ()) tl).val

theorem Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_empty_list {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : (insertManyIfNewUnit empty l).val.contains k = l.contains k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (h' : l.contains k = false) : (insertManyIfNewUnit empty l).val.getKey? k = none

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) : (insertManyIfNewUnit empty l).val.getKey? k' = some k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) {h' : (insertManyIfNewUnit empty l).val.contains k' = true} : (insertManyIfNewUnit empty l).val.getKey k' h' = k

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (h' : l.contains k = false) : (insertManyIfNewUnit empty l).val.getKey! k = default

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) : (insertManyIfNewUnit empty l).val.getKey! k' = k

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (h' : l.contains k = false) : (insertManyIfNewUnit empty l).val.getKeyD k fallback = fallback

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) : (insertManyIfNewUnit empty l).val.getKeyD k' fallback = k

theorem Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_empty_list {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) : (insertManyIfNewUnit empty l).val.val.size = l.length

theorem Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_empty_list_le {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} : (insertManyIfNewUnit empty l).val.val.size ≤ l.length

theorem Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertManyIfNewUnit_empty_list {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} : (insertManyIfNewUnit empty l).val.val.isEmpty = l.isEmpty

theorem Std.DHashMap.Internal.Raw₀.Const.get?_insertManyIfNewUnit_empty_list {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : get? (insertManyIfNewUnit empty l).val k = if l.contains k = true then some () else none

theorem Std.DHashMap.Internal.Raw₀.Const.get_insertManyIfNewUnit_empty_list {α : Type u} [BEq α] [Hashable α] {l : List α} {k : α} {h : (insertManyIfNewUnit empty l).val.contains k = true} : get (insertManyIfNewUnit empty l).val k h = ()

theorem Std.DHashMap.Internal.Raw₀.Const.get!_insertManyIfNewUnit_empty_list {α : Type u} [BEq α] [Hashable α] {l : List α} {k : α} : get! (insertManyIfNewUnit empty l).val k = ()

theorem Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_empty_list {α : Type u} [BEq α] [Hashable α] {l : List α} {k : α} {fallback : Unit} : getD (insertManyIfNewUnit empty l).val k fallback = ()

theorem Std.DHashMap.Internal.Raw₀.isEmpty_alter_eq_isEmpty_erase {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option (β k) → Option (β k)} : (m.alter k f).val.isEmpty = ((m.erase k).val.isEmpty && (f (m.get? k)).isNone)

@[simp]

theorem Std.DHashMap.Internal.Raw₀.isEmpty_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option (β k) → Option (β k)} : (m.alter k f).val.isEmpty = ((m.val.isEmpty || m.val.size == 1 && m.contains k) && (f (m.get? k)).isNone)

theorem Std.DHashMap.Internal.Raw₀.contains_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' : α} {f : Option (β k) → Option (β k)} : (m.alter k f).contains k' = if (k == k') = true then (f (m.get? k)).isSome else m.contains k'

theorem Std.DHashMap.Internal.Raw₀.size_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option (β k) → Option (β k)} : (m.alter k f).val.size = if (m.contains k && (f (m.get? k)).isNone) = true then m.val.size - 1 else if (!m.contains k && (f (m.get? k)).isSome) = true then m.val.size + 1 else m.val.size

theorem Std.DHashMap.Internal.Raw₀.size_alter_eq_add_one {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option (β k) → Option (β k)} (h₁ : m.contains k = false) (h₂ : (f (m.get? k)).isSome = true) : (m.alter k f).val.size = m.val.size + 1

theorem Std.DHashMap.Internal.Raw₀.size_alter_eq_sub_one {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option (β k) → Option (β k)} (h₁ : m.contains k = true) (h₂ : (f (m.get? k)).isNone = true) : (m.alter k f).val.size = m.val.size - 1

theorem Std.DHashMap.Internal.Raw₀.size_alter_eq_self_of_not_mem {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option (β k) → Option (β k)} (h₁ : m.contains k = false) (h₂ : (f (m.get? k)).isNone = true) : (m.alter k f).val.size = m.val.size

theorem Std.DHashMap.Internal.Raw₀.size_alter_eq_self_of_mem {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option (β k) → Option (β k)} (h₁ : m.contains k = true) (h₂ : (f (m.get? k)).isSome = true) : (m.alter k f).val.size = m.val.size

theorem Std.DHashMap.Internal.Raw₀.size_alter_le_size {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option (β k) → Option (β k)} : (m.alter k f).val.size ≤ m.val.size + 1

theorem Std.DHashMap.Internal.Raw₀.size_le_size_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option (β k) → Option (β k)} : m.val.size - 1 ≤ (m.alter k f).val.size

theorem Std.DHashMap.Internal.Raw₀.get?_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' : α} {f : Option (β k) → Option (β k)} : (m.alter k f).get? k' = if h : (k == k') = true then cast ⋯ (f (m.get? k)) else m.get? k'

theorem Std.DHashMap.Internal.Raw₀.get_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' : α} {f : Option (β k) → Option (β k)} (hc : (m.alter k f).contains k' = true) : (m.alter k f).get k' hc = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯

theorem Std.DHashMap.Internal.Raw₀.get_alter_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option (β k) → Option (β k)} {hc : (m.alter k f).contains k = true} : (m.alter k f).get k hc = (f (m.get? k)).get ⋯

theorem Std.DHashMap.Internal.Raw₀.get!_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {k k' : α} (h : m.val.WF) [Inhabited (β k')] {f : Option (β k) → Option (β k)} : (m.alter k f).get! k' = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).get! else m.get! k'

theorem Std.DHashMap.Internal.Raw₀.getD_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {k k' : α} {fallback : β k'} (h : m.val.WF) {f : Option (β k) → Option (β k)} : (m.alter k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).getD fallback else m.getD k' fallback

theorem Std.DHashMap.Internal.Raw₀.getD_alter_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {k : α} {fallback : β k} (h : m.val.WF) {f : Option (β k) → Option (β k)} : (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback

theorem Std.DHashMap.Internal.Raw₀.getKey?_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' : α} {f : Option (β k) → Option (β k)} : (m.alter k f).getKey? k' = if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k'

theorem Std.DHashMap.Internal.Raw₀.getKey!_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] [Inhabited α] {k k' : α} (h : m.val.WF) {f : Option (β k) → Option (β k)} : (m.alter k f).getKey! k' = if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else m.getKey! k'

theorem Std.DHashMap.Internal.Raw₀.getKey_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] [Inhabited α] {k k' : α} (h : m.val.WF) {f : Option (β k) → Option (β k)} (hc : (m.alter k f).contains k' = true) : (m.alter k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

theorem Std.DHashMap.Internal.Raw₀.getKeyD_alter {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {k k' fallback : α} (h : m.val.WF) {f : Option (β k) → Option (β k)} : (m.alter k f).getKeyD k' fallback = if (k == k') = true then if (f (m.get? k)).isSome = true then k else fallback else m.getKeyD k' fallback

theorem Std.DHashMap.Internal.Raw₀.Const.isEmpty_alter_eq_isEmpty_erase {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : Option β → Option β} : (alter m k f).val.isEmpty = ((m.erase k).val.isEmpty && (f (get? m k)).isNone)

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.isEmpty_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : Option β → Option β} : (alter m k f).val.isEmpty = ((m.val.isEmpty || m.val.size == 1 && m.contains k) && (f (get? m k)).isNone)

theorem Std.DHashMap.Internal.Raw₀.Const.contains_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' : α} {f : Option β → Option β} : (alter m k f).contains k' = if (k == k') = true then (f (get? m k)).isSome else m.contains k'

theorem Std.DHashMap.Internal.Raw₀.Const.size_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : Option β → Option β} : (alter m k f).val.size = if (m.contains k && (f (get? m k)).isNone) = true then m.val.size - 1 else if (!m.contains k && (f (get? m k)).isSome) = true then m.val.size + 1 else m.val.size

theorem Std.DHashMap.Internal.Raw₀.Const.size_alter_eq_add_one {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : Option β → Option β} (h₁ : m.contains k = false) (h₂ : (f (get? m k)).isSome = true) : (alter m k f).val.size = m.val.size + 1

theorem Std.DHashMap.Internal.Raw₀.Const.size_alter_eq_sub_one {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : Option β → Option β} (h₁ : m.contains k = true) (h₂ : (f (get? m k)).isNone = true) : (alter m k f).val.size = m.val.size - 1

theorem Std.DHashMap.Internal.Raw₀.Const.size_alter_eq_self_of_not_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : Option β → Option β} (h₁ : m.contains k = false) (h₂ : (f (get? m k)).isNone = true) : (alter m k f).val.size = m.val.size

theorem Std.DHashMap.Internal.Raw₀.Const.size_alter_eq_self_of_mem {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : Option β → Option β} (h₁ : m.contains k = true) (h₂ : (f (get? m k)).isSome = true) : (alter m k f).val.size = m.val.size

theorem Std.DHashMap.Internal.Raw₀.Const.size_alter_le_size {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option β → Option β} : (alter m k f).val.size ≤ m.val.size + 1

theorem Std.DHashMap.Internal.Raw₀.Const.size_le_size_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) [LawfulBEq α] (h : m.val.WF) {k : α} {f : Option β → Option β} : m.val.size - 1 ≤ (alter m k f).val.size

theorem Std.DHashMap.Internal.Raw₀.Const.get?_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' : α} {f : Option β → Option β} : get? (alter m k f) k' = if (k == k') = true then f (get? m k) else get? m k'

theorem Std.DHashMap.Internal.Raw₀.Const.get_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' : α} {f : Option β → Option β} (hc : (alter m k f).contains k' = true) : get (alter m k f) k' hc = if heq : (k == k') = true then (f (get? m k)).get ⋯ else get m k' ⋯

theorem Std.DHashMap.Internal.Raw₀.Const.get_alter_self {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : Option β → Option β} {hc : (alter m k f).contains k = true} : get (alter m k f) k hc = (f (get? m k)).get ⋯

theorem Std.DHashMap.Internal.Raw₀.Const.get!_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) {k k' : α} (h : m.val.WF) [Inhabited β] {f : Option β → Option β} : get! (alter m k f) k' = if (k == k') = true then (f (get? m k)).get! else get! m k'

theorem Std.DHashMap.Internal.Raw₀.Const.getD_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) {k k' : α} {fallback : β} (h : m.val.WF) {f : Option β → Option β} : getD (alter m k f) k' fallback = if (k == k') = true then (f (get? m k)).getD fallback else getD m k' fallback

theorem Std.DHashMap.Internal.Raw₀.Const.getD_alter_self {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) {k : α} {fallback : β} (h : m.val.WF) {f : Option β → Option β} : getD (alter m k f) k fallback = (f (get? m k)).getD fallback

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' : α} {f : Option β → Option β} : (alter m k f).getKey? k' = if (k == k') = true then if (f (get? m k)).isSome = true then some k else none else m.getKey? k'

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) [Inhabited α] {k k' : α} (h : m.val.WF) {f : Option β → Option β} : (alter m k f).getKey! k' = if (k == k') = true then if (f (get? m k)).isSome = true then k else default else m.getKey! k'

theorem Std.DHashMap.Internal.Raw₀.Const.getKey_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) [Inhabited α] {k k' : α} (h : m.val.WF) {f : Option β → Option β} (hc : (alter m k f).contains k' = true) : (alter m k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_alter {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) {k k' fallback : α} (h : m.val.WF) {f : Option β → Option β} : (alter m k f).getKeyD k' fallback = if (k == k') = true then if (f (get? m k)).isSome = true then k else fallback else m.getKeyD k' fallback

@[simp]

theorem Std.DHashMap.Internal.Raw₀.isEmpty_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : β k → β k} : (m.modify k f).val.isEmpty = m.val.isEmpty

theorem Std.DHashMap.Internal.Raw₀.contains_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' : α} {f : β k → β k} : (m.modify k f).contains k' = m.contains k'

theorem Std.DHashMap.Internal.Raw₀.size_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : β k → β k} : (m.modify k f).val.size = m.val.size

theorem Std.DHashMap.Internal.Raw₀.get?_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' : α} {f : β k → β k} : (m.modify k f).get? k' = if h : (k == k') = true then cast ⋯ (Option.map f (m.get? k)) else m.get? k'

@[simp]

theorem Std.DHashMap.Internal.Raw₀.get?_modify_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : β k → β k} : (m.modify k f).get? k = Option.map f (m.get? k)

theorem Std.DHashMap.Internal.Raw₀.get_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' : α} {f : β k → β k} (hc : (m.modify k f).contains k' = true) : (m.modify k f).get k' hc = if heq : (k == k') = true then cast ⋯ (f (m.get k ⋯)) else m.get k' ⋯

@[simp]

theorem Std.DHashMap.Internal.Raw₀.get_modify_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : β k → β k} {hc : (m.modify k f).contains k = true} : (m.modify k f).get k hc = f (m.get k ⋯)

theorem Std.DHashMap.Internal.Raw₀.get!_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} : (m.modify k f).get! k' = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).get! else m.get! k'

@[simp]

theorem Std.DHashMap.Internal.Raw₀.get!_modify_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} [Inhabited (β k)] {f : β k → β k} : (m.modify k f).get! k = (Option.map f (m.get? k)).get!

theorem Std.DHashMap.Internal.Raw₀.getD_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' : α} {fallback : β k'} {f : β k → β k} : (m.modify k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).getD fallback else m.getD k' fallback

@[simp]

theorem Std.DHashMap.Internal.Raw₀.getD_modify_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {fallback : β k} {f : β k → β k} : (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback

theorem Std.DHashMap.Internal.Raw₀.getKey?_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' : α} {f : β k → β k} : (m.modify k f).getKey? k' = if (k == k') = true then if m.contains k = true then some k else none else m.getKey? k'

theorem Std.DHashMap.Internal.Raw₀.getKey?_modify_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k : α} {f : β k → β k} : (m.modify k f).getKey? k = if m.contains k = true then some k else none

theorem Std.DHashMap.Internal.Raw₀.getKey!_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) [Inhabited α] {k k' : α} {f : β k → β k} : (m.modify k f).getKey! k' = if (k == k') = true then if m.contains k = true then k else default else m.getKey! k'

theorem Std.DHashMap.Internal.Raw₀.getKey!_modify_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) [Inhabited α] {k : α} {f : β k → β k} : (m.modify k f).getKey! k = if m.contains k = true then k else default

theorem Std.DHashMap.Internal.Raw₀.getKey_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) [Inhabited α] {k k' : α} {f : β k → β k} (hc : (m.modify k f).contains k' = true) : (m.modify k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

@[simp]

theorem Std.DHashMap.Internal.Raw₀.getKey_modify_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) [Inhabited α] {k : α} {f : β k → β k} (hc : (m.modify k f).contains k = true) : (m.modify k f).getKey k hc = k

theorem Std.DHashMap.Internal.Raw₀.getKeyD_modify {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) {k k' fallback : α} {f : β k → β k} : (m.modify k f).getKeyD k' fallback = if (k == k') = true then if m.contains k = true then k else fallback else m.getKeyD k' fallback

theorem Std.DHashMap.Internal.Raw₀.getKeyD_modify_self {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] (h : m.val.WF) [Inhabited α] {k fallback : α} {f : β k → β k} : (m.modify k f).getKeyD k fallback = if m.contains k = true then k else fallback

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.isEmpty_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : β → β} : (modify m k f).val.isEmpty = m.val.isEmpty

theorem Std.DHashMap.Internal.Raw₀.Const.contains_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' : α} {f : β → β} : (modify m k f).contains k' = m.contains k'

theorem Std.DHashMap.Internal.Raw₀.Const.size_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : β → β} : (modify m k f).val.size = m.val.size

theorem Std.DHashMap.Internal.Raw₀.Const.get?_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' : α} {f : β → β} : get? (modify m k f) k' = if (k == k') = true then Option.map f (get? m k) else get? m k'

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.get?_modify_self {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : β → β} : get? (modify m k f) k = Option.map f (get? m k)

theorem Std.DHashMap.Internal.Raw₀.Const.get_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' : α} {f : β → β} (hc : (modify m k f).contains k' = true) : get (modify m k f) k' hc = if heq : (k == k') = true then f (get m k ⋯) else get m k' ⋯

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.get_modify_self {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : β → β} {hc : (modify m k f).contains k = true} : get (modify m k f) k hc = f (get m k ⋯)

theorem Std.DHashMap.Internal.Raw₀.Const.get!_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' : α} [hi : Inhabited β] {f : β → β} : get! (modify m k f) k' = if (k == k') = true then (Option.map f (get? m k)).get! else get! m k'

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.get!_modify_self {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} [Inhabited β] {f : β → β} : get! (modify m k f) k = (Option.map f (get? m k)).get!

theorem Std.DHashMap.Internal.Raw₀.Const.getD_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' : α} {fallback : β} {f : β → β} : getD (modify m k f) k' fallback = if (k == k') = true then (Option.map f (get? m k)).getD fallback else getD m k' fallback

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.getD_modify_self {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {fallback : β} {f : β → β} : getD (modify m k f) k fallback = (Option.map f (get? m k)).getD fallback

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' : α} {f : β → β} : (modify m k f).getKey? k' = if (k == k') = true then if m.contains k = true then some k else none else m.getKey? k'

theorem Std.DHashMap.Internal.Raw₀.Const.getKey?_modify_self {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k : α} {f : β → β} : (modify m k f).getKey? k = if m.contains k = true then some k else none

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) [Inhabited α] {k k' : α} {f : β → β} : (modify m k f).getKey! k' = if (k == k') = true then if m.contains k = true then k else default else m.getKey! k'

theorem Std.DHashMap.Internal.Raw₀.Const.getKey!_modify_self {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) [Inhabited α] {k : α} {f : β → β} : (modify m k f).getKey! k = if m.contains k = true then k else default

theorem Std.DHashMap.Internal.Raw₀.Const.getKey_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) [Inhabited α] {k k' : α} {f : β → β} (hc : (modify m k f).contains k' = true) : (modify m k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

@[simp]

theorem Std.DHashMap.Internal.Raw₀.Const.getKey_modify_self {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) [Inhabited α] {k : α} {f : β → β} (hc : (modify m k f).contains k = true) : (modify m k f).getKey k hc = k

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_modify {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) {k k' fallback : α} {f : β → β} : (modify m k f).getKeyD k' fallback = if (k == k') = true then if m.contains k = true then k else fallback else m.getKeyD k' fallback

theorem Std.DHashMap.Internal.Raw₀.Const.getKeyD_modify_self {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : m.val.WF) [Inhabited α] {k fallback : α} {f : β → β} : (modify m k f).getKeyD k fallback = if m.contains k = true then k else fallback