Documentation

Std.Data.ExtDHashMap.Lemmas

Extensional dependent hash map lemmas #

This file contains lemmas about Std.ExtDHashMap.

@[simp]
theorem Std.ExtDHashMap.isEmpty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] :
@[simp]
theorem Std.ExtDHashMap.isEmpty_eq_false_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] :
@[simp]
theorem Std.ExtDHashMap.empty_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} :
= m m =
@[simp]
theorem Std.ExtDHashMap.emptyWithCapacity_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {c : Nat} :
@[simp]
theorem Std.ExtDHashMap.not_insert_eq_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
¬m.insert k v =
theorem Std.ExtDHashMap.mem_iff_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
@[simp]
theorem Std.ExtDHashMap.contains_iff_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
theorem Std.ExtDHashMap.contains_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) :
theorem Std.ExtDHashMap.mem_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) :
a m b m
@[simp]
theorem Std.ExtDHashMap.contains_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {a : α} :
@[simp]
theorem Std.ExtDHashMap.not_mem_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {a : α} :
theorem Std.ExtDHashMap.eq_empty_iff_forall_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] :
m = ∀ (a : α), m.contains a = false
theorem Std.ExtDHashMap.eq_empty_iff_forall_not_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] :
m = ∀ (a : α), ¬a m
@[simp]
theorem Std.ExtDHashMap.insert_eq_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} :
@[simp]
theorem Std.ExtDHashMap.singleton_eq_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} :
@[simp]
theorem Std.ExtDHashMap.contains_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insert k v).contains a = (k == a || m.contains a)
@[simp]
theorem Std.ExtDHashMap.mem_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insert k v (k == a) = true a m
theorem Std.ExtDHashMap.contains_of_contains_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insert k v).contains a = true(k == a) = falsem.contains a = true
theorem Std.ExtDHashMap.mem_of_mem_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insert k v(k == a) = falsea m
theorem Std.ExtDHashMap.contains_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).contains k = true
theorem Std.ExtDHashMap.mem_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
k m.insert k v
@[simp]
theorem Std.ExtDHashMap.size_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] :
theorem Std.ExtDHashMap.eq_empty_iff_size_eq_zero {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] :
m = m.size = 0
theorem Std.ExtDHashMap.size_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).size = if k m then m.size else m.size + 1
theorem Std.ExtDHashMap.size_le_size_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
m.size (m.insert k v).size
theorem Std.ExtDHashMap.size_insert_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).size m.size + 1
@[simp]
theorem Std.ExtDHashMap.erase_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {k : α} :
@[simp]
theorem Std.ExtDHashMap.erase_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
m.erase k = m = m.size = 1 k m
@[simp]
theorem Std.ExtDHashMap.contains_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = (!k == a && m.contains a)
@[simp]
theorem Std.ExtDHashMap.mem_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.erase k (k == a) = false a m
theorem Std.ExtDHashMap.contains_of_contains_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).contains a = truem.contains a = true
theorem Std.ExtDHashMap.mem_of_mem_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
a m.erase ka m
theorem Std.ExtDHashMap.size_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size = if k m then m.size - 1 else m.size
theorem Std.ExtDHashMap.size_erase_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
(m.erase k).size m.size
theorem Std.ExtDHashMap.size_le_size_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
m.size (m.erase k).size + 1
@[simp]
theorem Std.ExtDHashMap.containsThenInsert_fst {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@[simp]
theorem Std.ExtDHashMap.containsThenInsert_snd {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@[simp]
theorem Std.ExtDHashMap.containsThenInsertIfNew_fst {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@[simp]
theorem Std.ExtDHashMap.containsThenInsertIfNew_snd {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@[simp]
theorem Std.ExtDHashMap.get?_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {a : α} :
theorem Std.ExtDHashMap.get?_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a k : α} {v : β k} :
(m.insert k v).get? a = if h : (k == a) = true then some (cast v) else m.get? a
@[simp]
theorem Std.ExtDHashMap.get?_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {v : β k} :
(m.insert k v).get? k = some v
theorem Std.ExtDHashMap.contains_eq_isSome_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} :
m.contains a = (m.get? a).isSome
@[simp]
theorem Std.ExtDHashMap.isSome_get?_eq_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} :
(m.get? a).isSome = m.contains a
theorem Std.ExtDHashMap.mem_iff_isSome_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} :
a m (m.get? a).isSome = true
@[simp]
theorem Std.ExtDHashMap.isSome_get?_iff_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} :
(m.get? a).isSome = true a m
theorem Std.ExtDHashMap.get?_eq_none_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} :
m.contains a = falsem.get? a = none
theorem Std.ExtDHashMap.get?_eq_none {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} :
¬a mm.get? a = none
theorem Std.ExtDHashMap.get?_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} :
(m.erase k).get? a = if (k == a) = true then none else m.get? a
@[simp]
theorem Std.ExtDHashMap.get?_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} :
(m.erase k).get? k = none
@[simp]
theorem Std.ExtDHashMap.Const.get?_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {a : α} :
theorem Std.ExtDHashMap.Const.get?_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insert k v) a = if (k == a) = true then some v else get? m a
@[simp]
theorem Std.ExtDHashMap.Const.get?_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
get? (m.insert k v) k = some v
theorem Std.ExtDHashMap.Const.contains_eq_isSome_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = (get? m a).isSome
@[simp]
theorem Std.ExtDHashMap.Const.isSome_get?_eq_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} :
(get? m a).isSome = m.contains a
theorem Std.ExtDHashMap.Const.mem_iff_isSome_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} :
a m (get? m a).isSome = true
@[simp]
theorem Std.ExtDHashMap.Const.isSome_get?_iff_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} :
(get? m a).isSome = true a m
theorem Std.ExtDHashMap.Const.get?_eq_none_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} :
m.contains a = falseget? m a = none
theorem Std.ExtDHashMap.Const.get?_eq_none {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} :
¬a mget? m a = none
theorem Std.ExtDHashMap.Const.get?_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k a : α} :
get? (m.erase k) a = if (k == a) = true then none else get? m a
@[simp]
theorem Std.ExtDHashMap.Const.get?_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} :
get? (m.erase k) k = none
theorem Std.ExtDHashMap.Const.get?_eq_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [LawfulBEq α] {a : α} :
get? m a = m.get? a
theorem Std.ExtDHashMap.Const.get?_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) :
get? m a = get? m b
theorem Std.ExtDHashMap.get_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} {v : β k} {h₁ : a m.insert k v} :
(m.insert k v).get a h₁ = if h₂ : (k == a) = true then cast v else m.get a
@[simp]
theorem Std.ExtDHashMap.get_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {v : β k} :
(m.insert k v).get k = v
@[simp]
theorem Std.ExtDHashMap.get_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} {h' : a m.erase k} :
(m.erase k).get a h' = m.get a
theorem Std.ExtDHashMap.get?_eq_some_get {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} (h : a m) :
m.get? a = some (m.get a h)
theorem Std.ExtDHashMap.get_eq_get_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} {h : a m} :
m.get a h = (m.get? a).get
theorem Std.ExtDHashMap.get_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} {h : (m.get? a).isSome = true} :
(m.get? a).get h = m.get a
theorem Std.ExtDHashMap.Const.get_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a m.insert k v} :
get (m.insert k v) a h₁ = if h₂ : (k == a) = true then v else get m a
@[simp]
theorem Std.ExtDHashMap.Const.get_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
get (m.insert k v) k = v
@[simp]
theorem Std.ExtDHashMap.Const.get_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k a : α} {h' : a m.erase k} :
get (m.erase k) a h' = get m a
theorem Std.ExtDHashMap.Const.get?_eq_some_get {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} (h : a m) :
get? m a = some (get m a h)
theorem Std.ExtDHashMap.Const.get_eq_get_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} {h : a m} :
get m a h = (get? m a).get
theorem Std.ExtDHashMap.Const.get_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} {h : (get? m a).isSome = true} :
(get? m a).get h = get m a
theorem Std.ExtDHashMap.Const.get_eq_get {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [LawfulBEq α] {a : α} {h : a m} :
get m a h = m.get a h
theorem Std.ExtDHashMap.Const.get_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a b : α} (hab : (a == b) = true) {h' : a m} :
get m a h' = get m b
@[simp]
theorem Std.ExtDHashMap.get!_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {a : α} [Inhabited (β a)] :
theorem Std.ExtDHashMap.get!_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
(m.insert k v).get! a = if h : (k == a) = true then cast v else m.get! a
@[simp]
theorem Std.ExtDHashMap.get!_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] {b : β a} :
(m.insert a b).get! a = b
theorem Std.ExtDHashMap.get!_eq_default_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] :
theorem Std.ExtDHashMap.get!_eq_default {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] :
¬a mm.get! a = default
theorem Std.ExtDHashMap.get!_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} [Inhabited (β a)] :
(m.erase k).get! a = if (k == a) = true then default else m.get! a
@[simp]
theorem Std.ExtDHashMap.get!_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} [Inhabited (β k)] :
theorem Std.ExtDHashMap.get?_eq_some_get!_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] :
m.contains a = truem.get? a = some (m.get! a)
theorem Std.ExtDHashMap.get?_eq_some_get! {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] :
a mm.get? a = some (m.get! a)
theorem Std.ExtDHashMap.get!_eq_get!_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] :
m.get! a = (m.get? a).get!
theorem Std.ExtDHashMap.get_eq_get! {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] {h : a m} :
m.get a h = m.get! a
@[simp]
theorem Std.ExtDHashMap.Const.get!_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
theorem Std.ExtDHashMap.Const.get!_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insert k v) a = if (k == a) = true then v else get! m a
@[simp]
theorem Std.ExtDHashMap.Const.get!_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} :
get! (m.insert k v) k = v
theorem Std.ExtDHashMap.Const.get!_eq_default_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
theorem Std.ExtDHashMap.Const.get!_eq_default {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
¬a mget! m a = default
theorem Std.ExtDHashMap.Const.get!_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
get! (m.erase k) a = if (k == a) = true then default else get! m a
@[simp]
theorem Std.ExtDHashMap.Const.get!_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} :
theorem Std.ExtDHashMap.Const.get?_eq_some_get!_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
m.contains a = trueget? m a = some (get! m a)
theorem Std.ExtDHashMap.Const.get?_eq_some_get! {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
a mget? m a = some (get! m a)
theorem Std.ExtDHashMap.Const.get!_eq_get!_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
get! m a = (get? m a).get!
theorem Std.ExtDHashMap.Const.get_eq_get! {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} {h : a m} :
get m a h = get! m a
theorem Std.ExtDHashMap.Const.get!_eq_get! {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [LawfulBEq α] [Inhabited β] {a : α} :
get! m a = m.get! a
theorem Std.ExtDHashMap.Const.get!_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b : α} (hab : (a == b) = true) :
get! m a = get! m b
@[simp]
theorem Std.ExtDHashMap.getD_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {a : α} {fallback : β a} :
.getD a fallback = fallback
theorem Std.ExtDHashMap.getD_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
(m.insert k v).getD a fallback = if h : (k == a) = true then cast v else m.getD a fallback
@[simp]
theorem Std.ExtDHashMap.getD_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {fallback v : β k} :
(m.insert k v).getD k fallback = v
theorem Std.ExtDHashMap.getD_eq_fallback_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} :
m.contains a = falsem.getD a fallback = fallback
theorem Std.ExtDHashMap.getD_eq_fallback {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} :
¬a mm.getD a fallback = fallback
theorem Std.ExtDHashMap.getD_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} {fallback : β a} :
(m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
@[simp]
theorem Std.ExtDHashMap.getD_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {fallback : β k} :
(m.erase k).getD k fallback = fallback
theorem Std.ExtDHashMap.get?_eq_some_getD_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} :
m.contains a = truem.get? a = some (m.getD a fallback)
theorem Std.ExtDHashMap.get?_eq_some_getD {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} :
a mm.get? a = some (m.getD a fallback)
theorem Std.ExtDHashMap.getD_eq_getD_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} :
m.getD a fallback = (m.get? a).getD fallback
theorem Std.ExtDHashMap.get_eq_getD {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} {fallback : β a} {h : a m} :
m.get a h = m.getD a fallback
theorem Std.ExtDHashMap.get!_eq_getD_default {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {a : α} [Inhabited (β a)] :
m.get! a = m.getD a default
@[simp]
theorem Std.ExtDHashMap.Const.getD_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
getD a fallback = fallback
theorem Std.ExtDHashMap.Const.getD_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insert k v) a fallback = if (k == a) = true then v else getD m a fallback
@[simp]
theorem Std.ExtDHashMap.Const.getD_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} :
getD (m.insert k v) k fallback = v
theorem Std.ExtDHashMap.Const.getD_eq_fallback_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.contains a = falsegetD m a fallback = fallback
theorem Std.ExtDHashMap.Const.getD_eq_fallback {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
¬a mgetD m a fallback = fallback
theorem Std.ExtDHashMap.Const.getD_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
getD (m.erase k) a fallback = if (k == a) = true then fallback else getD m a fallback
@[simp]
theorem Std.ExtDHashMap.Const.getD_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} :
getD (m.erase k) k fallback = fallback
theorem Std.ExtDHashMap.Const.get?_eq_some_getD_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
m.contains a = trueget? m a = some (getD m a fallback)
theorem Std.ExtDHashMap.Const.get?_eq_some_getD {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
a mget? m a = some (getD m a fallback)
theorem Std.ExtDHashMap.Const.getD_eq_getD_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
getD m a fallback = (get? m a).getD fallback
theorem Std.ExtDHashMap.Const.get_eq_getD {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} {h : a m} :
get m a h = getD m a fallback
theorem Std.ExtDHashMap.Const.get!_eq_getD_default {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
get! m a = getD m a default
theorem Std.ExtDHashMap.Const.getD_eq_getD {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [LawfulBEq α] {a : α} {fallback : β} :
getD m a fallback = m.getD a fallback
theorem Std.ExtDHashMap.Const.getD_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β} (hab : (a == b) = true) :
getD m a fallback = getD m b fallback
@[simp]
theorem Std.ExtDHashMap.getKey?_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {a : α} :
theorem Std.ExtDHashMap.getKey?_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a k : α} {v : β k} :
(m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a
@[simp]
theorem Std.ExtDHashMap.getKey?_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).getKey? k = some k
theorem Std.ExtDHashMap.contains_eq_isSome_getKey? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
@[simp]
theorem Std.ExtDHashMap.isSome_getKey?_eq_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
theorem Std.ExtDHashMap.mem_iff_isSome_getKey? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
@[simp]
theorem Std.ExtDHashMap.isSome_getKey?_iff_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
theorem Std.ExtDHashMap.mem_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} (h : m.getKey? k = some k') :
k' m
theorem Std.ExtDHashMap.getKey?_eq_none_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
theorem Std.ExtDHashMap.getKey?_eq_none {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} :
¬a mm.getKey? a = none
theorem Std.ExtDHashMap.getKey?_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} :
(m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a
@[simp]
theorem Std.ExtDHashMap.getKey?_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
theorem Std.ExtDHashMap.getKey?_beq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} :
Option.all (fun (x : α) => x == k) (m.getKey? k) = true
theorem Std.ExtDHashMap.getKey?_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' : α} (h : (k == k') = true) :
m.getKey? k = m.getKey? k'
theorem Std.ExtDHashMap.getKey?_eq_some_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} (h : m.contains k = true) :
m.getKey? k = some k
theorem Std.ExtDHashMap.getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} (h : k m) :
m.getKey? k = some k
theorem Std.ExtDHashMap.getKey_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {h₁ : a m.insert k v} :
(m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a
@[simp]
theorem Std.ExtDHashMap.getKey_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insert k v).getKey k = k
@[simp]
theorem Std.ExtDHashMap.getKey_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {h' : a m.erase k} :
(m.erase k).getKey a h' = m.getKey a
theorem Std.ExtDHashMap.getKey?_eq_some_getKey {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} (h : a m) :
m.getKey? a = some (m.getKey a h)
theorem Std.ExtDHashMap.getKey_eq_get_getKey? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h : a m} :
m.getKey a h = (m.getKey? a).get
@[simp]
theorem Std.ExtDHashMap.get_getKey? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a : α} {h : (m.getKey? a).isSome = true} :
(m.getKey? a).get h = m.getKey a
theorem Std.ExtDHashMap.getKey_beq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} (h : k m) :
(m.getKey k h == k) = true
theorem Std.ExtDHashMap.getKey_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : (k₁ == k₂) = true) (h₁ : k₁ m) :
m.getKey k₁ h₁ = m.getKey k₂
theorem Std.ExtDHashMap.getKey_eq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} (h : k m) :
m.getKey k h = k
@[simp]
theorem Std.ExtDHashMap.getKey!_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
theorem Std.ExtDHashMap.getKey!_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β k} :
(m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a
@[simp]
theorem Std.ExtDHashMap.getKey!_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {b : β a} :
(m.insert a b).getKey! a = a
theorem Std.ExtDHashMap.getKey!_eq_default_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
theorem Std.ExtDHashMap.getKey!_eq_default {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
¬a mm.getKey! a = default
theorem Std.ExtDHashMap.getKey!_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} :
@[simp]
theorem Std.ExtDHashMap.getKey!_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} :
theorem Std.ExtDHashMap.getKey?_eq_some_getKey!_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.contains a = truem.getKey? a = some (m.getKey! a)
theorem Std.ExtDHashMap.getKey?_eq_some_getKey! {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
a mm.getKey? a = some (m.getKey! a)
theorem Std.ExtDHashMap.getKey!_eq_get!_getKey? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
m.getKey! a = (m.getKey? a).get!
theorem Std.ExtDHashMap.getKey_eq_getKey! {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} {h : a m} :
m.getKey a h = m.getKey! a
theorem Std.ExtDHashMap.getKey!_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} (h : (k == k') = true) :
m.getKey! k = m.getKey! k'
theorem Std.ExtDHashMap.getKey!_eq_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k : α} (h : m.contains k = true) :
m.getKey! k = k
theorem Std.ExtDHashMap.getKey!_eq_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k : α} (h : k m) :
m.getKey! k = k
@[simp]
theorem Std.ExtDHashMap.getKeyD_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
.getKeyD a fallback = fallback
theorem Std.ExtDHashMap.getKeyD_insert {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β k} :
(m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback
@[simp]
theorem Std.ExtDHashMap.getKeyD_insert_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k fallback : α} {v : β k} :
(m.insert k v).getKeyD k fallback = k
theorem Std.ExtDHashMap.getKeyD_eq_fallback_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.contains a = falsem.getKeyD a fallback = fallback
theorem Std.ExtDHashMap.getKeyD_eq_fallback {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
¬a mm.getKeyD a fallback = fallback
theorem Std.ExtDHashMap.getKeyD_erase {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
(m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback
@[simp]
theorem Std.ExtDHashMap.getKeyD_erase_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k fallback : α} :
(m.erase k).getKeyD k fallback = fallback
theorem Std.ExtDHashMap.getKey?_eq_some_getKeyD_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.contains a = truem.getKey? a = some (m.getKeyD a fallback)
theorem Std.ExtDHashMap.getKey?_eq_some_getKeyD {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
a mm.getKey? a = some (m.getKeyD a fallback)
theorem Std.ExtDHashMap.getKeyD_eq_getD_getKey? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} :
m.getKeyD a fallback = (m.getKey? a).getD fallback
theorem Std.ExtDHashMap.getKey_eq_getKeyD {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {a fallback : α} {h : a m} :
m.getKey a h = m.getKeyD a fallback
theorem Std.ExtDHashMap.getKey!_eq_getKeyD_default {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
theorem Std.ExtDHashMap.getKeyD_congr {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} (h : (k == k') = true) :
m.getKeyD k fallback = m.getKeyD k' fallback
theorem Std.ExtDHashMap.getKeyD_eq_of_contains {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k fallback : α} (h : m.contains k = true) :
m.getKeyD k fallback = k
theorem Std.ExtDHashMap.getKeyD_eq_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k fallback : α} (h : k m) :
m.getKeyD k fallback = k
@[simp]
theorem Std.ExtDHashMap.not_insertIfNew_eq_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
@[simp]
theorem Std.ExtDHashMap.contains_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a = (k == a || m.contains a)
@[simp]
theorem Std.ExtDHashMap.mem_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insertIfNew k v (k == a) = true a m
theorem Std.ExtDHashMap.contains_insertIfNew_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
theorem Std.ExtDHashMap.mem_insertIfNew_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
theorem Std.ExtDHashMap.contains_of_contains_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a = true(k == a) = falsem.contains a = true
theorem Std.ExtDHashMap.mem_of_mem_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
a m.insertIfNew k v(k == a) = falsea m
theorem Std.ExtDHashMap.contains_of_contains_insertIfNew' {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).contains a = true¬((k == a) = true m.contains k = false) → m.contains a = true

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

theorem Std.ExtDHashMap.mem_of_mem_insertIfNew' {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
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 get_insertIfNew.

theorem Std.ExtDHashMap.size_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insertIfNew k v).size = if k m then m.size else m.size + 1
theorem Std.ExtDHashMap.size_le_size_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
theorem Std.ExtDHashMap.size_insertIfNew_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
(m.insertIfNew k v).size m.size + 1
theorem Std.ExtDHashMap.get?_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} {v : β k} :
(m.insertIfNew k v).get? a = if h : (k == a) = true ¬k m then some (cast v) else m.get? a
theorem Std.ExtDHashMap.get_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} {v : β k} {h₁ : a m.insertIfNew k v} :
(m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true ¬k m then cast v else m.get a
theorem Std.ExtDHashMap.get!_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
(m.insertIfNew k v).get! a = if h : (k == a) = true ¬k m then cast v else m.get! a
theorem Std.ExtDHashMap.getD_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k a : α} {fallback : β a} {v : β k} :
(m.insertIfNew k v).getD a fallback = if h : (k == a) = true ¬k m then cast v else m.getD a fallback
theorem Std.ExtDHashMap.Const.get?_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
get? (m.insertIfNew k v) a = if (k == a) = true ¬k m then some v else get? m a
theorem Std.ExtDHashMap.Const.get_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁ : a m.insertIfNew k v} :
get (m.insertIfNew k v) a h₁ = if h₂ : (k == a) = true ¬k m then v else get m a
theorem Std.ExtDHashMap.Const.get!_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
get! (m.insertIfNew k v) a = if (k == a) = true ¬k m then v else get! m a
theorem Std.ExtDHashMap.Const.getD_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
getD (m.insertIfNew k v) a fallback = if (k == a) = true ¬k m then v else getD m a fallback
theorem Std.ExtDHashMap.getKey?_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
(m.insertIfNew k v).getKey? a = if (k == a) = true ¬k m then some k else m.getKey? a
theorem Std.ExtDHashMap.getKey_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} {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
theorem Std.ExtDHashMap.getKey!_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β k} :
(m.insertIfNew k v).getKey! a = if (k == a) = true ¬k m then k else m.getKey! a
theorem Std.ExtDHashMap.getKeyD_insertIfNew {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β k} :
(m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ¬k m then k else m.getKeyD a fallback
@[simp]
theorem Std.ExtDHashMap.getThenInsertIfNew?_fst {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {v : β k} :
@[simp]
theorem Std.ExtDHashMap.getThenInsertIfNew?_snd {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {v : β k} :
@[simp]
theorem Std.ExtDHashMap.Const.getThenInsertIfNew?_fst {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@[simp]
theorem Std.ExtDHashMap.Const.getThenInsertIfNew?_snd {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
@[simp]
theorem Std.ExtDHashMap.insertMany_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] :
@[simp]
theorem Std.ExtDHashMap.insertMany_list_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
theorem Std.ExtDHashMap.insertMany_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {p : (a : α) × β a} :
m.insertMany (p :: l) = (m.insert p.fst p.snd).insertMany l
theorem Std.ExtDHashMap.insertMany_append {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l₁ l₂ : List ((a : α) × β a)} :
m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
theorem Std.ExtDHashMap.insertMany_ind {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α] {motive : ExtDHashMap α βProp} (m : ExtDHashMap α β) (l : ρ) (init : motive m) (insert : ∀ (m : ExtDHashMap α β) (a : α) (b : β a), motive mmotive (m.insert a b)) :
motive (m.insertMany l)
@[simp]
theorem Std.ExtDHashMap.contains_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} :
@[simp]
theorem Std.ExtDHashMap.mem_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} :
theorem Std.ExtDHashMap.mem_of_mem_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} (mem : k m.insertMany l) (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
k m
theorem Std.ExtDHashMap.mem_insertMany_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α] {l : ρ} {k : α} (h' : k m) :
theorem Std.ExtDHashMap.get?_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(m.insertMany l).get? k = m.get? k
theorem Std.ExtDHashMap.get?_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k, v l) :
(m.insertMany l).get? k' = some (cast v)
theorem Std.ExtDHashMap.get_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h : k m.insertMany l} :
(m.insertMany l).get k h = m.get k
theorem Std.ExtDHashMap.get_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k, v l) {h : k' m.insertMany l} :
(m.insertMany l).get k' h = cast v
theorem Std.ExtDHashMap.get!_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(m.insertMany l).get! k = m.get! k
theorem Std.ExtDHashMap.get!_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k, v l) :
(m.insertMany l).get! k' = cast v
theorem Std.ExtDHashMap.getD_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(m.insertMany l).getD k fallback = m.getD k fallback
theorem Std.ExtDHashMap.getD_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k, v l) :
(m.insertMany l).getD k' fallback = cast v
theorem Std.ExtDHashMap.getKey?_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.ExtDHashMap.getKey?_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k List.map Sigma.fst l) :
theorem Std.ExtDHashMap.getKey_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h : k m.insertMany l} :
(m.insertMany l).getKey k h = m.getKey k
theorem Std.ExtDHashMap.getKey_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k List.map Sigma.fst l) {h : k' m.insertMany l} :
(m.insertMany l).getKey k' h = k
theorem Std.ExtDHashMap.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.ExtDHashMap.getKey!_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k List.map Sigma.fst l) :
(m.insertMany l).getKey! k' = k
theorem Std.ExtDHashMap.getKeyD_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k fallback : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(m.insertMany l).getKeyD k fallback = m.getKeyD k fallback
theorem Std.ExtDHashMap.getKeyD_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k List.map Sigma.fst l) :
(m.insertMany l).getKeyD k' fallback = k
theorem Std.ExtDHashMap.size_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) :
(∀ (a : α), a m(List.map Sigma.fst l).contains a = false)(m.insertMany l).size = m.size + l.length
theorem Std.ExtDHashMap.size_le_size_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
theorem Std.ExtDHashMap.size_le_size_insertMany {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α] {l : ρ} :
theorem Std.ExtDHashMap.size_insertMany_list_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
@[simp]
theorem Std.ExtDHashMap.insertMany_list_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
theorem Std.ExtDHashMap.eq_empty_of_insertMany_eq_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α] {l : ρ} :
m.insertMany l = m =
@[simp]
theorem Std.ExtDHashMap.Const.insertMany_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] :
@[simp]
theorem Std.ExtDHashMap.Const.insertMany_list_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
theorem Std.ExtDHashMap.Const.insertMany_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {p : α × β} :
insertMany m (p :: l) = insertMany (m.insert p.fst p.snd) l
theorem Std.ExtDHashMap.Const.insertMany_append {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l₁ l₂ : List (α × β)} :
insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂
theorem Std.ExtDHashMap.Const.insertMany_ind {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {ρ : Type w} [ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {motive : (ExtDHashMap α fun (x : α) => β)Prop} (m : ExtDHashMap α fun (x : α) => β) (l : ρ) (init : motive m) (insert : ∀ (m : ExtDHashMap α fun (x : α) => β) (a : α) (b : β), motive mmotive (m.insert a b)) :
motive (insertMany m l)
@[simp]
theorem Std.ExtDHashMap.Const.contains_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
@[simp]
theorem Std.ExtDHashMap.Const.mem_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
theorem Std.ExtDHashMap.Const.mem_of_mem_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (mem : k insertMany m l) (contains_eq_false : (List.map Prod.fst l).contains k = false) :
k m
theorem Std.ExtDHashMap.Const.mem_insertMany_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} {ρ : Type w} [ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ} {k : α} (h' : k m) :
theorem Std.ExtDHashMap.Const.getKey?_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.ExtDHashMap.Const.getKey?_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [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) :
theorem Std.ExtDHashMap.Const.getKey_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h : k insertMany m l} :
(insertMany m l).getKey k h = m.getKey k
theorem Std.ExtDHashMap.Const.getKey_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [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' insertMany m l} :
(insertMany m l).getKey k' h = k
theorem Std.ExtDHashMap.Const.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.ExtDHashMap.Const.getKey!_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k List.map Prod.fst l) :
(insertMany m l).getKey! k' = k
theorem Std.ExtDHashMap.Const.getKeyD_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(insertMany m l).getKeyD k fallback = m.getKeyD k fallback
theorem Std.ExtDHashMap.Const.getKeyD_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k List.map Prod.fst l) :
(insertMany m l).getKeyD k' fallback = k
theorem Std.ExtDHashMap.Const.size_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [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)(insertMany m l).size = m.size + l.length
theorem Std.ExtDHashMap.Const.size_le_size_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
theorem Std.ExtDHashMap.Const.size_le_size_insertMany {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} {ρ : Type w} [ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ} :
theorem Std.ExtDHashMap.Const.size_insertMany_list_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
@[simp]
theorem Std.ExtDHashMap.Const.insertMany_list_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
theorem Std.ExtDHashMap.Const.eq_empty_of_insertMany_eq_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} {ρ : Type w} [ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ} :
insertMany m l = m =
theorem Std.ExtDHashMap.Const.get?_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
get? (insertMany m l) k = get? m k
theorem Std.ExtDHashMap.Const.get?_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [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) :
get? (insertMany m l) k' = some v
theorem Std.ExtDHashMap.Const.get?_insertMany_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
get? (insertMany m l) k = (List.findSomeRev? (fun (x : α × β) => match x with | (a, b) => if (a == k) = true then some b else none) l).or (get? m k)
theorem Std.ExtDHashMap.Const.get_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h : k insertMany m l} :
get (insertMany m l) k h = get m k
theorem Std.ExtDHashMap.Const.get_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [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' insertMany m l} :
get (insertMany m l) k' h = v
theorem Std.ExtDHashMap.Const.get!_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
get! (insertMany m l) k = get! m k
theorem Std.ExtDHashMap.Const.get!_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [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) :
get! (insertMany m l) k' = v
theorem Std.ExtDHashMap.Const.getD_insertMany_list_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
getD (insertMany m l) k fallback = getD m k fallback
theorem Std.ExtDHashMap.Const.getD_insertMany_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [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) :
getD (insertMany m l) k' fallback = v
@[simp]
theorem Std.ExtDHashMap.Const.insertManyIfNewUnit_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] :
@[simp]
theorem Std.ExtDHashMap.Const.insertManyIfNewUnit_list_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {k : α} :
theorem Std.ExtDHashMap.Const.insertManyIfNewUnit_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
theorem Std.ExtDHashMap.Const.insertManyIfNewUnit_ind {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {ρ : Type w} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {motive : (ExtDHashMap α fun (x : α) => Unit)Prop} (m : ExtDHashMap α fun (x : α) => Unit) (l : ρ) (init : motive m) (insert : ∀ (m : ExtDHashMap α fun (x : α) => Unit) (a : α), motive mmotive (m.insertIfNew a ())) :
motive (insertManyIfNewUnit m l)
@[simp]
theorem Std.ExtDHashMap.Const.contains_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
@[simp]
theorem Std.ExtDHashMap.Const.mem_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
theorem Std.ExtDHashMap.Const.mem_of_mem_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
theorem Std.ExtDHashMap.Const.mem_insertManyIfNewUnit_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} {ρ : Type w} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {l : ρ} {k : α} (h : k m) :
theorem Std.ExtDHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (not_mem : ¬k m) (contains_eq_false : l.contains k = false) :
theorem Std.ExtDHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => 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) :
theorem Std.ExtDHashMap.Const.getKey?_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (h' : k m) :
theorem Std.ExtDHashMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => 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' insertManyIfNewUnit m l} :
theorem Std.ExtDHashMap.Const.getKey_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (mem : k m) {h : k insertManyIfNewUnit m l} :
theorem Std.ExtDHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (not_mem : ¬k m) (contains_eq_false : l.contains k = false) :
theorem Std.ExtDHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => 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) :
theorem Std.ExtDHashMap.Const.getKey!_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (mem : k m) :
theorem Std.ExtDHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (not_mem : ¬k m) (contains_eq_false : l.contains k = false) :
(insertManyIfNewUnit m l).getKeyD k fallback = fallback
theorem Std.ExtDHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => 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) :
(insertManyIfNewUnit m l).getKeyD k' fallback = k
theorem Std.ExtDHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (mem : k m) :
(insertManyIfNewUnit m l).getKeyD k fallback = m.getKeyD k fallback
theorem Std.ExtDHashMap.Const.size_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :
(∀ (a : α), a ml.contains a = false)(insertManyIfNewUnit m l).size = m.size + l.length
theorem Std.ExtDHashMap.Const.size_le_size_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} :
theorem Std.ExtDHashMap.Const.size_le_size_insertManyIfNewUnit {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} {ρ : Type w} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {l : ρ} :
theorem Std.ExtDHashMap.Const.size_insertManyIfNewUnit_list_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} :
@[simp]
theorem Std.ExtDHashMap.Const.insertManyIfNewUnit_list_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} :
theorem Std.ExtDHashMap.Const.eq_empty_of_insertManyIfNewUnit_eq_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} {ρ : Type w} [ForIn Id ρ α] [EquivBEq α] [LawfulHashable α] {l : ρ} :
theorem Std.ExtDHashMap.Const.get?_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
theorem Std.ExtDHashMap.Const.get_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} {h : k insertManyIfNewUnit m l} :
theorem Std.ExtDHashMap.Const.get!_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
theorem Std.ExtDHashMap.Const.getD_insertManyIfNewUnit_list {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : ExtDHashMap α fun (x : α) => Unit} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} {fallback : Unit} :
getD (insertManyIfNewUnit m l) k fallback = ()
@[simp]
theorem Std.ExtDHashMap.ofList_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] :
@[simp]
theorem Std.ExtDHashMap.ofList_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
theorem Std.ExtDHashMap.ofList_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} {tl : List ((a : α) × β a)} :
ofList (k, v :: tl) = (.insert k v).insertMany tl
@[simp]
theorem Std.ExtDHashMap.contains_ofList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} :
@[simp]
theorem Std.ExtDHashMap.mem_ofList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} :
theorem Std.ExtDHashMap.get?_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.ExtDHashMap.get?_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k, v l) :
(ofList l).get? k' = some (cast v)
theorem Std.ExtDHashMap.get_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k, v l) {h : k' ofList l} :
(ofList l).get k' h = cast v
theorem Std.ExtDHashMap.get!_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.ExtDHashMap.get!_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k, v l) :
(ofList l).get! k' = cast v
theorem Std.ExtDHashMap.getD_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(ofList l).getD k fallback = fallback
theorem Std.ExtDHashMap.getD_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k, v l) :
(ofList l).getD k' fallback = cast v
theorem Std.ExtDHashMap.getKey?_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.ExtDHashMap.getKey?_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k List.map Sigma.fst l) :
(ofList l).getKey? k' = some k
theorem Std.ExtDHashMap.getKey_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k List.map Sigma.fst l) {h : k' ofList l} :
(ofList l).getKey k' h = k
theorem Std.ExtDHashMap.getKey!_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.ExtDHashMap.getKey!_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k List.map Sigma.fst l) :
(ofList l).getKey! k' = k
theorem Std.ExtDHashMap.getKeyD_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k fallback : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(ofList l).getKeyD k fallback = fallback
theorem Std.ExtDHashMap.getKeyD_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) (mem : k List.map Sigma.fst l) :
(ofList l).getKeyD k' fallback = k
theorem Std.ExtDHashMap.size_ofList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l) :
theorem Std.ExtDHashMap.size_ofList_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
@[simp]
theorem Std.ExtDHashMap.ofList_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
@[simp]
theorem Std.ExtDHashMap.Const.ofList_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] :
@[simp]
theorem Std.ExtDHashMap.Const.ofList_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
theorem Std.ExtDHashMap.Const.ofList_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} {tl : List (α × β)} :
ofList ((k, v) :: tl) = insertMany (.insert k v) tl
@[simp]
theorem Std.ExtDHashMap.Const.contains_ofList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
@[simp]
theorem Std.ExtDHashMap.Const.mem_ofList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
theorem Std.ExtDHashMap.Const.get?_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.ExtDHashMap.Const.get?_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [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) :
get? (ofList l) k' = some v
theorem Std.ExtDHashMap.Const.get_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [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} :
get (ofList l) k' h = v
theorem Std.ExtDHashMap.Const.get!_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} [Inhabited β] (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.ExtDHashMap.Const.get!_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [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) :
get! (ofList l) k' = v
theorem Std.ExtDHashMap.Const.getD_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
getD (ofList l) k fallback = fallback
theorem Std.ExtDHashMap.Const.getD_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [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) :
getD (ofList l) k' fallback = v
theorem Std.ExtDHashMap.Const.getKey?_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.ExtDHashMap.Const.getKey?_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k List.map Prod.fst l) :
(ofList l).getKey? k' = some k
theorem Std.ExtDHashMap.Const.getKey_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k List.map Prod.fst l) {h : k' ofList l} :
(ofList l).getKey k' h = k
theorem Std.ExtDHashMap.Const.getKey!_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.ExtDHashMap.Const.getKey!_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k List.map Prod.fst l) :
(ofList l).getKey! k' = k
theorem Std.ExtDHashMap.Const.getKeyD_ofList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(ofList l).getKeyD k fallback = fallback
theorem Std.ExtDHashMap.Const.getKeyD_ofList_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) (mem : k List.map Prod.fst l) :
(ofList l).getKeyD k' fallback = k
theorem Std.ExtDHashMap.Const.size_ofList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l) :
theorem Std.ExtDHashMap.Const.size_ofList_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
@[simp]
theorem Std.ExtDHashMap.Const.ofList_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
@[simp]
theorem Std.ExtDHashMap.Const.unitOfList_nil {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] :
@[simp]
theorem Std.ExtDHashMap.Const.unitOfList_singleton {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {k : α} :
theorem Std.ExtDHashMap.Const.unitOfList_cons {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} :
@[simp]
theorem Std.ExtDHashMap.Const.contains_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
@[simp]
theorem Std.ExtDHashMap.Const.mem_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
theorem Std.ExtDHashMap.Const.getKey?_unitOfList_of_contains_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
theorem Std.ExtDHashMap.Const.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) :
theorem Std.ExtDHashMap.Const.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
theorem Std.ExtDHashMap.Const.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) :
theorem Std.ExtDHashMap.Const.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) :
theorem Std.ExtDHashMap.Const.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
theorem Std.ExtDHashMap.Const.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
theorem Std.ExtDHashMap.Const.size_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l) :
theorem Std.ExtDHashMap.Const.size_unitOfList_le {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} :
@[simp]
theorem Std.ExtDHashMap.Const.unitOfList_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} :
@[simp]
theorem Std.ExtDHashMap.Const.get?_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
@[simp]
theorem Std.ExtDHashMap.Const.get_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} {h : k unitOfList l} :
get (unitOfList l) k h = ()
@[simp]
theorem Std.ExtDHashMap.Const.get!_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
@[simp]
theorem Std.ExtDHashMap.Const.getD_unitOfList {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} {fallback : Unit} :
getD (unitOfList l) k fallback = ()
theorem Std.ExtDHashMap.alter_eq_empty_iff_erase_eq_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} :
m.alter k f = m.erase k = f (m.get? k) = none
@[simp]
theorem Std.ExtDHashMap.alter_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} :
m.alter k f = (m = m.size = 1 k m) f (m.get? k) = none
theorem Std.ExtDHashMap.contains_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} :
(m.alter k f).contains k' = if (k == k') = true then (f (m.get? k)).isSome else m.contains k'
theorem Std.ExtDHashMap.mem_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} :
k' m.alter k f if (k == k') = true then (f (m.get? k)).isSome = true else k' m
theorem Std.ExtDHashMap.mem_alter_of_beq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} (h : (k == k') = true) :
k' m.alter k f (f (m.get? k)).isSome = true
@[simp]
theorem Std.ExtDHashMap.contains_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} :
(m.alter k f).contains k = (f (m.get? k)).isSome
@[simp]
theorem Std.ExtDHashMap.mem_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} :
k m.alter k f (f (m.get? k)).isSome = true
theorem Std.ExtDHashMap.contains_alter_of_beq_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} (h : (k == k') = false) :
(m.alter k f).contains k' = m.contains k'
theorem Std.ExtDHashMap.mem_alter_of_beq_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} (h : (k == k') = false) :
k' m.alter k f k' m
theorem Std.ExtDHashMap.size_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} :
(m.alter k f).size = if k m (f (m.get? k)).isNone = true then m.size - 1 else if ¬k m (f (m.get? k)).isSome = true then m.size + 1 else m.size
theorem Std.ExtDHashMap.size_alter_eq_add_one {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} (h : ¬k m) (h' : (f (m.get? k)).isSome = true) :
(m.alter k f).size = m.size + 1
theorem Std.ExtDHashMap.size_alter_eq_sub_one {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} (h : k m) (h' : (f (m.get? k)).isNone = true) :
(m.alter k f).size = m.size - 1
theorem Std.ExtDHashMap.size_alter_eq_self_of_not_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} (h : ¬k m) (h' : (f (m.get? k)).isNone = true) :
(m.alter k f).size = m.size
theorem Std.ExtDHashMap.size_alter_eq_self_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} (h : k m) (h' : (f (m.get? k)).isSome = true) :
(m.alter k f).size = m.size
theorem Std.ExtDHashMap.size_alter_le_size {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} :
(m.alter k f).size m.size + 1
theorem Std.ExtDHashMap.size_le_size_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} :
m.size - 1 (m.alter k f).size
theorem Std.ExtDHashMap.get?_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} :
(m.alter k f).get? k' = if h : (k == k') = true then cast (f (m.get? k)) else m.get? k'
@[simp]
theorem Std.ExtDHashMap.get?_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} :
(m.alter k f).get? k = f (m.get? k)
theorem Std.ExtDHashMap.get_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} {h : k' m.alter k f} :
(m.alter k f).get k' h = if heq : (k == k') = true then cast ((f (m.get? k)).get ) else m.get k'
@[simp]
theorem Std.ExtDHashMap.get_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} {h : k m.alter k f} :
(m.alter k f).get k h = (f (m.get? k)).get
theorem Std.ExtDHashMap.get!_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : Option (β k)Option (β k)} :
(m.alter k f).get! k' = if heq : (k == k') = true then (Option.map (cast ) (f (m.get? k))).get! else m.get! k'
@[simp]
theorem Std.ExtDHashMap.get!_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} [Inhabited (β k)] {f : Option (β k)Option (β k)} :
(m.alter k f).get! k = (f (m.get? k)).get!
theorem Std.ExtDHashMap.getD_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k)Option (β k)} :
(m.alter k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ) (f (m.get? k))).getD fallback else m.getD k' fallback
@[simp]
theorem Std.ExtDHashMap.getD_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {fallback : β k} {f : Option (β k)Option (β k)} :
(m.alter k f).getD k fallback = (f (m.get? k)).getD fallback
theorem Std.ExtDHashMap.getKey?_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : Option (β k)Option (β k)} :
(m.alter k f).getKey? k' = if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k'
theorem Std.ExtDHashMap.getKey?_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : Option (β k)Option (β k)} :
(m.alter k f).getKey? k = if (f (m.get? k)).isSome = true then some k else none
theorem Std.ExtDHashMap.getKey!_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k)Option (β k)} :
(m.alter k f).getKey! k' = if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else m.getKey! k'
theorem Std.ExtDHashMap.getKey!_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k)Option (β k)} :
(m.alter k f).getKey! k = if (f (m.get? k)).isSome = true then k else default
theorem Std.ExtDHashMap.getKey_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k)Option (β k)} {h : k' m.alter k f} :
(m.alter k f).getKey k' h = if heq : (k == k') = true then k else m.getKey k'
@[simp]
theorem Std.ExtDHashMap.getKey_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k)Option (β k)} {h : k m.alter k f} :
(m.alter k f).getKey k h = k
theorem Std.ExtDHashMap.getKeyD_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' fallback : α} {f : Option (β k)Option (β k)} :
(m.alter k f).getKeyD k' fallback = if (k == k') = true then if (f (m.get? k)).isSome = true then k else fallback else m.getKeyD k' fallback
@[simp]
theorem Std.ExtDHashMap.getKeyD_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k fallback : α} {f : Option (β k)Option (β k)} :
(m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome = true then k else fallback
theorem Std.ExtDHashMap.Const.alter_eq_empty_iff_erase_eq_empty {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} :
alter m k f = m.erase k = f (get? m k) = none
@[simp]
theorem Std.ExtDHashMap.Const.alter_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} :
alter m k f = (m = m.size = 1 k m) f (get? m k) = none
theorem Std.ExtDHashMap.Const.contains_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option βOption β} :
(alter m k f).contains k' = if (k == k') = true then (f (get? m k)).isSome else m.contains k'
theorem Std.ExtDHashMap.Const.mem_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option βOption β} :
k' alter m k f if (k == k') = true then (f (get? m k)).isSome = true else k' m
theorem Std.ExtDHashMap.Const.mem_alter_of_beq {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option βOption β} (h : (k == k') = true) :
k' alter m k f (f (get? m k)).isSome = true
@[simp]
theorem Std.ExtDHashMap.Const.contains_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} :
(alter m k f).contains k = (f (get? m k)).isSome
@[simp]
theorem Std.ExtDHashMap.Const.mem_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} :
k alter m k f (f (get? m k)).isSome = true
theorem Std.ExtDHashMap.Const.contains_alter_of_beq_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option βOption β} (h : (k == k') = false) :
(alter m k f).contains k' = m.contains k'
theorem Std.ExtDHashMap.Const.mem_alter_of_beq_eq_false {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option βOption β} (h : (k == k') = false) :
k' alter m k f k' m
theorem Std.ExtDHashMap.Const.size_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} :
(alter m k f).size = if k m (f (get? m k)).isNone = true then m.size - 1 else if ¬k m (f (get? m k)).isSome = true then m.size + 1 else m.size
theorem Std.ExtDHashMap.Const.size_alter_eq_add_one {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} (h : ¬k m) (h' : (f (get? m k)).isSome = true) :
(alter m k f).size = m.size + 1
theorem Std.ExtDHashMap.Const.size_alter_eq_sub_one {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} (h : k m) (h' : (f (get? m k)).isNone = true) :
(alter m k f).size = m.size - 1
theorem Std.ExtDHashMap.Const.size_alter_eq_self_of_not_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} (h : ¬k m) (h' : (f (get? m k)).isNone = true) :
(alter m k f).size = m.size
theorem Std.ExtDHashMap.Const.size_alter_eq_self_of_mem {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} (h : k m) (h' : (f (get? m k)).isSome = true) :
(alter m k f).size = m.size
theorem Std.ExtDHashMap.Const.size_alter_le_size {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} :
(alter m k f).size m.size + 1
theorem Std.ExtDHashMap.Const.size_le_size_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} :
m.size - 1 (alter m k f).size
theorem Std.ExtDHashMap.Const.get?_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option βOption β} :
get? (alter m k f) k' = if (k == k') = true then f (get? m k) else get? m k'
@[simp]
theorem Std.ExtDHashMap.Const.get?_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} :
get? (alter m k f) k = f (get? m k)
theorem Std.ExtDHashMap.Const.get_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option βOption β} {h : k' alter m k f} :
get (alter m k f) k' h = if heq : (k == k') = true then (f (get? m k)).get else get m k'
@[simp]
theorem Std.ExtDHashMap.Const.get_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} {h : k alter m k f} :
get (alter m k f) k h = (f (get? m k)).get
theorem Std.ExtDHashMap.Const.get!_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : Option βOption β} :
get! (alter m k f) k' = if (k == k') = true then (f (get? m k)).get! else get! m k'
@[simp]
theorem Std.ExtDHashMap.Const.get!_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : Option βOption β} :
get! (alter m k f) k = (f (get? m k)).get!
theorem Std.ExtDHashMap.Const.getD_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : Option βOption β} :
getD (alter m k f) k' fallback = if (k == k') = true then (f (get? m k)).getD fallback else getD m k' fallback
@[simp]
theorem Std.ExtDHashMap.Const.getD_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : Option βOption β} :
getD (alter m k f) k fallback = (f (get? m k)).getD fallback
theorem Std.ExtDHashMap.Const.getKey?_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option βOption β} :
(alter m k f).getKey? k' = if (k == k') = true then if (f (get? m k)).isSome = true then some k else none else m.getKey? k'
theorem Std.ExtDHashMap.Const.getKey?_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : Option βOption β} :
(alter m k f).getKey? k = if (f (get? m k)).isSome = true then some k else none
theorem Std.ExtDHashMap.Const.getKey!_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : Option βOption β} :
(alter m k f).getKey! k' = if (k == k') = true then if (f (get? m k)).isSome = true then k else default else m.getKey! k'
theorem Std.ExtDHashMap.Const.getKey!_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : Option βOption β} :
(alter m k f).getKey! k = if (f (get? m k)).isSome = true then k else default
theorem Std.ExtDHashMap.Const.getKey_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : Option βOption β} {h : k' alter m k f} :
(alter m k f).getKey k' h = if heq : (k == k') = true then k else m.getKey k'
@[simp]
theorem Std.ExtDHashMap.Const.getKey_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : Option βOption β} {h : k alter m k f} :
(alter m k f).getKey k h = k
theorem Std.ExtDHashMap.Const.getKeyD_alter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option βOption β} :
(alter m k f).getKeyD k' fallback = if (k == k') = true then if (f (get? m k)).isSome = true then k else fallback else m.getKeyD k' fallback
theorem Std.ExtDHashMap.Const.getKeyD_alter_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : Option βOption β} :
(alter m k f).getKeyD k fallback = if (f (get? m k)).isSome = true then k else fallback
@[simp]
theorem Std.ExtDHashMap.modify_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : β kβ k} :
m.modify k f = m =
@[simp]
theorem Std.ExtDHashMap.contains_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : β kβ k} :
(m.modify k f).contains k' = m.contains k'
@[simp]
theorem Std.ExtDHashMap.mem_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : β kβ k} :
k' m.modify k f k' m
@[simp]
theorem Std.ExtDHashMap.size_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : β kβ k} :
(m.modify k f).size = m.size
theorem Std.ExtDHashMap.get?_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : β kβ k} :
(m.modify k f).get? k' = if h : (k == k') = true then cast (Option.map f (m.get? k)) else m.get? k'
@[simp]
theorem Std.ExtDHashMap.get?_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : β kβ k} :
(m.modify k f).get? k = Option.map f (m.get? k)
theorem Std.ExtDHashMap.get_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : β kβ k} (h : k' m.modify k f) :
(m.modify k f).get k' h = if heq : (k == k') = true then cast (f (m.get k )) else m.get k'
@[simp]
theorem Std.ExtDHashMap.get_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : β kβ k} {h : k m.modify k f} :
(m.modify k f).get k h = f (m.get k )
theorem Std.ExtDHashMap.get!_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β kβ k} :
(m.modify k f).get! k' = if heq : (k == k') = true then (Option.map (cast ) (Option.map f (m.get? k))).get! else m.get! k'
@[simp]
theorem Std.ExtDHashMap.get!_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} [Inhabited (β k)] {f : β kβ k} :
(m.modify k f).get! k = (Option.map f (m.get? k)).get!
theorem Std.ExtDHashMap.getD_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β kβ k} :
(m.modify k f).getD k' fallback = if heq : (k == k') = true then (Option.map (cast ) (Option.map f (m.get? k))).getD fallback else m.getD k' fallback
@[simp]
theorem Std.ExtDHashMap.getD_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {fallback : β k} {f : β kβ k} :
(m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback
theorem Std.ExtDHashMap.getKey?_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' : α} {f : β kβ k} :
(m.modify k f).getKey? k' = if (k == k') = true then if k m then some k else none else m.getKey? k'
theorem Std.ExtDHashMap.getKey?_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k : α} {f : β kβ k} :
(m.modify k f).getKey? k = if k m then some k else none
theorem Std.ExtDHashMap.getKey!_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k k' : α} {f : β kβ k} :
(m.modify k f).getKey! k' = if (k == k') = true then if k m then k else default else m.getKey! k'
theorem Std.ExtDHashMap.getKey!_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k : α} {f : β kβ k} :
(m.modify k f).getKey! k = if k m then k else default
theorem Std.ExtDHashMap.getKey_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k k' : α} {f : β kβ k} {h : k' m.modify k f} :
(m.modify k f).getKey k' h = if (k == k') = true then k else m.getKey k'
@[simp]
theorem Std.ExtDHashMap.getKey_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k : α} {f : β kβ k} {h : k m.modify k f} :
(m.modify k f).getKey k h = k
theorem Std.ExtDHashMap.getKeyD_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {k k' fallback : α} {f : β kβ k} :
(m.modify k f).getKeyD k' fallback = if (k == k') = true then if k m then k else fallback else m.getKeyD k' fallback
theorem Std.ExtDHashMap.getKeyD_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β kβ k} :
(m.modify k f).getKeyD k fallback = if k m then k else fallback
@[simp]
theorem Std.ExtDHashMap.Const.modify_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : ββ} :
modify m k f = m =
@[simp]
theorem Std.ExtDHashMap.Const.contains_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : ββ} :
(modify m k f).contains k' = m.contains k'
@[simp]
theorem Std.ExtDHashMap.Const.mem_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : ββ} :
k' modify m k f k' m
@[simp]
theorem Std.ExtDHashMap.Const.size_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : ββ} :
(modify m k f).size = m.size
theorem Std.ExtDHashMap.Const.get?_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : ββ} :
get? (modify m k f) k' = if (k == k') = true then Option.map f (get? m k) else get? m k'
@[simp]
theorem Std.ExtDHashMap.Const.get?_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : ββ} :
get? (modify m k f) k = Option.map f (get? m k)
theorem Std.ExtDHashMap.Const.get_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : ββ} {h : k' modify m k f} :
get (modify m k f) k' h = if heq : (k == k') = true then f (get m k ) else get m k'
@[simp]
theorem Std.ExtDHashMap.Const.get_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : ββ} {h : k modify m k f} :
get (modify m k f) k h = f (get m k )
theorem Std.ExtDHashMap.Const.get!_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : ββ} :
get! (modify m k f) k' = if (k == k') = true then (Option.map f (get? m k)).get! else get! m k'
@[simp]
theorem Std.ExtDHashMap.Const.get!_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : ββ} :
get! (modify m k f) k = (Option.map f (get? m k)).get!
theorem Std.ExtDHashMap.Const.getD_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : ββ} :
getD (modify m k f) k' fallback = if (k == k') = true then (Option.map f (get? m k)).getD fallback else getD m k' fallback
@[simp]
theorem Std.ExtDHashMap.Const.getD_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : ββ} :
getD (modify m k f) k fallback = (Option.map f (get? m k)).getD fallback
theorem Std.ExtDHashMap.Const.getKey?_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' : α} {f : ββ} :
(modify m k f).getKey? k' = if (k == k') = true then if k m then some k else none else m.getKey? k'
theorem Std.ExtDHashMap.Const.getKey?_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k : α} {f : ββ} :
(modify m k f).getKey? k = if k m then some k else none
theorem Std.ExtDHashMap.Const.getKey!_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : ββ} :
(modify m k f).getKey! k' = if (k == k') = true then if k m then k else default else m.getKey! k'
theorem Std.ExtDHashMap.Const.getKey!_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : ββ} :
(modify m k f).getKey! k = if k m then k else default
theorem Std.ExtDHashMap.Const.getKey_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : ββ} {h : k' modify m k f} :
(modify m k f).getKey k' h = if (k == k') = true then k else m.getKey k'
@[simp]
theorem Std.ExtDHashMap.Const.getKey_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : ββ} {h : k modify m k f} :
(modify m k f).getKey k h = k
theorem Std.ExtDHashMap.Const.getKeyD_modify {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : ββ} :
(modify m k f).getKeyD k' fallback = if (k == k') = true then if k m then k else fallback else m.getKeyD k' fallback
theorem Std.ExtDHashMap.Const.getKeyD_modify_self {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : ββ} :
(modify m k f).getKeyD k fallback = if k m then k else fallback
theorem Std.ExtDHashMap.ext_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {m₁ m₂ : ExtDHashMap α β} (h : ∀ (k : α), m₁.get? k = m₂.get? k) :
m₁ = m₂
theorem Std.ExtDHashMap.ext_get?_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} [LawfulBEq α] {m₁ m₂ : ExtDHashMap α β} :
m₁ = m₂ ∀ (k : α), m₁.get? k = m₂.get? k
theorem Std.ExtDHashMap.Const.ext_getKey_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (hk : ∀ (k : α) (hk : k m₁) (hk' : k m₂), m₁.getKey k hk = m₂.getKey k hk') (hv : ∀ (k : α), get? m₁ k = get? m₂ k) :
m₁ = m₂
theorem Std.ExtDHashMap.Const.ext_get? {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m₁ m₂ : ExtDHashMap α fun (x : α) => β} [LawfulBEq α] (h : ∀ (k : α), get? m₁ k = get? m₂ k) :
m₁ = m₂
theorem Std.ExtDHashMap.Const.ext_getKey?_unit {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : ExtDHashMap α fun (x : α) => Unit} (h : ∀ (k : α), m₁.getKey? k = m₂.getKey? k) :
m₁ = m₂
theorem Std.ExtDHashMap.Const.ext_contains_unit {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {m₁ m₂ : ExtDHashMap α fun (x : α) => Unit} (h : ∀ (k : α), m₁.contains k = m₂.contains k) :
m₁ = m₂
theorem Std.ExtDHashMap.Const.ext_mem_unit {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α] {m₁ m₂ : ExtDHashMap α fun (x : α) => Unit} (h : ∀ (k : α), k m₁ k m₂) :
m₁ = m₂
theorem Std.ExtDHashMap.filterMap_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} :
filterMap f m = ∀ (k : α) (h : k m), f k (m.get k h) = none
theorem Std.ExtDHashMap.contains_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} {k : α} :
(filterMap f m).contains k = Option.any (fun (x : β k) => (f k x).isSome) (m.get? k)
theorem Std.ExtDHashMap.mem_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} {k : α} :
k filterMap f m (h : k m), (f k (m.get k h)).isSome = true
theorem Std.ExtDHashMap.contains_of_contains_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aOption (γ a)} {k : α} :
theorem Std.ExtDHashMap.mem_of_mem_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aOption (γ a)} {k : α} :
k filterMap f mk m
theorem Std.ExtDHashMap.size_filterMap_le_size {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aOption (γ a)} :
theorem Std.ExtDHashMap.size_filterMap_eq_size_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} :
(filterMap f m).size = m.size ∀ (a : α) (h : a m), (f a (m.get a h)).isSome = true
@[simp]
theorem Std.ExtDHashMap.get?_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} {k : α} :
(filterMap f m).get? k = (m.get? k).bind (f k)
theorem Std.ExtDHashMap.isSome_apply_of_mem_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} {k : α} (h' : k filterMap f m) :
(f k (m.get k )).isSome = true
@[simp]
theorem Std.ExtDHashMap.get_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} {k : α} {h' : k filterMap f m} :
(filterMap f m).get k h' = (f k (m.get k )).get
theorem Std.ExtDHashMap.get!_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} {k : α} [Inhabited (γ k)] :
(filterMap f m).get! k = ((m.get? k).bind (f k)).get!
theorem Std.ExtDHashMap.getD_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} {k : α} {fallback : γ k} :
(filterMap f m).getD k fallback = ((m.get? k).bind (f k)).getD fallback
theorem Std.ExtDHashMap.getKey?_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} {k : α} :
(filterMap f m).getKey? k = (m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => (f x (m.get x )).isSome
@[simp]
theorem Std.ExtDHashMap.getKey_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aOption (γ a)} {k : α} {h' : k filterMap f m} :
(filterMap f m).getKey k h' = m.getKey k
theorem Std.ExtDHashMap.getKey!_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] [Inhabited α] {f : (a : α) → β aOption (γ a)} {k : α} :
(filterMap f m).getKey! k = ((m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => (f x (m.get x )).isSome).get!
theorem Std.ExtDHashMap.getKeyD_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aOption (γ a)} {k fallback : α} :
(filterMap f m).getKeyD k fallback = ((m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => (f x (m.get x )).isSome).getD fallback
theorem Std.ExtDHashMap.Const.filterMap_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβOption γ} :
filterMap f m = ∀ (k : α) (h : k m), f (m.getKey k h) (get m k h) = none
theorem Std.ExtDHashMap.Const.mem_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβOption γ} {k : α} :
k filterMap f m (h : k m), (f (m.getKey k h) (get m k h)).isSome = true
theorem Std.ExtDHashMap.Const.size_filterMap_eq_size_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβOption γ} :
(filterMap f m).size = m.size ∀ (k : α) (h : k m), (f (m.getKey k h) (get m k h)).isSome = true
theorem Std.ExtDHashMap.Const.get?_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβOption γ} {k : α} :
get? (filterMap f m) k = (get? m k).pbind fun (x : β) (h' : get? m k = some x) => f (m.getKey k ) x
theorem Std.ExtDHashMap.Const.get?_filterMap_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβOption γ} {k k' : α} (h : m.getKey? k = some k') :
get? (filterMap f m) k = (get? m k).bind (f k')
theorem Std.ExtDHashMap.Const.isSome_apply_of_mem_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβOption γ} {k : α} (h : k filterMap f m) :
(f (m.getKey k ) (get m k )).isSome = true
@[simp]
theorem Std.ExtDHashMap.Const.get_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβOption γ} {k : α} {h : k filterMap f m} :
get (filterMap f m) k h = (f (m.getKey k ) (get m k )).get
theorem Std.ExtDHashMap.Const.get!_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : αβOption γ} {k : α} :
get! (filterMap f m) k = ((get? m k).pbind fun (x : β) (h' : get? m k = some x) => f (m.getKey k ) x).get!
theorem Std.ExtDHashMap.Const.get!_filterMap_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : αβOption γ} {k k' : α} (h : m.getKey? k = some k') :
get! (filterMap f m) k = ((get? m k).bind (f k')).get!
theorem Std.ExtDHashMap.Const.getD_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβOption γ} {k : α} {fallback : γ} :
getD (filterMap f m) k fallback = ((get? m k).pbind fun (x : β) (h' : get? m k = some x) => f (m.getKey k ) x).getD fallback
theorem Std.ExtDHashMap.Const.getD_filterMap_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβOption γ} {k k' : α} {fallback : γ} (h : m.getKey? k = some k') :
getD (filterMap f m) k fallback = ((get? m k).bind (f k')).getD fallback
theorem Std.ExtDHashMap.Const.getKey?_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβOption γ} {k : α} :
(filterMap f m).getKey? k = (m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => (f x (get m x )).isSome
theorem Std.ExtDHashMap.Const.getKey!_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [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 (get m x )).isSome).get!
theorem Std.ExtDHashMap.Const.getKeyD_filterMap {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [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 (get m x )).isSome).getD fallback
theorem Std.ExtDHashMap.filterMap_eq_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aBool} :
filterMap (fun (k : α) => Option.guard fun (v : β k) => f k v) m = filter f m
@[simp]
theorem Std.ExtDHashMap.filter_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} :
filter f m = ∀ (k : α) (h : k m), f k (m.get k h) = false
theorem Std.ExtDHashMap.filter_key_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : αBool} :
filter (fun (a : α) (x : β a) => f a) m = ∀ (k : α) (h : k m), f (m.getKey k h) = false
theorem Std.ExtDHashMap.contains_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} {k : α} :
(filter f m).contains k = Option.any (f k) (m.get? k)
theorem Std.ExtDHashMap.mem_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} {k : α} :
k filter f m (h : k m), f k (m.get k h) = true
theorem Std.ExtDHashMap.mem_filter_key {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : αBool} {k : α} :
k filter (fun (a : α) (x : β a) => f a) m (h : k m), f (m.getKey k h) = true
theorem Std.ExtDHashMap.contains_of_contains_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aBool} {k : α} :
(filter f m).contains k = truem.contains k = true
theorem Std.ExtDHashMap.mem_of_mem_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aBool} {k : α} :
k filter f mk m
theorem Std.ExtDHashMap.size_filter_le_size {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aBool} :
theorem Std.ExtDHashMap.size_filter_eq_size_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} :
(filter f m).size = m.size ∀ (k : α) (h : k m), f k (m.get k h) = true
theorem Std.ExtDHashMap.filter_eq_self_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} :
filter f m = m ∀ (k : α) (h : k m), f k (m.get k h) = true
theorem Std.ExtDHashMap.filter_key_equiv_self_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : αBool} :
filter (fun (k : α) (x : β k) => f k) m = m ∀ (k : α) (h : k m), f (m.getKey k h) = true
theorem Std.ExtDHashMap.size_filter_key_eq_size_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : αBool} :
(filter (fun (k : α) (x : β k) => f k) m).size = m.size ∀ (k : α) (h : k m), f (m.getKey k h) = true
@[simp]
theorem Std.ExtDHashMap.get?_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} {k : α} :
(filter f m).get? k = Option.filter (f k) (m.get? k)
@[simp]
theorem Std.ExtDHashMap.get_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} {k : α} {h' : k filter f m} :
(filter f m).get k h' = m.get k
theorem Std.ExtDHashMap.get!_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} {k : α} [Inhabited (β k)] :
(filter f m).get! k = (Option.filter (f k) (m.get? k)).get!
theorem Std.ExtDHashMap.getD_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} {k : α} {fallback : β k} :
(filter f m).getD k fallback = (Option.filter (f k) (m.get? k)).getD fallback
theorem Std.ExtDHashMap.getKey?_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} {k : α} :
(filter f m).getKey? k = (m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => f x (m.get x )
theorem Std.ExtDHashMap.getKey?_filter_key {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : αBool} {k : α} :
(filter (fun (k : α) (x : β k) => f k) m).getKey? k = Option.filter f (m.getKey? k)
@[simp]
theorem Std.ExtDHashMap.getKey_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aBool} {k : α} {h' : k filter f m} :
(filter f m).getKey k h' = m.getKey k
theorem Std.ExtDHashMap.getKey!_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] [Inhabited α] {f : (a : α) → β aBool} {k : α} :
(filter f m).getKey! k = ((m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => f x (m.get x )).get!
theorem Std.ExtDHashMap.getKey!_filter_key {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : αBool} {k : α} :
(filter (fun (k : α) (x : β k) => f k) m).getKey! k = (Option.filter f (m.getKey? k)).get!
theorem Std.ExtDHashMap.getKeyD_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [LawfulBEq α] {f : (a : α) → β aBool} {k fallback : α} :
(filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => f x (m.get x )).getD fallback
theorem Std.ExtDHashMap.getKeyD_filter_key {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {f : αBool} {k fallback : α} :
(filter (fun (k : α) (x : β k) => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD fallback
theorem Std.ExtDHashMap.Const.filter_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} :
filter f m = ∀ (k : α) (h : k m), f (m.getKey k h) (get m k h) = false
theorem Std.ExtDHashMap.Const.mem_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} {k : α} :
k filter f m (h' : k m), f (m.getKey k h') (get m k h') = true
theorem Std.ExtDHashMap.Const.size_filter_le_size {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} :
theorem Std.ExtDHashMap.Const.size_filter_eq_size_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} :
(filter f m).size = m.size ∀ (a : α) (h : a m), f (m.getKey a h) (get m a h) = true
theorem Std.ExtDHashMap.Const.filter_eq_self_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} :
filter f m = m ∀ (k : α) (h : k m), f (m.getKey k h) (get m k h) = true
theorem Std.ExtDHashMap.Const.get?_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} {k : α} :
get? (filter f m) k = (get? m k).pfilter fun (x : β) (h' : get? m k = some x) => f (m.getKey k ) x
theorem Std.ExtDHashMap.Const.get?_filter_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} {k k' : α} :
m.getKey? k = some k'get? (filter f m) k = Option.filter (fun (x : β) => f k' x) (get? m k)
@[simp]
theorem Std.ExtDHashMap.Const.get_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} {k : α} {h' : k filter f m} :
get (filter f m) k h' = get m k
theorem Std.ExtDHashMap.Const.get!_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {f : αβBool} {k : α} :
get! (filter f m) k = ((get? m k).pfilter fun (x : β) (h' : get? m k = some x) => f (m.getKey k ) x).get!
theorem Std.ExtDHashMap.Const.get!_filter_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited β] {f : αβBool} {k k' : α} :
m.getKey? k = some k'get! (filter f m) k = (Option.filter (fun (x : β) => f k' x) (get? m k)).get!
theorem Std.ExtDHashMap.Const.getD_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} {k : α} {fallback : β} :
getD (filter f m) k fallback = ((get? m k).pfilter fun (x : β) (h' : get? m k = some x) => f (m.getKey k ) x).getD fallback
theorem Std.ExtDHashMap.Const.getD_filter_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} {k k' : α} {fallback : β} :
m.getKey? k = some k'getD (filter f m) k fallback = (Option.filter (fun (x : β) => f k' x) (get? m k)).getD fallback
theorem Std.ExtDHashMap.Const.getKey?_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβBool} {k : α} :
(filter f m).getKey? k = (m.getKey? k).pfilter fun (x : α) (h' : m.getKey? k = some x) => f x (get m x )
theorem Std.ExtDHashMap.Const.getKey!_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [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 (get m x )).get!
theorem Std.ExtDHashMap.Const.getKeyD_filter {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : ExtDHashMap α fun (x : α) => β} [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 (get m x )).getD fallback
@[simp]
theorem Std.ExtDHashMap.map_id_fun {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] :
map (fun (x : α) (v : β x) => v) m = m
@[simp]
theorem Std.ExtDHashMap.map_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} {δ : αType w'} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} {g : (a : α) → γ aδ a} :
map g (map f m) = map (fun (k : α) (v : β k) => g k (f k v)) m
theorem Std.ExtDHashMap.filterMap_eq_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} :
filterMap (fun (k : α) (v : β k) => some (f k v)) m = map f m
@[simp]
theorem Std.ExtDHashMap.map_eq_empty_iff {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} :
map f m = m =
theorem Std.ExtDHashMap.contains_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} {k : α} :
(map f m).contains k = m.contains k
theorem Std.ExtDHashMap.contains_of_contains_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} {k : α} :
(map f m).contains k = truem.contains k = true
@[simp]
theorem Std.ExtDHashMap.mem_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} {k : α} :
k map f m k m
theorem Std.ExtDHashMap.mem_of_mem_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} {k : α} :
k map f mk m
@[simp]
theorem Std.ExtDHashMap.size_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} :
(map f m).size = m.size
@[simp]
theorem Std.ExtDHashMap.get?_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aγ a} {k : α} :
(map f m).get? k = Option.map (f k) (m.get? k)
@[simp]
theorem Std.ExtDHashMap.get_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aγ a} {k : α} {h' : k map f m} :
(map f m).get k h' = f k (m.get k )
theorem Std.ExtDHashMap.get!_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aγ a} {k : α} [Inhabited (γ k)] :
(map f m).get! k = (Option.map (f k) (m.get? k)).get!
theorem Std.ExtDHashMap.getD_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [LawfulBEq α] {f : (a : α) → β aγ a} {k : α} {fallback : γ k} :
(map f m).getD k fallback = (Option.map (f k) (m.get? k)).getD fallback
@[simp]
theorem Std.ExtDHashMap.getKey?_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} {k : α} :
(map f m).getKey? k = m.getKey? k
@[simp]
theorem Std.ExtDHashMap.getKey_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} {k : α} {h' : k map f m} :
(map f m).getKey k h' = m.getKey k
@[simp]
theorem Std.ExtDHashMap.getKey!_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] [Inhabited α] {f : (a : α) → β aγ a} {k : α} :
(map f m).getKey! k = m.getKey! k
@[simp]
theorem Std.ExtDHashMap.getKeyD_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : αType v} {m : ExtDHashMap α β} {γ : αType w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β aγ a} {k fallback : α} :
(map f m).getKeyD k fallback = m.getKeyD k fallback
theorem Std.ExtDHashMap.Const.get?_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβγ} {k : α} :
get? (map f m) k = Option.pmap (fun (v : β) (h' : k m) => f (m.getKey k h') v) (get? m k)
theorem Std.ExtDHashMap.Const.get?_map_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβγ} {k k' : α} (h : m.getKey? k = some k') :
get? (map f m) k = Option.map (f k') (get? m k)
@[simp]
theorem Std.ExtDHashMap.Const.get_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβγ} {k : α} {h' : k map f m} :
get (map f m) k h' = f (m.getKey k ) (get m k )
theorem Std.ExtDHashMap.Const.get!_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : αβγ} {k : α} :
get! (map f m) k = (Option.pmap (fun (v : β) (h : k m) => f (m.getKey k h) v) (get? m k) ).get!
theorem Std.ExtDHashMap.Const.get!_map_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : αβγ} {k k' : α} (h : m.getKey? k = some k') :
get! (map f m) k = (Option.map (f k') (get? m k)).get!
theorem Std.ExtDHashMap.Const.getD_map {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] {f : αβγ} {k : α} {fallback : γ} :
getD (map f m) k fallback = (Option.pmap (fun (v : β) (h : k m) => f (m.getKey k h) v) (get? m k) ).getD fallback
theorem Std.ExtDHashMap.Const.getD_map_of_getKey?_eq_some {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {γ : Type w} {m : ExtDHashMap α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] [Inhabited γ] {f : αβγ} {k k' : α} {fallback : γ} (h : m.getKey? k = some k') :
getD (map f m) k fallback = (Option.map (f k') (get? m k)).getD fallback