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.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}
:
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)
:
theorem
Std.ExtDHashMap.eq_empty_iff_forall_contains
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
theorem
Std.ExtDHashMap.eq_empty_iff_forall_not_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
@[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.contains_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β k}
:
theorem
Std.ExtDHashMap.mem_of_mem_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β k}
:
theorem
Std.ExtDHashMap.contains_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.ExtDHashMap.mem_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.ExtDHashMap.eq_empty_iff_size_eq_zero
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
theorem
Std.ExtDHashMap.size_le_size_insert
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.ExtDHashMap.size_insert_le
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β k}
:
theorem
Std.ExtDHashMap.mem_of_mem_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
:
theorem
Std.ExtDHashMap.size_erase_le
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
theorem
Std.ExtDHashMap.size_le_size_erase
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
@[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.Const.get?_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β}
:
theorem
Std.ExtDHashMap.Const.contains_eq_isSome_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
@[simp]
theorem
Std.ExtDHashMap.Const.isSome_get?_eq_contains
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
theorem
Std.ExtDHashMap.Const.mem_iff_isSome_get?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
@[simp]
theorem
Std.ExtDHashMap.Const.isSome_get?_iff_mem
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
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 : α}
:
theorem
Std.ExtDHashMap.Const.get?_eq_none
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
:
@[simp]
theorem
Std.ExtDHashMap.Const.get?_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
:
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)
:
@[simp]
theorem
Std.ExtDHashMap.Const.get_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{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}
:
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)
:
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}
:
@[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 : β}
:
theorem
Std.ExtDHashMap.Const.get!_eq_default
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{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!
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{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 : α}
:
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}
:
@[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 : β}
:
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 : β}
:
theorem
Std.ExtDHashMap.Const.getD_eq_fallback
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{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 : β}
:
theorem
Std.ExtDHashMap.Const.get?_eq_some_getD
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{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 : β}
:
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}
:
theorem
Std.ExtDHashMap.Const.get!_eq_getD_default
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
{a : α}
:
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)
:
@[simp]
theorem
Std.ExtDHashMap.getKey?_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β 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')
:
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 : α}
:
@[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 : α}
:
theorem
Std.ExtDHashMap.getKey?_congr
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k k' : α}
(h : (k == k') = true)
:
@[simp]
theorem
Std.ExtDHashMap.getKey_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{v : β 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}
:
theorem
Std.ExtDHashMap.getKey?_eq_some_getKey
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
(h : a ∈ m)
:
theorem
Std.ExtDHashMap.getKey_eq_get_getKey?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a : α}
{h : a ∈ m}
:
theorem
Std.ExtDHashMap.getKey_beq
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
(h : k ∈ m)
:
@[simp]
theorem
Std.ExtDHashMap.getKey!_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
{b : β a}
:
theorem
Std.ExtDHashMap.getKey!_eq_default
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{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!
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
theorem
Std.ExtDHashMap.getKey!_eq_get!_getKey?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
:
theorem
Std.ExtDHashMap.getKey_eq_getKey!
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{a : α}
{h : a ∈ m}
:
@[simp]
theorem
Std.ExtDHashMap.getKeyD_insert_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
{v : β 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 : α}
:
theorem
Std.ExtDHashMap.getKeyD_eq_fallback
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
@[simp]
theorem
Std.ExtDHashMap.getKeyD_erase_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k fallback : α}
:
theorem
Std.ExtDHashMap.getKey?_eq_some_getKeyD
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.ExtDHashMap.getKeyD_eq_getD_getKey?
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
:
theorem
Std.ExtDHashMap.getKey_eq_getKeyD
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{a fallback : α}
{h : a ∈ m}
:
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)
:
@[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}
:
@[simp]
theorem
Std.ExtDHashMap.mem_insertIfNew
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{v : β k}
:
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}
:
theorem
Std.ExtDHashMap.mem_of_mem_insertIfNew
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{k a : α}
{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}
:
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}
:
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}
:
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}
:
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}
:
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}
:
@[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}
:
theorem
Std.ExtDHashMap.insertMany_append
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{l₁ l₂ : List ((a : α) × β a)}
:
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 m → motive (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)
:
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_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)
:
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}
:
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}
:
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)
:
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)
:
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}
:
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}
:
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)
:
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)
:
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)
:
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)
:
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 : α × β}
:
theorem
Std.ExtDHashMap.Const.insertMany_append
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{l₁ l₂ : List (α × β)}
:
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 m → motive (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 : α}
:
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)
:
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}
:
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}
:
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)
:
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)
:
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)
:
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)
:
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 (α × β)}
:
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)
:
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)
:
theorem
Std.ExtDHashMap.Const.get?_insertMany_list
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
{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}
:
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}
:
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)
:
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)
:
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)
:
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)
:
@[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 m → motive (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)
:
k ∈ insertManyIfNewUnit m l → k ∈ m
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)
:
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)
:
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)
:
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)
:
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 : ρ}
:
insertManyIfNewUnit m l = ∅ → m = ∅
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}
:
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}
:
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)
:
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)
:
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)
:
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}
:
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)
:
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)
:
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)
:
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}
:
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)
:
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)
:
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)
:
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}
:
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)
:
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)
:
@[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}
:
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)
:
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)
:
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 : α}
{h : k ∈ unitOfList l}
:
@[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}
:
theorem
Std.ExtDHashMap.size_alter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
{k : α}
{f : Option (β k) → Option (β k)}
:
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)}
:
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)}
:
theorem
Std.ExtDHashMap.getKey?_alter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
{k k' : α}
{f : Option (β k) → Option (β k)}
:
theorem
Std.ExtDHashMap.getKey!_alter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
[Inhabited α]
{k k' : α}
{f : Option (β k) → Option (β 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)}
:
@[simp]
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 β}
:
theorem
Std.ExtDHashMap.Const.size_alter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{f : Option β → Option β}
:
@[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 β}
:
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}
:
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 β}
:
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 β}
:
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 β}
:
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 β}
:
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 β}
:
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}
:
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 β}
:
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 β}
:
@[simp]
theorem
Std.ExtDHashMap.get?_modify_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
{k : α}
{f : β k → β 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}
:
@[simp]
theorem
Std.ExtDHashMap.get!_modify_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
{k : α}
[Inhabited (β k)]
{f : β k → β k}
:
theorem
Std.ExtDHashMap.getD_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
{k k' : α}
{fallback : β k'}
{f : β k → β k}
:
@[simp]
theorem
Std.ExtDHashMap.getD_modify_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
{k : α}
{fallback : β k}
{f : β k → β k}
:
@[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 : β → β}
:
@[simp]
theorem
Std.ExtDHashMap.Const.contains_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k k' : α}
{f : β → β}
:
@[simp]
theorem
Std.ExtDHashMap.Const.mem_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k k' : α}
{f : β → β}
:
@[simp]
theorem
Std.ExtDHashMap.Const.size_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{f : β → β}
:
@[simp]
theorem
Std.ExtDHashMap.Const.get?_modify_self
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k : α}
{f : β → β}
:
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}
:
@[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}
:
theorem
Std.ExtDHashMap.Const.get!_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k k' : α}
[Inhabited β]
{f : β → β}
:
@[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 : β → β}
:
theorem
Std.ExtDHashMap.Const.getD_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k k' : α}
{fallback : β}
{f : β → β}
:
@[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 : β → β}
:
theorem
Std.ExtDHashMap.Const.getKey!_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{k k' : α}
{f : β → β}
:
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}
:
@[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}
:
theorem
Std.ExtDHashMap.Const.getKeyD_modify
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{k k' fallback : α}
{f : β → β}
:
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)
:
theorem
Std.ExtDHashMap.mem_of_mem_filterMap
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
{γ : α → Type w}
[EquivBEq α]
[LawfulHashable α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
:
theorem
Std.ExtDHashMap.size_filterMap_le_size
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
{γ : α → Type w}
[EquivBEq α]
[LawfulHashable α]
{f : (a : α) → β a → Option (γ a)}
:
theorem
Std.ExtDHashMap.getKey?_filterMap
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
{γ : α → Type w}
[LawfulBEq α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
:
theorem
Std.ExtDHashMap.getKey!_filterMap
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
{γ : α → Type w}
[LawfulBEq α]
[Inhabited α]
{f : (a : α) → β a → Option (γ a)}
{k : α}
:
theorem
Std.ExtDHashMap.getKeyD_filterMap
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
{γ : α → Type w}
[LawfulBEq α]
{f : (a : α) → β a → Option (γ a)}
{k fallback : α}
:
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 γ}
:
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 : α}
:
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')
:
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)
:
@[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}
:
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 : α}
:
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')
:
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 : γ}
:
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')
:
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 : α}
:
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 : α}
:
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 : α}
:
theorem
Std.ExtDHashMap.filterMap_eq_filter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{f : (a : α) → β a → Bool}
:
theorem
Std.ExtDHashMap.contains_filter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
{f : (a : α) → β a → Bool}
{k : α}
:
theorem
Std.ExtDHashMap.mem_of_mem_filter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{f : (a : α) → β a → Bool}
{k : α}
:
theorem
Std.ExtDHashMap.size_filter_le_size
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{f : (a : α) → β a → Bool}
:
@[simp]
theorem
Std.ExtDHashMap.get?_filter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
{f : (a : α) → β a → Bool}
{k : α}
:
theorem
Std.ExtDHashMap.getD_filter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
{f : (a : α) → β a → Bool}
{k : α}
{fallback : β k}
:
theorem
Std.ExtDHashMap.getKey?_filter_key
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{f : α → Bool}
{k : α}
:
theorem
Std.ExtDHashMap.getKey!_filter_key
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{f : α → Bool}
{k : α}
:
theorem
Std.ExtDHashMap.getKeyD_filter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[LawfulBEq α]
{f : (a : α) → β a → Bool}
{k fallback : α}
:
theorem
Std.ExtDHashMap.getKeyD_filter_key
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
{f : α → Bool}
{k fallback : α}
:
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.get?_filter_of_getKey?_eq_some
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{f : α → β → Bool}
{k 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 : α}
:
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' : α}
:
theorem
Std.ExtDHashMap.Const.getD_filter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{f : α → β → Bool}
{k : α}
{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 : β}
:
theorem
Std.ExtDHashMap.Const.getKey?_filter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{f : α → β → Bool}
{k : α}
:
theorem
Std.ExtDHashMap.Const.getKey!_filter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{f : α → β → Bool}
{k : α}
:
theorem
Std.ExtDHashMap.Const.getKeyD_filter
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{f : α → β → Bool}
{k fallback : α}
:
@[simp]
theorem
Std.ExtDHashMap.map_id_fun
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
[EquivBEq α]
[LawfulHashable α]
:
@[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}
:
theorem
Std.ExtDHashMap.filterMap_eq_map
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
{γ : α → Type w}
[EquivBEq α]
[LawfulHashable α]
{f : (a : α) → β a → γ a}
:
theorem
Std.ExtDHashMap.contains_map
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
{γ : α → Type w}
[EquivBEq α]
[LawfulHashable α]
{f : (a : α) → β a → γ a}
{k : α}
:
@[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 : α}
:
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 : α}
:
@[simp]
theorem
Std.ExtDHashMap.size_map
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
{γ : α → Type w}
[EquivBEq α]
[LawfulHashable α]
{f : (a : α) → β a → γ a}
:
@[simp]
theorem
Std.ExtDHashMap.get?_map
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : α → Type v}
{m : ExtDHashMap α β}
{γ : α → Type w}
[LawfulBEq α]
{f : (a : α) → β a → γ a}
{k : α}
:
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}
:
@[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 : α}
:
@[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 : α}
:
@[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 : α}
:
theorem
Std.ExtDHashMap.Const.get?_map
{α : Type u}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type v}
{γ : Type w}
{m : ExtDHashMap α fun (x : α) => β}
[EquivBEq α]
[LawfulHashable α]
{f : α → β → γ}
{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')
:
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 : α}
:
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')
:
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 : γ}
:
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')
: