Dependent hash map lemmas #

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

Internal implementation detail of the hash map

Equations

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

Instances For

source

@[simp]

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

(Std.DHashMap.Raw.empty c).isEmpty = true

source

@[simp]

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

∅.isEmpty = true

source

@[simp]

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

(m.insert k v).isEmpty = false

source

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

a ∈ m ↔ m.contains a = true

source

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

m.contains a = m.contains b

source

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

a ∈ m ↔ b ∈ m

source

@[simp]

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

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

source

@[simp]

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

¬a ∈ Std.DHashMap.Raw.empty c

source

@[simp]

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

∅.contains a = false

source

@[simp]

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

¬a ∈ ∅

source

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

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

source

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

m.isEmpty = true → ¬a ∈ m

source

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

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

source

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

m.isEmpty = false ↔ ∃ (a : α), a ∈ m

source

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

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

source

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

m.isEmpty = true ↔ ∀ (a : α), ¬a ∈ m

source

@[simp]

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

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

source

@[simp]

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

a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m

source

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

(m.insert k v).contains a = true → (k == a) = false → m.contains a = true

source

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

a ∈ m.insert k v → (k == a) = false → a ∈ m

source

@[simp]

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

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

source

@[simp]

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

k ∈ m.insert k v

source

@[simp]

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

(Std.DHashMap.Raw.empty c).size = 0

source

@[simp]

theorem Std.DHashMap.Raw.size_emptyc {α : Type u} {β : α → Type v} :

∅.size = 0

source

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

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

source

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

(m.insert k v).size = if k ∈ m then m.size else m.size + 1

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

∅.erase k = ∅

source

@[simp]

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

(m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)

source

@[simp]

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

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

source

@[simp]

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

a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m

source

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

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

source

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

a ∈ m.erase k → a ∈ m

source

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

(m.erase k).size = if k ∈ m then m.size - 1 else m.size

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

∅.get? a = none

source

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

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

source

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

(m.insert k v).get? a = if h : (k == a) = true then some (cast ⋯ v) else m.get? a

source

@[simp]

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

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

source

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

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

source

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

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

source

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

¬a ∈ m → m.get? a = none

source

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

(m.erase k).get? a = if (k == a) = true then none else m.get? a

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

Std.DHashMap.Raw.Const.get? ∅ a = none

source

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

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

source

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

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

¬a ∈ m → Std.DHashMap.Raw.Const.get? m a = none

source

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

theorem Std.DHashMap.Raw.get_insert {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) [LawfulBEq α] {k : α} {a : α} {v : β k} {h₁ : a ∈ m.insert k v} :

(m.insert k v).get a h₁ = if h₂ : (k == a) = true then cast ⋯ v else m.get a ⋯

source

@[simp]

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

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

source

@[simp]

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

(m.erase a).get k h' = m.get k ⋯

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

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

Std.DHashMap.Raw.Const.get m a h = m.get a h

source

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

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

source

@[simp]

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

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

source

@[simp]

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

∅.get! a = default

source

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

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

source

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

(m.insert k v).get! a = if h : (k == a) = true then cast ⋯ v else m.get! a

source

@[simp]

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

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

source

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

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

source

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

¬a ∈ m → m.get! a = default

source

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

(m.erase k).get! a = if (k == a) = true then default else m.get! a

source

@[simp]

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

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

source

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

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

source

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

a ∈ m → m.get? a = some (m.get! a)

source

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

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

source

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

m.get a h = m.get! a

source

@[simp]

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

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

source

@[simp]

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

Std.DHashMap.Raw.Const.get! ∅ a = default

source

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

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

source

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

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

source

@[simp]

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

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

source

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

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

source

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

¬a ∈ m → Std.DHashMap.Raw.Const.get! m a = default

source

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

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

source

@[simp]

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

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

source

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

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

source

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

a ∈ m → Std.DHashMap.Raw.Const.get? m a = some (Std.DHashMap.Raw.Const.get! m a)

source

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

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

source

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

Std.DHashMap.Raw.Const.get m a h = Std.DHashMap.Raw.Const.get! m a

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

∅.getD a fallback = fallback

source

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

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

source

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

(m.insert k v).getD a fallback = if h : (k == a) = true then cast ⋯ v else m.getD a fallback

source

@[simp]

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

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

source

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

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

source

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

¬a ∈ m → m.getD a fallback = fallback

source

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

(m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback

source

@[simp]

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

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

source

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

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

source

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

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

source

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

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

source

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

m.get a h = m.getD a fallback

source

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

m.get! a = m.getD a default

source

@[simp]

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

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

source

@[simp]

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

Std.DHashMap.Raw.Const.getD ∅ a fallback = fallback

source

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

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

source

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

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

source

@[simp]

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

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

source

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

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

source

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

¬a ∈ m → Std.DHashMap.Raw.Const.getD m a fallback = fallback

source

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

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

source

@[simp]

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

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

source

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

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

source

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

a ∈ m → Std.DHashMap.Raw.Const.get? m a = some (Std.DHashMap.Raw.Const.getD m a fallback)

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[simp]

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

(m.insertIfNew k v).isEmpty = false

source

@[simp]

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

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

source

@[simp]

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

a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m

source

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

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

source

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

k ∈ m.insertIfNew k v

source

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

(m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true

source

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

a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m

source

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

(m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true

This is a restatement of contains_insertIfNew that is written to exactly match the proof obligation in the statement of get_insertIfNew.

source

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

a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ ¬k ∈ m) → a ∈ m

This is a restatement of mem_insertIfNew that is written to exactly match the proof obligation in the statement of get_insertIfNew.

source

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

(m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1

source

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

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

source

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

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

source

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

(m.insertIfNew k v).get? a = if h : (k == a) = true ∧ ¬k ∈ m then some (cast ⋯ v) else m.get? a

source

theorem Std.DHashMap.Raw.get_insertIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) [LawfulBEq α] {k : α} {a : α} {v : β k} {h₁ : a ∈ m.insertIfNew k v} :

(m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.get a ⋯

source

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

(m.insertIfNew k v).get! a = if h : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.get! a

source

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

(m.insertIfNew k v).getD a fallback = if h : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.getD a fallback

source

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

Std.DHashMap.Raw.Const.get? (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then some v else Std.DHashMap.Raw.Const.get? m a

source

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

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

source

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

Std.DHashMap.Raw.Const.get! (m.insertIfNew k v) a = if (k == a) = true ∧ ¬k ∈ m then v else Std.DHashMap.Raw.Const.get! m a

source

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

Std.DHashMap.Raw.Const.getD (m.insertIfNew k v) a fallback = if (k == a) = true ∧ ¬k ∈ m then v else Std.DHashMap.Raw.Const.getD m a fallback

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

Documentation

Std.Data.DHashMap.RawLemmas

Dependent hash map lemmas #