Documentation

Std.Data.ExtHashMap.Lemmas

Extensional hash map lemmas #

This module contains lemmas about Std.ExtHashMap.

source
@[simp]
theorem Std.ExtHashMap.isEmpty_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] :
m.isEmpty = true ↔ m = ∅
source
@[simp]
theorem Std.ExtHashMap.isEmpty_eq_false_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] :
m.isEmpty = false ↔ ¬m = ∅
source
@[simp]
theorem Std.ExtHashMap.empty_eq {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} :
∅ = m ↔ m = ∅
source
@[simp]
theorem Std.ExtHashMap.emptyWithCapacity_eq {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {c : Nat} :
emptyWithCapacity c = ∅
source
@[simp]
theorem Std.ExtHashMap.not_insert_eq_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
¬m.insert k v = ∅
source
theorem Std.ExtHashMap.mem_iff_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ m.contains a = true
source
@[simp]
theorem Std.ExtHashMap.contains_iff_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = true ↔ a ∈ m
source
theorem Std.ExtHashMap.contains_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) :
m.contains a = m.contains b
source
theorem Std.ExtHashMap.mem_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) :
a ∈ m ↔ b ∈ m
source
@[simp]
theorem Std.ExtHashMap.contains_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} :
∅.contains a = false
source
@[simp]
theorem Std.ExtHashMap.not_mem_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} :
¬a ∈ ∅
source
theorem Std.ExtHashMap.eq_empty_iff_forall_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] :
m = ∅ ↔ ∀ (a : α), m.contains a = false
source
theorem Std.ExtHashMap.eq_empty_iff_forall_not_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] :
m = ∅ ↔ ∀ (a : α), ¬a ∈ m
source
@[simp]
theorem Std.ExtHashMap.insert_eq_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {p : α × β} :
Insert.insert p m = m.insert p.fst p.snd
source
@[simp]
theorem Std.ExtHashMap.singleton_eq_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {p : α × β} :
{p} = ∅.insert p.fst p.snd
source
@[simp]
theorem Std.ExtHashMap.contains_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).contains a = (k == a || m.contains a)
source
@[simp]
theorem Std.ExtHashMap.mem_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m
source
theorem Std.ExtHashMap.contains_of_contains_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).contains a = true → (k == a) = false → m.contains a = true
source
theorem Std.ExtHashMap.mem_of_mem_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a ∈ m.insert k v → (k == a) = false → a ∈ m
source
theorem Std.ExtHashMap.contains_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).contains k = true
source
theorem Std.ExtHashMap.mem_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
k ∈ m.insert k v
source
@[simp]
theorem Std.ExtHashMap.size_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] :
∅.size = 0
source
theorem Std.ExtHashMap.eq_empty_iff_size_eq_zero {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] :
m = ∅ ↔ m.size = 0
source
theorem Std.ExtHashMap.size_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).size = if k ∈ m then m.size else m.size + 1
source
theorem Std.ExtHashMap.size_le_size_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
m.size ≤ (m.insert k v).size
source
theorem Std.ExtHashMap.size_insert_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).size ≤ m.size + 1
source
@[simp]
theorem Std.ExtHashMap.erase_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} :
∅.erase a = ∅
source
@[simp]
theorem Std.ExtHashMap.erase_eq_empty_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
m.erase k = ∅ ↔ m = ∅ ∨ m.size = 1 ∧ k ∈ m
source
@[simp]
theorem Std.ExtHashMap.contains_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = (!k == a && m.contains a)
source
@[simp]
theorem Std.ExtHashMap.mem_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
source
theorem Std.ExtHashMap.contains_of_contains_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = true → m.contains a = true
source
theorem Std.ExtHashMap.mem_of_mem_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
a ∈ m.erase k → a ∈ m
source
theorem Std.ExtHashMap.size_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size = if k ∈ m then m.size - 1 else m.size
source
theorem Std.ExtHashMap.size_erase_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size ≤ m.size
source
theorem Std.ExtHashMap.size_le_size_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
m.size ≤ (m.erase k).size + 1
source
@[simp]
theorem Std.ExtHashMap.containsThenInsert_fst {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.containsThenInsert k v).fst = m.contains k
source
@[simp]
theorem Std.ExtHashMap.containsThenInsert_snd {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.containsThenInsert k v).snd = m.insert k v
source
@[simp]
theorem Std.ExtHashMap.containsThenInsertIfNew_fst {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.containsThenInsertIfNew k v).fst = m.contains k
source
@[simp]
theorem Std.ExtHashMap.containsThenInsertIfNew_snd {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.containsThenInsertIfNew k v).snd = m.insertIfNew k v
source
@[simp]
theorem Std.ExtHashMap.get_eq_getElem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h : a ∈ m} :
m.get a h = m[a]
source
@[simp]
theorem Std.ExtHashMap.get?_eq_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.get? a = m[a]?
source
@[simp]
theorem Std.ExtHashMap.get!_eq_getElem! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m.get! a = m[a]!
source
@[simp]
theorem Std.ExtHashMap.getElem?_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} :
∅[a]? = none
source
theorem Std.ExtHashMap.getElem?_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v)[a]? = if (k == a) = true then some v else m[a]?
source
@[simp]
theorem Std.ExtHashMap.getElem?_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v)[k]? = some v
source
theorem Std.ExtHashMap.contains_eq_isSome_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = m[a]?.isSome
source
@[simp]
theorem Std.ExtHashMap.isSome_getElem?_eq_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m[a]?.isSome = m.contains a
source
theorem Std.ExtHashMap.mem_iff_isSome_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ m[a]?.isSome = true
source
@[simp]
theorem Std.ExtHashMap.isSome_getElem?_iff_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m[a]?.isSome = true ↔ a ∈ m
source
theorem Std.ExtHashMap.getElem?_eq_none_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false → m[a]? = none
source
theorem Std.ExtHashMap.getElem?_eq_none {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
¬a ∈ m → m[a]? = none
source
theorem Std.ExtHashMap.getElem?_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k)[a]? = if (k == a) = true then none else m[a]?
source
@[simp]
theorem Std.ExtHashMap.getElem?_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k)[k]? = none
source
theorem Std.ExtHashMap.getElem?_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) :
m[a]? = m[b]?
source
theorem Std.ExtHashMap.getElem_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v} :
(m.insert k v)[a] = if h₂ : (k == a) = true then v else m[a]
source
@[simp]
theorem Std.ExtHashMap.getElem_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v)[k] = v
source
@[simp]
theorem Std.ExtHashMap.getElem_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {h' : a ∈ m.erase k} :
(m.erase k)[a] = m[a]
source
theorem Std.ExtHashMap.getElem?_eq_some_getElem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} (h' : a ∈ m) :
m[a]? = some m[a]
source
theorem Std.ExtHashMap.getElem_eq_get_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h : a ∈ m} :
m[a] = m[a]?.get ⋯
source
theorem Std.ExtHashMap.get_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h : m[a]?.isSome = true} :
m[a]?.get h = m[a]
source
theorem Std.ExtHashMap.getElem_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) {h' : a ∈ m} :
m[a] = m[b]
source
@[simp]
theorem Std.ExtHashMap.getElem!_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
∅[a]! = default
source
theorem Std.ExtHashMap.getElem!_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
(m.insert k v)[a]! = if (k == a) = true then v else m[a]!
source
@[simp]
theorem Std.ExtHashMap.getElem!_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
(m.insert k v)[k]! = v
source
theorem Std.ExtHashMap.getElem!_eq_default_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m.contains a = false → m[a]! = default
source
theorem Std.ExtHashMap.getElem!_eq_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
¬a ∈ m → m[a]! = default
source
theorem Std.ExtHashMap.getElem!_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
(m.erase k)[a]! = if (k == a) = true then default else m[a]!
source
@[simp]
theorem Std.ExtHashMap.getElem!_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
(m.erase k)[k]! = default
source
theorem Std.ExtHashMap.getElem?_eq_some_getElem!_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m.contains a = true → m[a]? = some m[a]!
source
theorem Std.ExtHashMap.getElem?_eq_some_getElem! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
a ∈ m → m[a]? = some m[a]!
source
theorem Std.ExtHashMap.getElem!_eq_get!_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m[a]! = m[a]?.get!
source
theorem Std.ExtHashMap.getElem_eq_getElem! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {h' : a ∈ m} :
m[a] = m[a]!
source
theorem Std.ExtHashMap.getElem!_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : α} (hab : (a == b) = true) :
m[a]! = m[b]!
source
@[simp]
theorem Std.ExtHashMap.getD_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
∅.getD a fallback = fallback
source
theorem Std.ExtHashMap.getD_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
(m.insert k v).getD a fallback = if (k == a) = true then v else m.getD a fallback
source
@[simp]
theorem Std.ExtHashMap.getD_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} :
(m.insert k v).getD k fallback = v
source
theorem Std.ExtHashMap.getD_eq_fallback_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.contains a = false → m.getD a fallback = fallback
source
theorem Std.ExtHashMap.getD_eq_fallback {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
¬a ∈ m → m.getD a fallback = fallback
source
theorem Std.ExtHashMap.getD_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
(m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
source
@[simp]
theorem Std.ExtHashMap.getD_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
(m.erase k).getD k fallback = fallback
source
theorem Std.ExtHashMap.getElem?_eq_some_getD_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.contains a = true → m[a]? = some (m.getD a fallback)
source
theorem Std.ExtHashMap.getElem?_eq_some_getD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
a ∈ m → m[a]? = some (m.getD a fallback)
source
theorem Std.ExtHashMap.getD_eq_getD_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.getD a fallback = m[a]?.getD fallback
source
theorem Std.ExtHashMap.getElem_eq_getD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} {h' : a ∈ m} :
m[a] = m.getD a fallback
source
theorem Std.ExtHashMap.getElem!_eq_getD_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m[a]! = m.getD a default
source
theorem Std.ExtHashMap.getD_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β} (hab : (a == b) = true) :
m.getD a fallback = m.getD b fallback
source
@[simp]
theorem Std.ExtHashMap.getKey?_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a : α} :
∅.getKey? a = none
source
theorem Std.ExtHashMap.getKey?_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a
source
@[simp]
theorem Std.ExtHashMap.getKey?_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).getKey? k = some k
source
theorem Std.ExtHashMap.contains_eq_isSome_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (m.getKey? a).isSome
source
@[simp]
theorem Std.ExtHashMap.isSome_getKey?_eq_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
(m.getKey? a).isSome = m.contains a
source
theorem Std.ExtHashMap.mem_iff_isSome_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
a ∈ m ↔ (m.getKey? a).isSome = true
source
@[simp]
theorem Std.ExtHashMap.isSome_getKey?_iff_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
(m.getKey? a).isSome = true ↔ a ∈ m
source
theorem Std.ExtHashMap.mem_of_getKey?_eq_some {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.getKey? k = some k') :
k' ∈ m
source
theorem Std.ExtHashMap.getKey?_eq_none_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = false → m.getKey? a = none
source
theorem Std.ExtHashMap.getKey?_eq_none {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
¬a ∈ m → m.getKey? a = none
source
theorem Std.ExtHashMap.getKey?_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a
source
@[simp]
theorem Std.ExtHashMap.getKey?_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).getKey? k = none
source
theorem Std.ExtHashMap.getKey?_beq {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
Option.all (fun (x : α) => x == k) (m.getKey? k) = true
source
theorem Std.ExtHashMap.getKey?_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} (h : (k == k') = true) :
m.getKey? k = m.getKey? k'
source
theorem Std.ExtHashMap.getKey?_eq_some_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] {k : α} (h : m.contains k = true) :
m.getKey? k = some k
source
theorem Std.ExtHashMap.getKey?_eq_some {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] {k : α} (h : k ∈ m) :
m.getKey? k = some k
source
theorem Std.ExtHashMap.getKey_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insert k v} :
(m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯
source
@[simp]
theorem Std.ExtHashMap.getKey_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insert k v).getKey k ⋯ = k
source
@[simp]
theorem Std.ExtHashMap.getKey_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {h' : a ∈ m.erase k} :
(m.erase k).getKey a h' = m.getKey a ⋯
source
theorem Std.ExtHashMap.getKey?_eq_some_getKey {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} (h : a ∈ m) :
m.getKey? a = some (m.getKey a h)
source
theorem Std.ExtHashMap.getKey_eq_get_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h : a ∈ m} :
m.getKey a h = (m.getKey? a).get ⋯
source
@[simp]
theorem Std.ExtHashMap.get_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h : (m.getKey? a).isSome = true} :
(m.getKey? a).get h = m.getKey a ⋯
source
theorem Std.ExtHashMap.getKey_beq {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} (h : k ∈ m) :
(m.getKey k h == k) = true
source
theorem Std.ExtHashMap.getKey_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : (k₁ == k₂) = true) (h₁ : k₁ ∈ m) :
m.getKey k₁ h₁ = m.getKey k₂ ⋯
source
@[simp]
theorem Std.ExtHashMap.getKey_eq {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] {k : α} (h : k ∈ m) :
m.getKey k h = k
source
@[simp]
theorem Std.ExtHashMap.getKey!_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
∅.getKey! a = default
source
theorem Std.ExtHashMap.getKey!_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
(m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a
source
@[simp]
theorem Std.ExtHashMap.getKey!_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {v : β} :
(m.insert k v).getKey! k = k
source
theorem Std.ExtHashMap.getKey!_eq_default_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.contains a = false → m.getKey! a = default
source
theorem Std.ExtHashMap.getKey!_eq_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
¬a ∈ m → m.getKey! a = default
source
theorem Std.ExtHashMap.getKey!_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} :
(m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a
source
@[simp]
theorem Std.ExtHashMap.getKey!_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} :
(m.erase k).getKey! k = default
source
theorem Std.ExtHashMap.getKey?_eq_some_getKey!_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.contains a = true → m.getKey? a = some (m.getKey! a)
source
theorem Std.ExtHashMap.getKey?_eq_some_getKey! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
a ∈ m → m.getKey? a = some (m.getKey! a)
source
theorem Std.ExtHashMap.getKey!_eq_get!_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.getKey! a = (m.getKey? a).get!
source
theorem Std.ExtHashMap.getKey_eq_getKey! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h' : a ∈ m} :
m.getKey a h' = m.getKey! a
source
theorem Std.ExtHashMap.getKey!_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} (h : (k == k') = true) :
m.getKey! k = m.getKey! k'
source
theorem Std.ExtHashMap.getKey!_eq_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [Inhabited α] {k : α} (h : m.contains k = true) :
m.getKey! k = k
source
theorem Std.ExtHashMap.getKey!_eq_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) :
m.getKey! k = k
source
@[simp]
theorem Std.ExtHashMap.getKeyD_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
∅.getKeyD a fallback = fallback
source
theorem Std.ExtHashMap.getKeyD_insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
(m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback
source
@[simp]
theorem Std.ExtHashMap.getKeyD_insert_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k fallback : α} {v : β} :
(m.insert k v).getKeyD k fallback = k
source
theorem Std.ExtHashMap.getKeyD_eq_fallback_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.contains a = false → m.getKeyD a fallback = fallback
source
theorem Std.ExtHashMap.getKeyD_eq_fallback {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
¬a ∈ m → m.getKeyD a fallback = fallback
source
theorem Std.ExtHashMap.getKeyD_erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
(m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback
source
@[simp]
theorem Std.ExtHashMap.getKeyD_erase_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k fallback : α} :
(m.erase k).getKeyD k fallback = fallback
source
theorem Std.ExtHashMap.getKey?_eq_some_getKeyD_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)
source
theorem Std.ExtHashMap.getKey?_eq_some_getKeyD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
a ∈ m → m.getKey? a = some (m.getKeyD a fallback)
source
theorem Std.ExtHashMap.getKeyD_eq_getD_getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.getKeyD a fallback = (m.getKey? a).getD fallback
source
theorem Std.ExtHashMap.getKey_eq_getKeyD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} {h' : a ∈ m} :
m.getKey a h' = m.getKeyD a fallback
source
theorem Std.ExtHashMap.getKey!_eq_getKeyD_default {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.getKey! a = m.getKeyD a default
source
theorem Std.ExtHashMap.getKeyD_congr {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} (h : (k == k') = true) :
m.getKeyD k fallback = m.getKeyD k' fallback
source
theorem Std.ExtHashMap.getKeyD_eq_of_contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] {k fallback : α} (h : m.contains k = true) :
m.getKeyD k fallback = k
source
theorem Std.ExtHashMap.getKeyD_eq_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] {k fallback : α} (h : k ∈ m) :
m.getKeyD k fallback = k
source
@[simp]
theorem Std.ExtHashMap.not_insertIfNew_eq_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
¬m.insertIfNew k v = ∅
source
@[simp]
theorem Std.ExtHashMap.contains_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a = (k == a || m.contains a)
source
@[simp]
theorem Std.ExtHashMap.mem_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m
source
theorem Std.ExtHashMap.contains_insertIfNew_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).contains k = true
source
theorem Std.ExtHashMap.mem_insertIfNew_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
k ∈ m.insertIfNew k v
source
theorem Std.ExtHashMap.contains_of_contains_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true
source
theorem Std.ExtHashMap.mem_of_mem_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m
source
theorem Std.ExtHashMap.contains_of_contains_insertIfNew' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true

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

source
theorem Std.ExtHashMap.mem_of_mem_insertIfNew' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ ¬k ∈ m) → a ∈ m

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

source
theorem Std.ExtHashMap.size_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1
source
theorem Std.ExtHashMap.size_le_size_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
m.size ≤ (m.insertIfNew k v).size
source
theorem Std.ExtHashMap.size_insertIfNew_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.insertIfNew k v).size ≤ m.size + 1
source
theorem Std.ExtHashMap.getElem?_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v)[a]? = if (k == a) = true ∧ ¬k ∈ m then some v else m[a]?
source
theorem Std.ExtHashMap.getElem_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v} :
(m.insertIfNew k v)[a] = if h₂ : (k == a) = true ∧ ¬k ∈ m then v else m[a]
source
theorem Std.ExtHashMap.getElem!_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
(m.insertIfNew k v)[a]! = if (k == a) = true ∧ ¬k ∈ m then v else m[a]!
source
theorem Std.ExtHashMap.getD_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
(m.insertIfNew k v).getD a fallback = if (k == a) = true ∧ ¬k ∈ m then v else m.getD a fallback
source
theorem Std.ExtHashMap.getKey?_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
(m.insertIfNew k v).getKey? a = if (k == a) = true ∧ ¬k ∈ m then some k else m.getKey? a
source
theorem Std.ExtHashMap.getKey_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v} :
(m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then k else m.getKey a ⋯
source
theorem Std.ExtHashMap.getKey!_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
(m.insertIfNew k v).getKey! a = if (k == a) = true ∧ ¬k ∈ m then k else m.getKey! a
source
theorem Std.ExtHashMap.getKeyD_insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
(m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ ¬k ∈ m then k else m.getKeyD a fallback
source
@[simp]
theorem Std.ExtHashMap.getThenInsertIfNew?_fst {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.getThenInsertIfNew? k v).fst = m.get? k
source
@[simp]
theorem Std.ExtHashMap.getThenInsertIfNew?_snd {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
(m.getThenInsertIfNew? k v).snd = m.insertIfNew k v
source
instance Std.ExtHashMap.instLawfulGetElemMem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] :
LawfulGetElem (ExtHashMap α β) α β fun (m : ExtHashMap α β) (a : α) => a ∈ m
source
@[simp]
theorem Std.ExtHashMap.insertMany_nil {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] :
m.insertMany [] = m
source
@[simp]
theorem Std.ExtHashMap.insertMany_list_singleton {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
m.insertMany [(k, v)] = m.insert k v
source
theorem Std.ExtHashMap.insertMany_cons {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {v : β} :
m.insertMany ((k, v) :: l) = (m.insert k v).insertMany l
source
theorem Std.ExtHashMap.insertMany_append {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l₁ l₂ : List (α × β)} :
m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
source
theorem Std.ExtHashMap.insertMany_ind {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {ρ : Type w} [ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {motive : ExtHashMap α β → Prop} (m : ExtHashMap α β) {l : ρ} (init : motive m) (insert : ∀ (m : ExtHashMap α β) (a : α) (b : β), motive m → motive (m.insert a b)) :
motive (m.insertMany l)
source
@[simp]
theorem Std.ExtHashMap.contains_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
(m.insertMany l).contains k = (m.contains k || (List.map Prod.fst l).contains k)
source
@[simp]
theorem Std.ExtHashMap.mem_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
k ∈ m.insertMany l ↔ k ∈ m ∨ (List.map Prod.fst l).contains k = true
source
theorem Std.ExtHashMap.mem_of_mem_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (mem : k ∈ m.insertMany l) (contains_eq_false : (List.map Prod.fst l).contains k = false) :
k ∈ m
source
theorem Std.ExtHashMap.mem_insertMany_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} {ρ : Type w} [ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ} {k : α} :
k ∈ m → k ∈ m.insertMany l
source
theorem Std.ExtHashMap.getElem?_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(m.insertMany l)[k]? = m[k]?
source
theorem Std.ExtHashMap.getElem?_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {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) :
(m.insertMany l)[k']? = some v
source
theorem Std.ExtHashMap.getElem?_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
(m.insertMany l)[k]? = (List.findSomeRev? (fun (x : α × β) => match x with | (a, b) => if (a == k) = true then some b else none) l).or m[k]?
source
theorem Std.ExtHashMap.getElem_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h : k ∈ m.insertMany l} :
(m.insertMany l)[k] = m[k]
source
theorem Std.ExtHashMap.getElem_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {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 : k' ∈ m.insertMany l} :
(m.insertMany l)[k'] = v
source
theorem Std.ExtHashMap.getElem!_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(m.insertMany l)[k]! = m[k]!
source
theorem Std.ExtHashMap.getElem!_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {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) :
(m.insertMany l)[k']! = v
source
theorem Std.ExtHashMap.getD_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(m.insertMany l).getD k fallback = m.getD k fallback
source
theorem Std.ExtHashMap.getD_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {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) :
(m.insertMany l).getD k' fallback = v
source
theorem Std.ExtHashMap.getKey?_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(m.insertMany l).getKey? k = m.getKey? k
source
theorem Std.ExtHashMap.getKey?_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [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) :
(m.insertMany l).getKey? k' = some k
source
theorem Std.ExtHashMap.getKey_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h : k ∈ m.insertMany l} :
(m.insertMany l).getKey k h = m.getKey k ⋯
source
theorem Std.ExtHashMap.getKey_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [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 : k' ∈ m.insertMany l} :
(m.insertMany l).getKey k' h = k
source
theorem Std.ExtHashMap.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(m.insertMany l).getKey! k = m.getKey! k
source
theorem Std.ExtHashMap.getKey!_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [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) :
(m.insertMany l).getKey! k' = k
source
theorem Std.ExtHashMap.getKeyD_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(m.insertMany l).getKeyD k fallback = m.getKeyD k fallback
source
theorem Std.ExtHashMap.getKeyD_insertMany_list_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [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) :
(m.insertMany l).getKeyD k' fallback = k
source
theorem Std.ExtHashMap.size_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) :
(∀ (a : α), a ∈ m → (List.map Prod.fst l).contains a = false) → (m.insertMany l).size = m.size + l.length
source
theorem Std.ExtHashMap.size_le_size_insertMany_list {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
m.size ≤ (m.insertMany l).size
source
theorem Std.ExtHashMap.size_le_size_insertMany {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} {ρ : Type w} [ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ} :
m.size ≤ (m.insertMany l).size
source
theorem Std.ExtHashMap.size_insertMany_list_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
(m.insertMany l).size ≤ m.size + l.length
source
@[simp]
theorem Std.ExtHashMap.insertMany_list_eq_empty_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
m.insertMany l = ∅ ↔ m = ∅ ∧ l = []
source
theorem Std.ExtHashMap.eq_empty_of_insertMany_eq_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} {ρ : Type w} [ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ} :
m.insertMany l = ∅ → m = ∅
source
@[simp]
theorem Std.ExtHashMap.insertManyIfNewUnit_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] :
m.insertManyIfNewUnit [] = m
source
@[simp]
theorem Std.ExtHashMap.insertManyIfNewUnit_list_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {k : α} :
m.insertManyIfNewUnit [k] = m.insertIfNew k ()
source
theorem Std.ExtHashMap.insertManyIfNewUnit_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
m.insertManyIfNewUnit (k :: l) = (m.insertIfNew k ()).insertManyIfNewUnit l
source
theorem Std.ExtHashMap.insertManyIfNewUnit_ind {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {ρ : Type w} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {motive : ExtHashMap α Unit → Prop} (m : ExtHashMap α Unit) (l : ρ) (init : motive m) (insert : ∀ (m : ExtHashMap α Unit) (a : α), motive m → motive (m.insertIfNew a ())) :
motive (m.insertManyIfNewUnit l)
source
@[simp]
theorem Std.ExtHashMap.contains_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
(m.insertManyIfNewUnit l).contains k = (m.contains k || l.contains k)
source
@[simp]
theorem Std.ExtHashMap.mem_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
k ∈ m.insertManyIfNewUnit l ↔ k ∈ m ∨ l.contains k = true
source
theorem Std.ExtHashMap.mem_of_mem_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
k ∈ m.insertManyIfNewUnit l → k ∈ m
source
theorem Std.ExtHashMap.mem_insertManyIfNewUnit_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} {ρ : Type w} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {l : ρ} {k : α} :
k ∈ m → k ∈ m.insertManyIfNewUnit l
source
theorem Std.ExtHashMap.getElem?_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
(m.insertManyIfNewUnit l)[k]? = if k ∈ m ∨ l.contains k = true then some () else none
source
theorem Std.ExtHashMap.getElem_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} {h : k ∈ m.insertManyIfNewUnit l} :
(m.insertManyIfNewUnit l)[k] = ()
source
theorem Std.ExtHashMap.getElem!_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
(m.insertManyIfNewUnit l)[k]! = ()
source
theorem Std.ExtHashMap.getD_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} {fallback : Unit} :
(m.insertManyIfNewUnit l).getD k fallback = ()
source
theorem Std.ExtHashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) :
(m.insertManyIfNewUnit l).getKey? k = none
source
theorem Std.ExtHashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :
(m.insertManyIfNewUnit l).getKey? k' = some k
source
theorem Std.ExtHashMap.getKey?_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (mem : k ∈ m) :
(m.insertManyIfNewUnit l).getKey? k = m.getKey? k
source
theorem Std.ExtHashMap.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) {h : k' ∈ m.insertManyIfNewUnit l} :
(m.insertManyIfNewUnit l).getKey k' h = k
source
theorem Std.ExtHashMap.getKey_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (mem : k ∈ m) {h : k ∈ m.insertManyIfNewUnit l} :
(m.insertManyIfNewUnit l).getKey k h = m.getKey k mem
source
theorem Std.ExtHashMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) :
(m.insertManyIfNewUnit l).getKey! k = default
source
theorem Std.ExtHashMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :
(m.insertManyIfNewUnit l).getKey! k' = k
source
theorem Std.ExtHashMap.getKey!_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (mem : k ∈ m) :
(m.insertManyIfNewUnit l).getKey! k = m.getKey! k
source
theorem Std.ExtHashMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (not_mem : ¬k ∈ m) (contains_eq_false : l.contains k = false) :
(m.insertManyIfNewUnit l).getKeyD k fallback = fallback
source
theorem Std.ExtHashMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) (not_mem : ¬k ∈ m) (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) (mem : k ∈ l) :
(m.insertManyIfNewUnit l).getKeyD k' fallback = k
source
theorem Std.ExtHashMap.getKeyD_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (mem : k ∈ m) :
(m.insertManyIfNewUnit l).getKeyD k fallback = m.getKeyD k fallback
source
theorem Std.ExtHashMap.size_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :
(∀ (a : α), a ∈ m → l.contains a = false) → (m.insertManyIfNewUnit l).size = m.size + l.length
source
theorem Std.ExtHashMap.size_le_size_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} :
m.size ≤ (m.insertManyIfNewUnit l).size
source
theorem Std.ExtHashMap.size_le_size_insertManyIfNewUnit {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} {ρ : Type w} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {l : ρ} :
m.size ≤ (m.insertManyIfNewUnit l).size
source
theorem Std.ExtHashMap.size_insertManyIfNewUnit_list_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} :
(m.insertManyIfNewUnit l).size ≤ m.size + l.length
source
@[simp]
theorem Std.ExtHashMap.insertManyIfNewUnit_list_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α} :
m.insertManyIfNewUnit l = ∅ ↔ m = ∅ ∧ l = []
source
theorem Std.ExtHashMap.eq_empty_of_insertManyIfNewUnit_eq_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α Unit} {ρ : Type w} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {l : ρ} :
m.insertManyIfNewUnit l = ∅ → m = ∅
source
@[simp]
theorem Std.ExtHashMap.ofList_nil {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] :
ofList [] = ∅
source
@[simp]
theorem Std.ExtHashMap.ofList_singleton {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
ofList [(k, v)] = ∅.insert k v
source
theorem Std.ExtHashMap.ofList_cons {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} {tl : List (α × β)} :
ofList ((k, v) :: tl) = (∅.insert k v).insertMany tl
source
theorem Std.ExtHashMap.ofList_eq_insertMany_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
ofList l = ∅.insertMany l
source
@[simp]
theorem Std.ExtHashMap.contains_ofList {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
(ofList l).contains k = (List.map Prod.fst l).contains k
source
@[simp]
theorem Std.ExtHashMap.mem_ofList {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
k ∈ ofList l ↔ (List.map Prod.fst l).contains k = true
source
theorem Std.ExtHashMap.getElem?_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(ofList l)[k]? = none
source
theorem Std.ExtHashMap.getElem?_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {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) :
(ofList l)[k']? = some v
source
theorem Std.ExtHashMap.getElem_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {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 : k' ∈ ofList l} :
(ofList l)[k'] = v
source
theorem Std.ExtHashMap.getElem!_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} [Inhabited β] (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(ofList l)[k]! = default
source
theorem Std.ExtHashMap.getElem!_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {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) :
(ofList l)[k']! = v
source
theorem Std.ExtHashMap.getD_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(ofList l).getD k fallback = fallback
source
theorem Std.ExtHashMap.getD_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {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) :
(ofList l).getD k' fallback = v
source
theorem Std.ExtHashMap.getKey?_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(ofList l).getKey? k = none
source
theorem Std.ExtHashMap.getKey?_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [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) :
(ofList l).getKey? k' = some k
source
theorem Std.ExtHashMap.getKey_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [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 : k' ∈ ofList l} :
(ofList l).getKey k' h = k
source
theorem Std.ExtHashMap.getKey!_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(ofList l).getKey! k = default
source
theorem Std.ExtHashMap.getKey!_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [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) :
(ofList l).getKey! k' = k
source
theorem Std.ExtHashMap.getKeyD_ofList_of_contains_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(ofList l).getKeyD k fallback = fallback
source
theorem Std.ExtHashMap.getKeyD_ofList_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [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) :
(ofList l).getKeyD k' fallback = k
source
theorem Std.ExtHashMap.size_ofList {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) :
(ofList l).size = l.length
source
theorem Std.ExtHashMap.size_ofList_le {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
(ofList l).size ≤ l.length
source
@[simp]
theorem Std.ExtHashMap.ofList_eq_empty_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
ofList l = ∅ ↔ l = []
source
@[simp]
theorem Std.ExtHashMap.unitOfList_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] :
unitOfList [] = ∅
source
@[simp]
theorem Std.ExtHashMap.unitOfList_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {k : α} :
unitOfList [k] = ∅.insertIfNew k ()
source
theorem Std.ExtHashMap.unitOfList_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} :
unitOfList (hd :: tl) = (∅.insertIfNew hd ()).insertManyIfNewUnit tl
source
@[simp]
theorem Std.ExtHashMap.contains_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
(unitOfList l).contains k = l.contains k
source
@[simp]
theorem Std.ExtHashMap.mem_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
k ∈ unitOfList l ↔ l.contains k = true
source
@[simp]
theorem Std.ExtHashMap.getElem?_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
(unitOfList l)[k]? = if l.contains k = true then some () else none
source
@[simp]
theorem Std.ExtHashMap.getElem_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} {h : k ∈ unitOfList l} :
(unitOfList l)[k] = ()
source
@[simp]
theorem Std.ExtHashMap.getElem!_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
(unitOfList l)[k]! = ()
source
@[simp]
theorem Std.ExtHashMap.getD_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} {fallback : Unit} :
(unitOfList l).getD k fallback = ()
source
theorem Std.ExtHashMap.getKey?_unitOfList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
(unitOfList l).getKey? k = none
source
theorem Std.ExtHashMap.getKey?_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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) :
(unitOfList l).getKey? k' = some k
source
theorem Std.ExtHashMap.getKey_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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 : k' ∈ unitOfList l} :
(unitOfList l).getKey k' h = k
source
theorem Std.ExtHashMap.getKey!_unitOfList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
(unitOfList l).getKey! k = default
source
theorem Std.ExtHashMap.getKey!_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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) :
(unitOfList l).getKey! k' = k
source
theorem Std.ExtHashMap.getKeyD_unitOfList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (contains_eq_false : l.contains k = false) :
(unitOfList l).getKeyD k fallback = fallback
source
theorem Std.ExtHashMap.getKeyD_unitOfList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : 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) :
(unitOfList l).getKeyD k' fallback = k
source
theorem Std.ExtHashMap.size_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :
(unitOfList l).size = l.length
source
theorem Std.ExtHashMap.size_unitOfList_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} :
(unitOfList l).size ≤ l.length
source
@[simp]
theorem Std.ExtHashMap.unitOfList_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} :
unitOfList l = ∅ ↔ l = []
source
theorem Std.ExtHashMap.alter_eq_empty_iff_erase_eq_empty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
m.alter k f = ∅ ↔ m.erase k = ∅ ∧ f m[k]? = none
source
@[simp]
theorem Std.ExtHashMap.alter_eq_empty_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
m.alter k f = ∅ ↔ (m = ∅ ∨ m.size = 1 ∧ k ∈ m) ∧ f m[k]? = none
source
theorem Std.ExtHashMap.contains_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
(m.alter k f).contains k' = if (k == k') = true then (f m[k]?).isSome else m.contains k'
source
theorem Std.ExtHashMap.mem_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
k' ∈ m.alter k f ↔ if (k == k') = true then (f m[k]?).isSome = true else k' ∈ m
source
theorem Std.ExtHashMap.mem_alter_of_beq {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : (k == k') = true) :
k' ∈ m.alter k f ↔ (f m[k]?).isSome = true
source
@[simp]
theorem Std.ExtHashMap.contains_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(m.alter k f).contains k = (f m[k]?).isSome
source
@[simp]
theorem Std.ExtHashMap.mem_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
k ∈ m.alter k f ↔ (f m[k]?).isSome = true
source
theorem Std.ExtHashMap.contains_alter_of_beq_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : (k == k') = false) :
(m.alter k f).contains k' = m.contains k'
source
theorem Std.ExtHashMap.mem_alter_of_beq_eq_false {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : (k == k') = false) :
k' ∈ m.alter k f ↔ k' ∈ m
source
theorem Std.ExtHashMap.size_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(m.alter k f).size = if k ∈ m ∧ (f m[k]?).isNone = true then m.size - 1 else if ¬k ∈ m ∧ (f m[k]?).isSome = true then m.size + 1 else m.size
source
theorem Std.ExtHashMap.size_alter_eq_add_one {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : ¬k ∈ m) (h' : (f m[k]?).isSome = true) :
(m.alter k f).size = m.size + 1
source
theorem Std.ExtHashMap.size_alter_eq_sub_one {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : k ∈ m) (h' : (f m[k]?).isNone = true) :
(m.alter k f).size = m.size - 1
source
theorem Std.ExtHashMap.size_alter_eq_self_of_not_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : ¬k ∈ m) (h' : (f m[k]?).isNone = true) :
(m.alter k f).size = m.size
source
theorem Std.ExtHashMap.size_alter_eq_self_of_mem {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : k ∈ m) (h' : (f m[k]?).isSome = true) :
(m.alter k f).size = m.size
source
theorem Std.ExtHashMap.size_alter_le_size {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(m.alter k f).size ≤ m.size + 1
source
theorem Std.ExtHashMap.size_le_size_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
m.size - 1 ≤ (m.alter k f).size
source
theorem Std.ExtHashMap.getElem?_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
(m.alter k f)[k']? = if (k == k') = true then f m[k]? else m[k']?
source
@[deprecated Std.ExtHashMap.getElem?_alter (since := "2025-02-09")]
theorem Std.ExtHashMap.get?_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
(m.alter k f).get? k' = if (k == k') = true then f (m.get? k) else m.get? k'
source
@[simp]
theorem Std.ExtHashMap.getElem?_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(m.alter k f)[k]? = f m[k]?
source
@[deprecated Std.ExtHashMap.getElem?_alter_self (since := "2025-02-09")]
theorem Std.ExtHashMap.get?_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(m.alter k f).get? k = f (m.get? k)
source
theorem Std.ExtHashMap.getElem_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} {h : k' ∈ m.alter k f} :
(m.alter k f)[k'] = if heq : (k == k') = true then (f m[k]?).get ⋯ else m[k']
source
@[deprecated Std.ExtHashMap.getElem_alter (since := "2025-02-09")]
theorem Std.ExtHashMap.get_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} {h : k' ∈ m.alter k f} :
(m.alter k f).get k' h = if heq : (k == k') = true then (f (m.get? k)).get ⋯ else m.get k' ⋯
source
@[simp]
theorem Std.ExtHashMap.getElem_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} {h : k ∈ m.alter k f} :
(m.alter k f)[k] = (f m[k]?).get ⋯
source
@[deprecated Std.ExtHashMap.getElem_alter_self (since := "2025-02-09")]
theorem Std.ExtHashMap.get_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} {h : k ∈ m.alter k f} :
(m.alter k f).get k h = (f (m.get? k)).get ⋯
source
theorem Std.ExtHashMap.getElem!_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : Option β → Option β} :
(m.alter k f)[k']! = if (k == k') = true then (f m[k]?).get! else m[k']!
source
@[deprecated Std.ExtHashMap.getElem!_alter (since := "2025-02-09")]
theorem Std.ExtHashMap.get!_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : Option β → Option β} :
(m.alter k f).get! k' = if (k == k') = true then (f (m.get? k)).get! else m.get! k'
source
@[simp]
theorem Std.ExtHashMap.getElem!_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : Option β → Option β} :
(m.alter k f)[k]! = (f m[k]?).get!
source
@[deprecated Std.ExtHashMap.getElem!_alter_self (since := "2025-02-09")]
theorem Std.ExtHashMap.get!_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : Option β → Option β} :
(m.alter k f).get! k = (f (m.get? k)).get!
source
theorem Std.ExtHashMap.getD_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β} :
(m.alter k f).getD k' fallback = if (k == k') = true then (f m[k]?).getD fallback else m.getD k' fallback
source
@[simp]
theorem Std.ExtHashMap.getD_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : Option β → Option β} :
(m.alter k f).getD k fallback = (f m[k]?).getD fallback
source
theorem Std.ExtHashMap.getKey?_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
(m.alter k f).getKey? k' = if (k == k') = true then if (f m[k]?).isSome = true then some k else none else m.getKey? k'
source
theorem Std.ExtHashMap.getKey?_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
(m.alter k f).getKey? k = if (f m[k]?).isSome = true then some k else none
source
theorem Std.ExtHashMap.getKey!_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : Option β → Option β} :
(m.alter k f).getKey! k' = if (k == k') = true then if (f m[k]?).isSome = true then k else default else m.getKey! k'
source
theorem Std.ExtHashMap.getKey!_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : Option β → Option β} :
(m.alter k f).getKey! k = if (f m[k]?).isSome = true then k else default
source
theorem Std.ExtHashMap.getKey_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : Option β → Option β} {h : k' ∈ m.alter k f} :
(m.alter k f).getKey k' h = if heq : (k == k') = true then k else m.getKey k' ⋯
source
@[simp]
theorem Std.ExtHashMap.getKey_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : Option β → Option β} {h : k ∈ m.alter k f} :
(m.alter k f).getKey k h = k
source
theorem Std.ExtHashMap.getKeyD_alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β} :
(m.alter k f).getKeyD k' fallback = if (k == k') = true then if (f m[k]?).isSome = true then k else fallback else m.getKeyD k' fallback
source
theorem Std.ExtHashMap.getKeyD_alter_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : Option β → Option β} :
(m.alter k f).getKeyD k fallback = if (f m[k]?).isSome = true then k else fallback
source
@[simp]
theorem Std.ExtHashMap.modify_eq_empty_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
m.modify k f = ∅ ↔ m = ∅
source
@[simp]
theorem Std.ExtHashMap.contains_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
(m.modify k f).contains k' = m.contains k'
source
@[simp]
theorem Std.ExtHashMap.mem_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
k' ∈ m.modify k f ↔ k' ∈ m
source
@[simp]
theorem Std.ExtHashMap.size_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
(m.modify k f).size = m.size
source
theorem Std.ExtHashMap.getElem?_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
(m.modify k f)[k']? = if (k == k') = true then Option.map f m[k]? else m[k']?
source
@[deprecated Std.ExtHashMap.getElem?_modify (since := "2025-02-09")]
theorem Std.ExtHashMap.get?_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
(m.modify k f).get? k' = if (k == k') = true then Option.map f (m.get? k) else m.get? k'
source
@[simp]
theorem Std.ExtHashMap.getElem?_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
(m.modify k f)[k]? = Option.map f m[k]?
source
@[deprecated Std.ExtHashMap.getElem?_modify_self (since := "2025-02-09")]
theorem Std.ExtHashMap.get?_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
(m.modify k f).get? k = Option.map f (m.get? k)
source
theorem Std.ExtHashMap.getElem_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} {h : k' ∈ m.modify k f} :
(m.modify k f)[k'] = if heq : (k == k') = true then f m[k] else m[k']
source
@[deprecated Std.ExtHashMap.getElem_modify (since := "2025-02-09")]
theorem Std.ExtHashMap.get_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} {h : k' ∈ m.modify k f} :
(m.modify k f).get k' h = if heq : (k == k') = true then f (m.get k ⋯) else m.get k' ⋯
source
@[simp]
theorem Std.ExtHashMap.getElem_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} {h : k ∈ m.modify k f} :
(m.modify k f)[k] = f m[k]
source
@[deprecated Std.ExtHashMap.getElem_modify_self (since := "2025-02-09")]
theorem Std.ExtHashMap.get_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} {h : k ∈ m.modify k f} :
(m.modify k f).get k h = f (m.get k ⋯)
source
theorem Std.ExtHashMap.getElem!_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} :
(m.modify k f)[k']! = if (k == k') = true then (Option.map f m[k]?).get! else m[k']!
source
@[deprecated Std.ExtHashMap.getElem!_modify (since := "2025-02-09")]
theorem Std.ExtHashMap.get!_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} :
(m.modify k f).get! k' = if (k == k') = true then (Option.map f (m.get? k)).get! else m.get! k'
source
@[simp]
theorem Std.ExtHashMap.getElem!_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} :
(m.modify k f)[k]! = (Option.map f m[k]?).get!
source
@[deprecated Std.ExtHashMap.getElem!_modify_self (since := "2025-02-09")]
theorem Std.ExtHashMap.get!_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} :
(m.modify k f).get! k = (Option.map f (m.get? k)).get!
source
theorem Std.ExtHashMap.getD_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} :
(m.modify k f).getD k' fallback = if (k == k') = true then (Option.map f m[k]?).getD fallback else m.getD k' fallback
source
@[simp]
theorem Std.ExtHashMap.getD_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} :
(m.modify k f).getD k fallback = (Option.map f m[k]?).getD fallback
source
theorem Std.ExtHashMap.getKey?_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
(m.modify k f).getKey? k' = if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'
source
theorem Std.ExtHashMap.getKey?_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
(m.modify k f).getKey? k = if k ∈ m then some k else none
source
theorem Std.ExtHashMap.getKey!_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} :
(m.modify k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'
source
theorem Std.ExtHashMap.getKey!_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} :
(m.modify k f).getKey! k = if k ∈ m then k else default
source
theorem Std.ExtHashMap.getKey_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} {h : k' ∈ m.modify k f} :
(m.modify k f).getKey k' h = if (k == k') = true then k else m.getKey k' ⋯
source
@[simp]
theorem Std.ExtHashMap.getKey_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} {h : k ∈ m.modify k f} :
(m.modify k f).getKey k h = k
source
theorem Std.ExtHashMap.getKeyD_modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} :
(m.modify k f).getKeyD k' fallback = if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback
source
theorem Std.ExtHashMap.getKeyD_modify_self {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β} :
(m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback
source
theorem Std.ExtHashMap.ext_getKey_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : ExtHashMap α β} (hk : ∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') (hv : ∀ (k : α), m₁[k]? = m₂[k]?) :
m₁ = m₂
source
theorem Std.ExtHashMap.ext_getKey_getElem?_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : ExtHashMap α β} :
m₁ = m₂ ↔ (∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') ∧ ∀ (k : α), m₁[k]? = m₂[k]?
source
theorem Std.ExtHashMap.ext_getElem? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {m₁ m₂ : ExtHashMap α β} (h : ∀ (k : α), m₁[k]? = m₂[k]?) :
m₁ = m₂
source
theorem Std.ExtHashMap.ext_getElem?_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {m₁ m₂ : ExtHashMap α β} :
m₁ = m₂ ↔ ∀ (k : α), m₁[k]? = m₂[k]?
source
theorem Std.ExtHashMap.ext_getKey?_unit {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : ExtHashMap α Unit} (h : ∀ (k : α), m₁.getKey? k = m₂.getKey? k) :
m₁ = m₂
source
theorem Std.ExtHashMap.ext_contains_unit {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {m₁ m₂ : ExtHashMap α Unit} (h : ∀ (k : α), m₁.contains k = m₂.contains k) :
m₁ = m₂
source
theorem Std.ExtHashMap.ext_mem_unit {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {m₁ m₂ : ExtHashMap α Unit} (h : ∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) :
m₁ = m₂
source
theorem Std.ExtHashMap.filterMap_eq_empty_iff {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} :
filterMap f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = none
source
theorem Std.ExtHashMap.mem_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} :
k ∈ filterMap f m ↔ ∃ (h : k ∈ m), (f (m.getKey k h) m[k]).isSome = true
source
theorem Std.ExtHashMap.contains_of_contains_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} :
(filterMap f m).contains k = true → m.contains k = true
source
theorem Std.ExtHashMap.mem_of_mem_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} :
k ∈ filterMap f m → k ∈ m
source
theorem Std.ExtHashMap.size_filterMap_le_size {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} :
(filterMap f m).size ≤ m.size
source
theorem Std.ExtHashMap.size_filterMap_eq_size_iff {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} :
(filterMap f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), (f (m.getKey k h) m[k]).isSome = true
source
@[simp]
theorem Std.ExtHashMap.getElem?_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} :
(filterMap f m)[k]? = m[k]?.pbind fun (x : β) (h' : m[k]? = some x) => f (m.getKey k ⋯) x
source
theorem Std.ExtHashMap.getElem?_filterMap' {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} :
(filterMap f m)[k]? = m[k]?.bind fun (x : β) => f k x

Simpler variant of getElem?_filterMap when LawfulBEq is available.

source
theorem Std.ExtHashMap.getElem?_filterMap_of_getKey?_eq_some {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k k' : α} (h : m.getKey? k = some k') :
(filterMap f m)[k]? = m[k]?.bind (f k')
source
theorem Std.ExtHashMap.isSome_apply_of_mem_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} (h : k ∈ filterMap f m) :
(f (m.getKey k ⋯) m[k]).isSome = true
source
@[simp]
theorem Std.ExtHashMap.getElem_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} {h : k ∈ filterMap f m} :
(filterMap f m)[k] = (f (m.getKey k ⋯) m[k]).get ⋯
source
theorem Std.ExtHashMap.getElem_filterMap' {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} {h : k ∈ filterMap f m} :
(filterMap f m)[k] = (f k m[k]).get ⋯

Simpler variant of getElem_filterMap when LawfulBEq is available.

source
theorem Std.ExtHashMap.getElem!_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : α → β → Option γ} {k : α} :
(filterMap f m)[k]! = (m[k]?.pbind fun (x : β) (h' : m[k]? = some x) => f (m.getKey k ⋯) x).get!
source
theorem Std.ExtHashMap.getElem!_filterMap_of_getKey?_eq_some {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : α → β → Option γ} {k k' : α} (h : m.getKey? k = some k') :
(filterMap f m)[k]! = (m[k]?.bind (f k')).get!
source
theorem Std.ExtHashMap.getD_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ} :
(filterMap f m).getD k fallback = (m[k]?.pbind fun (x : β) (h' : m[k]? = some x) => f (m.getKey k ⋯) x).getD fallback
source
theorem Std.ExtHashMap.getD_filterMap_of_getKey?_eq_some {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k k' : α} {fallback : γ} (h : m.getKey? k = some k') :
(filterMap f m).getD k fallback = (m[k]?.bind (f k')).getD fallback
source
theorem Std.ExtHashMap.getKey?_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} :
(filterMap f m).getKey? k = (m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => (f x m[x]).isSome
source
@[simp]
theorem Std.ExtHashMap.getKey_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k : α} {h' : k ∈ filterMap f m} :
(filterMap f m).getKey k h' = m.getKey k ⋯
source
theorem Std.ExtHashMap.getKey!_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : α → β → Option γ} {k : α} :
(filterMap f m).getKey! k = ((m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => (f x m[x]).isSome).get!
source
theorem Std.ExtHashMap.getKeyD_filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Option γ} {k fallback : α} :
(filterMap f m).getKeyD k fallback = ((m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => (f x m[x]).isSome).getD fallback
source
theorem Std.ExtHashMap.filterMap_eq_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} :
filterMap (fun (k : α) => Option.guard fun (v : β) => f k v) m = filter f m
source
theorem Std.ExtHashMap.filter_eq_empty_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} :
filter f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = false
source
theorem Std.ExtHashMap.mem_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} :
k ∈ filter f m ↔ ∃ (h' : k ∈ m), f (m.getKey k h') m[k] = true
source
theorem Std.ExtHashMap.contains_of_contains_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} :
(filter f m).contains k = true → m.contains k = true
source
theorem Std.ExtHashMap.mem_of_mem_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} :
k ∈ filter f m → k ∈ m
source
theorem Std.ExtHashMap.size_filter_le_size {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} :
(filter f m).size ≤ m.size
source
theorem Std.ExtHashMap.size_filter_eq_size_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} :
(filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) (m.get k h) = true
source
theorem Std.ExtHashMap.filter_eq_self_iff {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} :
filter f m = m ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) (m.get k h) = true
source
theorem Std.ExtHashMap.getElem?_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} :
(filter f m)[k]? = m[k]?.pfilter fun (x : β) (h' : m[k]? = some x) => f (m.getKey k ⋯) x
source
@[simp]
theorem Std.ExtHashMap.getElem?_filter' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} :
(filter f m)[k]? = Option.filter (f k) m[k]?

Simpler variant of getElem?_filter when LawfulBEq is available.

source
theorem Std.ExtHashMap.getElem?_filter_of_getKey?_eq_some {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α} :
m.getKey? k = some k' → (filter f m)[k]? = Option.filter (fun (x : β) => f k' x) m[k]?
source
@[simp]
theorem Std.ExtHashMap.getElem_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} {h' : k ∈ filter f m} :
(filter f m)[k] = m[k]
source
theorem Std.ExtHashMap.getElem!_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {f : α → β → Bool} {k : α} :
(filter f m)[k]! = (m[k]?.pfilter fun (x : β) (h' : m[k]? = some x) => f (m.getKey k ⋯) x).get!
source
theorem Std.ExtHashMap.getElem!_filter' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [LawfulHashable α] [Inhabited β] {f : α → β → Bool} {k : α} :
(filter f m)[k]! = (Option.filter (f k) m[k]?).get!

Simpler variant of getElem!_filter when LawfulBEq is available.

source
theorem Std.ExtHashMap.getElem!_filter_of_getKey?_eq_some {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {f : α → β → Bool} {k k' : α} :
m.getKey? k = some k' → (filter f m)[k]! = (Option.filter (f k') m[k]?).get!
source
theorem Std.ExtHashMap.getD_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β} :
(filter f m).getD k fallback = (m[k]?.pfilter fun (x : β) (h' : m[k]? = some x) => f (m.getKey k ⋯) x).getD fallback
source
theorem Std.ExtHashMap.getD_filter' {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β} :
(filter f m).getD k fallback = (Option.filter (f k) m[k]?).getD fallback

Simpler variant of getD_filter when LawfulBEq is available.

source
theorem Std.ExtHashMap.getD_filter_of_getKey?_eq_some {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k k' : α} {fallback : β} :
m.getKey? k = some k' → (filter f m).getD k fallback = (Option.filter (fun (x : β) => f k' x) m[k]?).getD fallback
source
theorem Std.ExtHashMap.getKey?_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} :
(filter f m).getKey? k = (m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => f x m[x]
source
theorem Std.ExtHashMap.getKey?_filter_key {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k : α} :
(filter (fun (k : α) (x : β) => f k) m).getKey? k = Option.filter f (m.getKey? k)
source
@[simp]
theorem Std.ExtHashMap.getKey_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k : α} {h' : k ∈ filter f m} :
(filter f m).getKey k h' = m.getKey k ⋯
source
theorem Std.ExtHashMap.getKey!_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : α → β → Bool} {k : α} :
(filter f m).getKey! k = ((m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => f x m[x]).get!
source
theorem Std.ExtHashMap.getKey!_filter_key {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : α → Bool} {k : α} :
(filter (fun (k : α) (x : β) => f k) m).getKey! k = (Option.filter f (m.getKey? k)).get!
source
theorem Std.ExtHashMap.getKeyD_filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → Bool} {k fallback : α} :
(filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => f x m[x]).getD fallback
source
theorem Std.ExtHashMap.getKeyD_filter_key {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → Bool} {k fallback : α} :
(filter (fun (k : α) (x : β) => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD fallback
source
@[simp]
theorem Std.ExtHashMap.map_id_fun {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] :
map (fun (x : α) (v : β) => v) m = m
source
@[simp]
theorem Std.ExtHashMap.map_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type w'} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {g : α → γ → δ} :
map g (map f m) = map (fun (k : α) (v : β) => g k (f k v)) m
source
theorem Std.ExtHashMap.filterMap_equiv_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} :
filterMap (fun (k : α) (v : β) => some (f k v)) m = map f m
source
@[simp]
theorem Std.ExtHashMap.map_eq_empty_iff {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} :
map f m = ∅ ↔ m = ∅
source
@[simp]
theorem Std.ExtHashMap.contains_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} :
(map f m).contains k = m.contains k
source
theorem Std.ExtHashMap.contains_of_contains_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} :
(map f m).contains k = true → m.contains k = true
source
@[simp]
theorem Std.ExtHashMap.mem_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} :
k ∈ map f m ↔ k ∈ m
source
theorem Std.ExtHashMap.mem_of_mem_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} :
k ∈ map f m → k ∈ m
source
@[simp]
theorem Std.ExtHashMap.size_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} :
(map f m).size = m.size
source
@[simp]
theorem Std.ExtHashMap.getElem?_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} :
(map f m)[k]? = Option.map (f k) m[k]?
source
@[simp]
theorem Std.ExtHashMap.getElem?_map' {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} :
(map f m)[k]? = Option.pmap (fun (v : β) (h' : k ∈ m) => f (m.getKey k h') v) m[k]? ⋯

Variant of getElem?_map that holds with EquivBEq (i.e. without LawfulBEq).

source
theorem Std.ExtHashMap.getElem?_map_of_getKey?_eq_some {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k k' : α} (h : m.getKey? k = some k') :
(map f m)[k]? = Option.map (f k') m[k]?
source
@[simp]
theorem Std.ExtHashMap.getElem_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ map f m} :
(map f m)[k] = f k m[k]
source
@[simp]
theorem Std.ExtHashMap.getElem_map' {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ map f m} :
(map f m)[k] = f (m.getKey k ⋯) m[k]

Variant of getElem_map that holds with EquivBEq (i.e. without LawfulBEq).

source
theorem Std.ExtHashMap.getElem!_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k : α} :
(map f m)[k]! = (Option.map (f k) m[k]?).get!
source
theorem Std.ExtHashMap.getElem!_map' {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k : α} :
(map f m)[k]! = (Option.pmap (fun (v : β) (h : k ∈ m) => f (m.getKey k h) v) m[k]? ⋯).get!

Variant of getElem!_map that holds with EquivBEq (i.e. without LawfulBEq).

source
theorem Std.ExtHashMap.getElem!_map_of_getKey?_eq_some {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k k' : α} (h : m.getKey? k = some k') :
(map f m)[k]! = (Option.map (f k') m[k]?).get!
source
theorem Std.ExtHashMap.getD_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [LawfulBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ} :
(map f m).getD k fallback = (Option.map (f k) m[k]?).getD fallback
source
theorem Std.ExtHashMap.getD_map' {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} {fallback : γ} :
(map f m).getD k fallback = (Option.pmap (fun (v : β) (h : k ∈ m) => f (m.getKey k h) v) m[k]? ⋯).getD fallback

Variant of getD_map that holds with EquivBEq (i.e. without LawfulBEq).

source
theorem Std.ExtHashMap.getD_map_of_getKey?_eq_some {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ} (h : m.getKey? k = some k') :
(map f m).getD k fallback = (Option.map (f k') m[k]?).getD fallback
source
@[simp]
theorem Std.ExtHashMap.getKey?_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} :
(map f m).getKey? k = m.getKey? k
source
@[simp]
theorem Std.ExtHashMap.getKey_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ map f m} :
(map f m).getKey k h' = m.getKey k ⋯
source
@[simp]
theorem Std.ExtHashMap.getKey!_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : α → β → γ} {k : α} :
(map f m).getKey! k = m.getKey! k
source
@[simp]
theorem Std.ExtHashMap.getKeyD_map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k fallback : α} :
(map f m).getKeyD k fallback = m.getKeyD k fallback