Std.Data.DHashMap.Internal.RawLemmas

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

File contents: verification of operations on Raw₀

source

@[simp]

theorem Std.DHashMap.Internal.Raw₀.buckets_empty {α : Type u} {β : α → Type v} {c i : Nat} {h : i < (Std.DHashMap.Internal.Raw₀.empty c).val.buckets.size} :

(Std.DHashMap.Internal.Raw₀.empty c).val.buckets[i] = Std.DHashMap.Internal.AssocList.nil

source

@[simp]

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

(Std.DHashMap.Raw.empty c).buckets[i] = Std.DHashMap.Internal.AssocList.nil

source

@[simp]

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

∅.buckets[i] = Std.DHashMap.Internal.AssocList.nil

source

@[simp]

theorem Std.DHashMap.Internal.buckets_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c i : Nat} {h : i < (Std.DHashMap.empty c).val.buckets.size} :

(Std.DHashMap.empty c).val.buckets[i] = Std.DHashMap.Internal.AssocList.nil

source

@[simp]

theorem Std.DHashMap.Internal.buckets_emptyc {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {i : Nat} {h : i < ∅.val.buckets.size} :

∅.val.buckets[i] = Std.DHashMap.Internal.AssocList.nil

source

@[simp]

theorem Std.DHashMap.Internal.Raw₀.size_empty {α : Type u} {β : α → Type v} {c : Nat} :

(Std.DHashMap.Internal.Raw₀.empty c).val.size = 0

source

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

m.val.isEmpty = (m.val.size == 0)

source

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)

Instances For

source

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)

Instances For

source

def Std.DHashMap.Internal.Raw₀.tacticSimp_to_modelUsing_ :

Lean.ParserDescr

Internal implementation detail of the hash map

Equations

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

Instances For

source

@[simp]

theorem Std.DHashMap.Internal.Raw₀.isEmpty_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c : Nat} :

(Std.DHashMap.Internal.Raw₀.empty c).val.isEmpty = true

source

@[simp]

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

(m.insert k v).val.isEmpty = false

source

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

m.contains a = m.contains b

source

@[simp]

theorem Std.DHashMap.Internal.Raw₀.contains_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a : α} {c : Nat} :

(Std.DHashMap.Internal.Raw₀.empty c).contains a = false

source

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

m.val.isEmpty = true → m.contains a = false

source

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

m.val.isEmpty = false ↔ ∃ (a : α), m.contains a = true

source

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

m.val.isEmpty = true ↔ ∀ (a : α), m.contains a = false

source

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

(m.insert k v).contains a = (k == a || m.contains a)

source

theorem Std.DHashMap.Internal.Raw₀.contains_of_contains_insert {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.insert k v).contains k = true

source

theorem Std.DHashMap.Internal.Raw₀.size_insert {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

m.val.size ≤ (m.insert k v).val.size

source

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

(m.insert k v).val.size ≤ m.val.size + 1

source

@[simp]

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

(Std.DHashMap.Internal.Raw₀.empty c).erase k = Std.DHashMap.Internal.Raw₀.empty c

source

theorem Std.DHashMap.Internal.Raw₀.isEmpty_erase {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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)

source

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

(m.erase k).contains a = (!k == a && m.contains a)

source

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

(m.erase k).contains a = true → m.contains a = true

source

theorem Std.DHashMap.Internal.Raw₀.size_erase {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.erase k).val.size ≤ m.val.size

source

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

m.val.size ≤ (m.erase k).val.size + 1

source

@[simp]

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

(m.containsThenInsert k v).fst = m.contains k

source

@[simp]

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

(m.containsThenInsert k v).snd = m.insert k v

source

@[simp]

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

(m.containsThenInsertIfNew k v).fst = m.contains k

source

@[simp]

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

(m.containsThenInsertIfNew k v).snd = m.insertIfNew k v

source

@[simp]

theorem Std.DHashMap.Internal.Raw₀.get?_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {a : α} {c : Nat} :

(Std.DHashMap.Internal.Raw₀.empty c).get? a = none

source

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

m.val.isEmpty = true → m.get? a = none

source

theorem Std.DHashMap.Internal.Raw₀.get?_insert {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.insert k v).get? k = some v

source

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

m.contains a = (m.get? a).isSome

source

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

m.contains a = false → m.get? a = none

source

theorem Std.DHashMap.Internal.Raw₀.get?_erase {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.erase k).get? k = none

source

@[simp]

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

Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.empty c) a = none

source

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

m.val.isEmpty = true → Std.DHashMap.Internal.Raw₀.Const.get? m a = none

source

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

Std.DHashMap.Internal.Raw₀.Const.get? (m.insert k v) a = if (k == a) = true then some v else Std.DHashMap.Internal.Raw₀.Const.get? m a

source

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

Std.DHashMap.Internal.Raw₀.Const.get? (m.insert k v) k = some v

source

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

m.contains a = (Std.DHashMap.Internal.Raw₀.Const.get? m a).isSome

source

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

m.contains a = false → Std.DHashMap.Internal.Raw₀.Const.get? m a = none

source

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

Std.DHashMap.Internal.Raw₀.Const.get? (m.erase k) a = if (k == a) = true then none else Std.DHashMap.Internal.Raw₀.Const.get? m a

source

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

Std.DHashMap.Internal.Raw₀.Const.get? (m.erase k) k = none

source

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

Std.DHashMap.Internal.Raw₀.Const.get? m a = m.get? a

source

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

Std.DHashMap.Internal.Raw₀.Const.get? m a = Std.DHashMap.Internal.Raw₀.Const.get? m b

source

theorem Std.DHashMap.Internal.Raw₀.get_insert {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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 ⋯

source

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

(m.insert k v).get k ⋯ = v

source

@[simp]

theorem Std.DHashMap.Internal.Raw₀.get_erase {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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 ⋯

source

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

m.get? a = some (m.get a h✝)

source

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

Std.DHashMap.Internal.Raw₀.Const.get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else Std.DHashMap.Internal.Raw₀.Const.get m a ⋯

source

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

Std.DHashMap.Internal.Raw₀.Const.get (m.insert k v) k ⋯ = v

source

@[simp]

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

Std.DHashMap.Internal.Raw₀.Const.get (m.erase k) a h' = Std.DHashMap.Internal.Raw₀.Const.get m a ⋯

source

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

Std.DHashMap.Internal.Raw₀.Const.get? m a = some (Std.DHashMap.Internal.Raw₀.Const.get m a h✝)

source

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

Std.DHashMap.Internal.Raw₀.Const.get m a h✝ = m.get a h✝

source

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

Std.DHashMap.Internal.Raw₀.Const.get m a h' = Std.DHashMap.Internal.Raw₀.Const.get m b ⋯

source

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

(Std.DHashMap.Internal.Raw₀.empty c).get! a = default

source

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

m.val.isEmpty = true → m.get! a = default

source

theorem Std.DHashMap.Internal.Raw₀.get!_insert {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.insert a b).get! a = b

source

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

m.contains a = false → m.get! a = default

source

theorem Std.DHashMap.Internal.Raw₀.get!_erase {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.erase k).get! k = default

source

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

m.contains a = true → m.get? a = some (m.get! a)

source

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

m.get! a = (m.get? a).get!

source

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

m.get a h✝ = m.get! a

source

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

Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.empty c) a = default

source

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

m.val.isEmpty = true → Std.DHashMap.Internal.Raw₀.Const.get! m a = default

source

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

Std.DHashMap.Internal.Raw₀.Const.get! (m.insert k v) a = if (k == a) = true then v else Std.DHashMap.Internal.Raw₀.Const.get! m a

source

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

Std.DHashMap.Internal.Raw₀.Const.get! (m.insert k v) k = v

source

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

m.contains a = false → Std.DHashMap.Internal.Raw₀.Const.get! m a = default

source

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

Std.DHashMap.Internal.Raw₀.Const.get! (m.erase k) a = if (k == a) = true then default else Std.DHashMap.Internal.Raw₀.Const.get! m a

source

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

Std.DHashMap.Internal.Raw₀.Const.get! (m.erase k) k = default

source

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

m.contains a = true → Std.DHashMap.Internal.Raw₀.Const.get? m a = some (Std.DHashMap.Internal.Raw₀.Const.get! m a)

source

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

Std.DHashMap.Internal.Raw₀.Const.get! m a = (Std.DHashMap.Internal.Raw₀.Const.get? m a).get!

source

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

Std.DHashMap.Internal.Raw₀.Const.get m a h✝ = Std.DHashMap.Internal.Raw₀.Const.get! m a

source

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

Std.DHashMap.Internal.Raw₀.Const.get! m a = m.get! a

source

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

Std.DHashMap.Internal.Raw₀.Const.get! m a = Std.DHashMap.Internal.Raw₀.Const.get! m b

source

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

(Std.DHashMap.Internal.Raw₀.empty c).getD a fallback = fallback

source

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

m.val.isEmpty = true → m.getD a fallback = fallback

source

theorem Std.DHashMap.Internal.Raw₀.getD_insert {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.insert a b).getD a fallback = b

source

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

m.contains a = false → m.getD a fallback = fallback

source

theorem Std.DHashMap.Internal.Raw₀.getD_erase {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.erase k).getD k fallback = fallback

source

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

m.contains a = true → m.get? a = some (m.getD a fallback)

source

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

m.getD a fallback = (m.get? a).getD fallback

source

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

m.get a h✝ = m.getD a fallback

source

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

m.get! a = m.getD a default

source

theorem Std.DHashMap.Internal.Raw₀.Const.getD_empty {α : Type u} [BEq α] [Hashable α] {β : Type v} {a : α} {fallback : β} {c : Nat} :

Std.DHashMap.Internal.Raw₀.Const.getD (Std.DHashMap.Internal.Raw₀.empty c) a fallback = fallback

source

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

m.val.isEmpty = true → Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = fallback

source

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

Std.DHashMap.Internal.Raw₀.Const.getD (m.insert k v) a fallback = if (k == a) = true then v else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback

source

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

Std.DHashMap.Internal.Raw₀.Const.getD (m.insert k v) k fallback = v

source

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

m.contains a = false → Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = fallback

source

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

Std.DHashMap.Internal.Raw₀.Const.getD (m.erase k) a fallback = if (k == a) = true then fallback else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback

source

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

Std.DHashMap.Internal.Raw₀.Const.getD (m.erase k) k fallback = fallback

source

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

m.contains a = true → Std.DHashMap.Internal.Raw₀.Const.get? m a = some (Std.DHashMap.Internal.Raw₀.Const.getD m a fallback)

source

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

Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = (Std.DHashMap.Internal.Raw₀.Const.get? m a).getD fallback

source

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

Std.DHashMap.Internal.Raw₀.Const.get m a h✝ = Std.DHashMap.Internal.Raw₀.Const.getD m a fallback

source

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

Std.DHashMap.Internal.Raw₀.Const.get! m a = Std.DHashMap.Internal.Raw₀.Const.getD m a default

source

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

Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = m.getD a fallback

source

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

Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = Std.DHashMap.Internal.Raw₀.Const.getD m b fallback

source

@[simp]

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

(Std.DHashMap.Internal.Raw₀.empty c).getKey? a = none

source

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

m.val.isEmpty = true → m.getKey? a = none

source

theorem Std.DHashMap.Internal.Raw₀.getKey?_insert {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.insert k v).getKey? k = some k

source

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

m.contains a = (m.getKey? a).isSome

source

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

m.contains a = false → m.getKey? a = none

source

theorem Std.DHashMap.Internal.Raw₀.getKey?_erase {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.erase k).getKey? k = none

source

theorem Std.DHashMap.Internal.Raw₀.getKey_insert {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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 ⋯

source

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

(m.insert k v).getKey k ⋯ = k

source

@[simp]

theorem Std.DHashMap.Internal.Raw₀.getKey_erase {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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 ⋯

source

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

m.getKey? a = some (m.getKey a h✝)

source

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

(Std.DHashMap.Internal.Raw₀.empty c).getKey! a = default

source

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

m.val.isEmpty = true → m.getKey! a = default

source

theorem Std.DHashMap.Internal.Raw₀.getKey!_insert {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.insert a b).getKey! a = a

source

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

m.contains a = false → m.getKey! a = default

source

theorem Std.DHashMap.Internal.Raw₀.getKey!_erase {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.erase k).getKey! k = default

source

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

m.contains a = true → m.getKey? a = some (m.getKey! a)

source

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

m.getKey! a = (m.getKey? a).get!

source

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

m.getKey a h✝ = m.getKey! a

source

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

(Std.DHashMap.Internal.Raw₀.empty c).getKeyD a fallback = fallback

source

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

m.val.isEmpty = true → m.getKeyD a fallback = fallback

source

theorem Std.DHashMap.Internal.Raw₀.getKeyD_insert {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.insert a b).getKeyD a fallback = a

source

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

m.contains a = false → m.getKeyD a fallback = fallback

source

theorem Std.DHashMap.Internal.Raw₀.getKeyD_erase {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

(m.erase k).getKeyD k fallback = fallback

source

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

m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)

source

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

m.getKeyD a fallback = (m.getKey? a).getD fallback

source

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

m.getKey a h✝ = m.getKeyD a fallback

source

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

m.getKey! a = m.getKeyD a default

source

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

(m.insertIfNew k v).val.isEmpty = false

source

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

(m.insertIfNew k v).contains a = (k == a || m.contains a)

source

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

(m.insertIfNew k v).contains k = true

source

theorem Std.DHashMap.Internal.Raw₀.contains_of_contains_insertIfNew {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

theorem Std.DHashMap.Internal.Raw₀.contains_of_contains_insertIfNew' {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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.

source

theorem Std.DHashMap.Internal.Raw₀.size_insertIfNew {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

m.val.size ≤ (m.insertIfNew k v).val.size

source

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

(m.insertIfNew k v).val.size ≤ m.val.size + 1

source

theorem Std.DHashMap.Internal.Raw₀.get?_insertIfNew {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

theorem Std.DHashMap.Internal.Raw₀.get_insertIfNew {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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 ⋯

source

theorem Std.DHashMap.Internal.Raw₀.get!_insertIfNew {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

theorem Std.DHashMap.Internal.Raw₀.getD_insertIfNew {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

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

Std.DHashMap.Internal.Raw₀.Const.get? (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then some v else Std.DHashMap.Internal.Raw₀.Const.get? m a

source

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

Std.DHashMap.Internal.Raw₀.Const.get (m.insertIfNew k v) a h₁ = if h₂ : (k == a) = true ∧ m.contains k = false then v else Std.DHashMap.Internal.Raw₀.Const.get m a ⋯

source

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

Std.DHashMap.Internal.Raw₀.Const.get! (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then v else Std.DHashMap.Internal.Raw₀.Const.get! m a

source

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

Std.DHashMap.Internal.Raw₀.Const.getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ m.contains k = false then v else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback

source

theorem Std.DHashMap.Internal.Raw₀.getKey?_insertIfNew {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

theorem Std.DHashMap.Internal.Raw₀.getKey_insertIfNew {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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 ⋯

source

theorem Std.DHashMap.Internal.Raw₀.getKey!_insertIfNew {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

theorem Std.DHashMap.Internal.Raw₀.getKeyD_insertIfNew {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.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

source

@[simp]

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

(m.getThenInsertIfNew? k v).fst = m.get? k

source

@[simp]

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

(m.getThenInsertIfNew? k v).snd = m.insertIfNew k v

source

@[simp]

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

(Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m k v).fst = Std.DHashMap.Internal.Raw₀.Const.get? m k

source

@[simp]

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

(Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m k v).snd = m.insertIfNew k v

source

@[simp]

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

m.val.keys.length = m.val.size

source

@[simp]

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

m.val.keys.isEmpty = m.val.isEmpty

source

@[simp]

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

m.val.keys.contains k = m.contains k

source

@[simp]

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

k ∈ m.val.keys ↔ m.contains k = true

source

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

List.Pairwise (fun (a b : α) => (a == b) = false) m.val.keys