This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.
File contents: verification of operations on Raw₀
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.buckets_emptyWithCapacity
{α : Type u}
{β : α → Type v}
{c i : Nat}
{h : i < (emptyWithCapacity c).val.buckets.size}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.buckets_emptyWithCapacity (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.buckets_empty
{α : Type u_1}
{β : α → Type u_2}
{c i : Nat}
{h : i < (emptyWithCapacity c).val.buckets.size}
:
Equations
Instances For
@[simp]
theorem
Std.DHashMap.Internal.Raw.buckets_emptyWithCapacity
{α : Type u}
{β : α → Type v}
{c i : Nat}
{h : i < (Raw.emptyWithCapacity c).buckets.size}
:
@[simp]
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.size_emptyWithCapacity (since := "2025-03-12")]
Equations
Instances For
Internal implementation detail of the hash map
Equations
Instances For
Internal implementation detail of the hash map
Equations
Instances For
Internal implementation detail of the hash map
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.contains_insertIfNew_self
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{k : α}
{v : β k}
:
theorem
Std.DHashMap.Internal.Raw₀.contains_of_contains_insertIfNew'
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.Const.get_insertIfNew
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{k a : α}
{v : β}
{h₁ : (m.insertIfNew k v).contains a = true}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.getD_insertIfNew
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{k a : α}
{fallback v : β}
:
theorem
Std.DHashMap.Internal.Raw₀.getKey_insertIfNew
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{k a : α}
{v : β k}
{h₁ : (m.insertIfNew k v).contains a = true}
:
theorem
Std.DHashMap.Internal.Raw₀.getKeyD_insertIfNew
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{k a fallback : α}
{v : β k}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toList
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{k : α}
{v : β}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{k k' : α}
{v : β}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.find?_toList_eq_none_iff_contains_eq_false
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{k : α}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{k : α}
{v : β}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.distinct_keys_toList
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
:
List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) (Raw.Const.toList m.val)
theorem
Std.DHashMap.Internal.Raw₀.foldM_eq_foldlM_toList
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
{δ : Type w}
{m' : Type w → Type w}
[Monad m']
[LawfulMonad m']
{f : δ → (a : α) → β a → m' δ}
{init : δ}
:
theorem
Std.DHashMap.Internal.Raw₀.foldRevM_eq_foldrM_toList
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
{δ : Type w}
{m' : Type w → Type w}
[Monad m']
[LawfulMonad m']
{f : δ → (a : α) → β a → m' δ}
{init : δ}
:
Raw.Internal.foldRevM f init m.val = List.foldrM (fun (a : (a : α) × β a) (b : δ) => f b a.fst a.snd) init m.val.toList
theorem
Std.DHashMap.Internal.Raw₀.foldRev_eq_foldr_toList
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
{δ : Type w}
{f : δ → (a : α) → β a → δ}
{init : δ}
:
Raw.Internal.foldRev f init m.val = List.foldr (fun (a : (a : α) × β a) (b : δ) => f b a.fst a.snd) init m.val.toList
theorem
Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_toList
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
{δ : Type w}
{m' : Type w → Type w}
[Monad m']
[LawfulMonad m']
{f : (a : α) → β a → δ → m' (ForInStep δ)}
{init : δ}
:
theorem
Std.DHashMap.Internal.Raw₀.foldRevM_eq_foldrM_keys
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
{δ : Type w}
{m' : Type w → Type w}
[Monad m']
[LawfulMonad m']
{f : δ → α → m' δ}
{init : δ}
:
Raw.Internal.foldRevM (fun (d : δ) (a : α) (x : β a) => f d a) init m.val = List.foldrM (fun (a : α) (b : δ) => f b a) init m.val.keys
theorem
Std.DHashMap.Internal.Raw₀.foldRev_eq_foldr_keys
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
{δ : Type w}
{f : δ → α → δ}
{init : δ}
:
Raw.Internal.foldRev (fun (d : δ) (a : α) (x : β a) => f d a) init m.val = List.foldr (fun (a : α) (b : δ) => f b a) init m.val.keys
theorem
Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_keys
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
{δ : Type w}
{m' : Type w → Type w}
[Monad m']
[LawfulMonad m']
{f : α → δ → m' (ForInStep δ)}
{init : δ}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.foldM_eq_foldlM_toList
{α : Type u}
{δ : Type w}
{m' : Type w → Type w}
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[Monad m']
[LawfulMonad m']
{f : δ → α → β → m' δ}
{init : δ}
:
Raw.foldM f init m.val = List.foldlM (fun (a : δ) (b : α × β) => f a b.fst b.snd) init (Raw.Const.toList m.val)
theorem
Std.DHashMap.Internal.Raw₀.Const.fold_eq_foldl_toList
{α : Type u}
{δ : Type w}
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
{f : δ → α → β → δ}
{init : δ}
:
Raw.fold f init m.val = List.foldl (fun (a : δ) (b : α × β) => f a b.fst b.snd) init (Raw.Const.toList m.val)
theorem
Std.DHashMap.Internal.Raw₀.Const.foldRevM_eq_foldrM_toList
{α : Type u}
{δ : Type w}
{m' : Type w → Type w}
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[Monad m']
[LawfulMonad m']
{f : δ → α → β → m' δ}
{init : δ}
:
Raw.Internal.foldRevM f init m.val = List.foldrM (fun (a : α × β) (b : δ) => f b a.fst a.snd) init (Raw.Const.toList m.val)
theorem
Std.DHashMap.Internal.Raw₀.Const.foldRev_eq_foldr_toList
{α : Type u}
{δ : Type w}
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
{f : δ → α → β → δ}
{init : δ}
:
Raw.Internal.foldRev f init m.val = List.foldr (fun (a : α × β) (b : δ) => f b a.fst a.snd) init (Raw.Const.toList m.val)
theorem
Std.DHashMap.Internal.Raw₀.Const.forIn_eq_forIn_toList
{α : Type u}
{δ : Type w}
{m' : Type w → Type w}
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[Monad m']
[LawfulMonad m']
{f : α → β → δ → m' (ForInStep δ)}
{init : δ}
:
Raw.forIn f init m.val = ForIn.forIn (Raw.Const.toList m.val) init fun (a : α × β) (b : δ) => f a.fst a.snd b
theorem
Std.DHashMap.Internal.Raw₀.insertMany_ind
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{ρ : Type w}
[ForIn Id ρ ((a : α) × β a)]
{motive : Raw₀ α β → Prop}
(m : Raw₀ α β)
(l : ρ)
(init : motive m)
(insert : ∀ (m : Raw₀ α β) (a : α) (b : β a), motive m → motive (m.insert a b))
:
motive (m.insertMany l).val
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.get?_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[LawfulBEq α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.get_insertMany_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[LawfulBEq α]
(h : m.val.WF)
{l : List ((a : α) × β a)}
{k : α}
(contains : (List.map Sigma.fst l).contains k = false)
{h' : (m.insertMany l).val.contains k = true}
:
theorem
Std.DHashMap.Internal.Raw₀.get_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[LawfulBEq α]
(h : m.val.WF)
{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' : (m.insertMany l).val.contains k' = true}
:
theorem
Std.DHashMap.Internal.Raw₀.get!_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[LawfulBEq α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.getD_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[LawfulBEq α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.getKey?_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.getKey_insertMany_list_of_contains_eq_false
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{l : List ((a : α) × β a)}
{k : α}
(h₁ : (List.map Sigma.fst l).contains k = false)
{h' : (m.insertMany l).val.contains k = true}
:
theorem
Std.DHashMap.Internal.Raw₀.getKey_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{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' : (m.insertMany l).val.contains k' = true}
:
theorem
Std.DHashMap.Internal.Raw₀.getKey!_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.getKeyD_insertMany_list_of_mem
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.Const.insertMany_ind
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
{ρ : Type w}
[ForIn Id ρ (α × β)]
{motive : (Raw₀ α fun (x : α) => β) → Prop}
(m : Raw₀ α fun (x : α) => β)
(l : ρ)
(init : motive m)
(insert : ∀ (m : Raw₀ α fun (x : α) => β) (a : α) (b : β), motive m → motive (m.insert a b))
:
motive (insertMany m l).val
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_list_of_mem
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.Const.getKey_insertMany_list_of_contains_eq_false
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{l : List (α × β)}
{k : α}
(h₁ : (List.map Prod.fst l).contains k = false)
{h' : (insertMany m l).val.contains k = true}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey_insertMany_list_of_mem
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{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' : (insertMany m l).val.contains k' = true}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_list_of_contains_eq_false
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
(h : m.val.WF)
{l : List (α × β)}
{k : α}
(h' : (List.map Prod.fst l).contains k = false)
:
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_list_of_mem
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_list_of_mem
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.Const.get?_insertMany_list_of_mem
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.Const.get_insertMany_list_of_contains_eq_false
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{l : List (α × β)}
{k : α}
(h₁ : (List.map Prod.fst l).contains k = false)
{h' : (insertMany m l).val.contains k = true}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.get_insertMany_list_of_mem
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{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' : (insertMany m l).val.contains k' = true}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_list_of_mem
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
[Inhabited β]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.Const.getD_insertMany_list_of_mem
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{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.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_ind
{α : Type u}
[BEq α]
[Hashable α]
{ρ : Type w}
[ForIn Id ρ α]
{motive : (Raw₀ α fun (x : α) => Unit) → Prop}
(m : Raw₀ α fun (x : α) => Unit)
(l : ρ)
(init : motive m)
(insert : ∀ (m : Raw₀ α fun (x : α) => Unit) (a : α), motive m → motive (m.insertIfNew a ()))
:
motive (insertManyIfNewUnit m l).val
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains
{α : Type u}
[BEq α]
[Hashable α]
(m : Raw₀ α fun (x : α) => Unit)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{l : List α}
{k : α}
{h' : (insertManyIfNewUnit m l).val.contains k = true}
(contains : m.contains k = true)
:
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
{α : Type u}
[BEq α]
[Hashable α]
(m : Raw₀ α fun (x : α) => Unit)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{l : List α}
{k k' : α}
(k_beq : (k == k') = true)
{h' : (insertManyIfNewUnit m l).val.contains k' = true}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_list_mem_of_contains
{α : Type u}
[BEq α]
[Hashable α]
(m : Raw₀ α fun (x : α) => Unit)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{l : List α}
{k : α}
(contains : m.contains k = true)
{h' : (insertManyIfNewUnit m l).val.contains k = true}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_list
{α : Type u}
[BEq α]
[Hashable α]
(m : Raw₀ α fun (x : α) => Unit)
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{l : List α}
(distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l)
:
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_nil
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_nil (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.insertMany_empty_list_nil
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
:
Equations
Instances For
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_singleton
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{k : α}
{v : β k}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_singleton (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.insertMany_empty_list_singleton
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
{k : α}
{v : β k}
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_cons
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{k : α}
{v : β k}
{tl : List ((a : α) × β a)}
:
(emptyWithCapacity.insertMany (⟨k, v⟩ :: tl)).val = ((emptyWithCapacity.insert k v).insertMany tl).val
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_cons (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.insertMany_empty_list_cons
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
{k : α}
{v : β k}
{tl : List ((a : α) × β a)}
:
(emptyWithCapacity.insertMany (⟨k, v⟩ :: tl)).val = ((emptyWithCapacity.insert k v).insertMany tl).val
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.contains_insertMany_emptyWithCapacity_list
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
{k : α}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.contains_insertMany_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.contains_insertMany_empty_list
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
{k : α}
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.get?_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[LawfulBEq α]
{l : List ((a : α) × β a)}
{k : α}
(h : (List.map Sigma.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.get?_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.get?_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.get?_insertMany_empty_list_of_mem
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[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)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.get_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[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 : (emptyWithCapacity.insertMany l).val.contains k' = true}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.get_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.get_insertMany_empty_list_of_mem
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[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 : (emptyWithCapacity.insertMany l).val.contains k' = true}
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.get!_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[LawfulBEq α]
{l : List ((a : α) × β a)}
{k : α}
[Inhabited (β k)]
(h : (List.map Sigma.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.get!_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.get!_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.get!_insertMany_empty_list_of_mem
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[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)
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.getD_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[LawfulBEq α]
{l : List ((a : α) × β a)}
{k : α}
{fallback : β k}
(contains_eq_false : (List.map Sigma.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.getD_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.getD_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.getD_insertMany_empty_list_of_mem
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[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)
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.getKey?_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
{k : α}
(h : (List.map Sigma.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.getKey?_insertMany_empty_list_of_mem
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[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)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.getKey_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[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' : (emptyWithCapacity.insertMany l).val.contains k' = true}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.getKey_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.getKey_insertMany_empty_list_of_mem
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[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' : (emptyWithCapacity.insertMany l).val.contains k' = true}
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.getKey!_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{l : List ((a : α) × β a)}
{k : α}
(h : (List.map Sigma.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.getKey!_insertMany_empty_list_of_mem
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[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)
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
{k fallback : α}
(h : (List.map Sigma.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_empty_list_of_mem
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[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)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.size_insertMany_emptyWithCapacity_list
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.size_insertMany_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.size_insertMany_empty_list
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
(distinct : List.Pairwise (fun (a b : (a : α) × β a) => (a.fst == b.fst) = false) l)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.size_insertMany_emptyWithCapacity_list_le
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.size_insertMany_emptyWithCapacity_list_le (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.size_insertMany_empty_list_le
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.isEmpty_insertMany_emptyWithCapacity_list
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.isEmpty_insertMany_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.isEmpty_insertMany_empty_list
{α : Type u_1}
{β : α → Type u_2}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List ((a : α) × β a)}
:
Equations
Instances For
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_nil
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_nil (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.insertMany_empty_list_nil
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
:
Equations
Instances For
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_singleton
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
{k : α}
{v : β}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_singleton (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.insertMany_empty_list_singleton
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
{k : α}
{v : β}
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_cons
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
{k : α}
{v : β}
{tl : List (α × β)}
:
(insertMany emptyWithCapacity ((k, v) :: tl)).val = (insertMany (emptyWithCapacity.insert k v) tl).val
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_cons (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.insertMany_empty_list_cons
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
{k : α}
{v : β}
{tl : List (α × β)}
:
(insertMany emptyWithCapacity ((k, v) :: tl)).val = (insertMany (emptyWithCapacity.insert k v) tl).val
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_emptyWithCapacity_list
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
{k : α}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_empty_list
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
{k : α}
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
{k : α}
(h : (List.map Prod.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_empty_list_of_mem
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[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)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.get_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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 : (insertMany emptyWithCapacity l).val.contains k' = true}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.get_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.get_insertMany_empty_list_of_mem
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[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 : (insertMany emptyWithCapacity l).val.contains k' = true}
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
{k : α}
[Inhabited β]
(h : (List.map Prod.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_empty_list_of_mem
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[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)
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
{k : α}
{fallback : β}
(contains_eq_false : (List.map Prod.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_empty_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_empty_list_of_mem
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[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)
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
{k : α}
(h : (List.map Prod.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_empty_list_of_mem
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[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)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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' : (insertMany emptyWithCapacity l).val.contains k' = true}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKey_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKey_insertMany_empty_list_of_mem
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[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' : (insertMany emptyWithCapacity l).val.contains k' = true}
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{l : List (α × β)}
{k : α}
(h : (List.map Prod.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_empty_list_of_mem
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[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)
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_empty_list_of_contains_eq_false
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
{k fallback : α}
(h : (List.map Prod.fst l).contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_empty_list_of_mem
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[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)
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.size_insertMany_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.size_insertMany_empty_list
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
(distinct : List.Pairwise (fun (a b : α × β) => (a.fst == b.fst) = false) l)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.size_insertMany_emptyWithCapacity_list_le
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.size_insertMany_emptyWithCapacity_list_le (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.size_insertMany_empty_list_le
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertMany_empty_list
{α : Type u_1}
[BEq α]
[Hashable α]
{β : Type u_2}
[EquivBEq α]
[LawfulHashable α]
{l : List (α × β)}
:
Equations
Instances For
@[simp]
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_nil (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_empty_list_nil
{α : Type u_1}
[BEq α]
[Hashable α]
:
Equations
Instances For
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_singleton
{α : Type u}
[BEq α]
[Hashable α]
{k : α}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_singleton (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_empty_list_singleton
{α : Type u_1}
[BEq α]
[Hashable α]
{k : α}
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons
{α : Type u}
[BEq α]
[Hashable α]
{hd : α}
{tl : List α}
:
(insertManyIfNewUnit emptyWithCapacity (hd :: tl)).val = (insertManyIfNewUnit (emptyWithCapacity.insertIfNew hd ()) tl).val
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_empty_list_cons
{α : Type u_1}
[BEq α]
[Hashable α]
{hd : α}
{tl : List α}
:
(insertManyIfNewUnit emptyWithCapacity (hd :: tl)).val = (insertManyIfNewUnit (emptyWithCapacity.insertIfNew hd ()) tl).val
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_emptyWithCapacity_list
{α : Type u}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_empty_list
{α : Type u_1}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false
{α : Type u}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
(h' : l.contains k = false)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false
{α : Type u_1}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
(h' : l.contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem
{α : Type u_1}
[BEq α]
[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)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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' : (insertManyIfNewUnit emptyWithCapacity l).val.contains k' = true}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_empty_list_of_mem
{α : Type u_1}
[BEq α]
[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' : (insertManyIfNewUnit emptyWithCapacity l).val.contains k' = true}
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false
{α : Type u_1}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
[Inhabited α]
{l : List α}
{k : α}
(h' : l.contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem
{α : Type u_1}
[BEq α]
[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)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false
{α : Type u}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k fallback : α}
(h' : l.contains k = false)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false
{α : Type u_1}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k fallback : α}
(h' : l.contains k = false)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem
{α : Type u}
[BEq α]
[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)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_empty_list_of_mem
{α : Type u_1}
[BEq α]
[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)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list
{α : Type u}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
(distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_empty_list
{α : Type u_1}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
(distinct : List.Pairwise (fun (a b : α) => (a == b) = false) l)
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list_le
{α : Type u}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list_le (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_empty_list_le
{α : Type u_1}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertManyIfNewUnit_emptyWithCapacity_list
{α : Type u}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertManyIfNewUnit_empty_list
{α : Type u_1}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.get?_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.get?_insertManyIfNewUnit_empty_list
{α : Type u_1}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{l : List α}
{k : α}
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.get_insertManyIfNewUnit_emptyWithCapacity_list
{α : Type u}
[BEq α]
[Hashable α]
{l : List α}
{k : α}
{h : (insertManyIfNewUnit emptyWithCapacity l).val.contains k = true}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.get_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.get_insertManyIfNewUnit_empty_list
{α : Type u_1}
[BEq α]
[Hashable α]
{l : List α}
{k : α}
{h : (insertManyIfNewUnit emptyWithCapacity l).val.contains k = true}
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.Const.get!_insertManyIfNewUnit_emptyWithCapacity_list
{α : Type u}
[BEq α]
[Hashable α]
{l : List α}
{k : α}
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.get!_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.get!_insertManyIfNewUnit_empty_list
{α : Type u_1}
[BEq α]
[Hashable α]
{l : List α}
{k : α}
:
Equations
Instances For
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_emptyWithCapacity_list (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_empty_list
{α : Type u_1}
[BEq α]
[Hashable α]
{l : List α}
{k : α}
{fallback : Unit}
:
Equations
Instances For
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.Const.getD_modify
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
[EquivBEq α]
[LawfulHashable α]
(m : Raw₀ α fun (x : α) => β)
(h : m.val.WF)
{k k' : α}
{fallback : β}
{f : β → β}
:
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.Const.getKey?_modify
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
[EquivBEq α]
[LawfulHashable α]
(m : Raw₀ α fun (x : α) => β)
(h : m.val.WF)
{k k' : α}
{f : β → β}
:
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.Const.getKeyD_modify
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
[EquivBEq α]
[LawfulHashable α]
(m : Raw₀ α fun (x : α) => β)
(h : m.val.WF)
{k k' fallback : α}
{f : β → β}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.equiv_iff_toList_perm_toList
{α : Type u}
{β : Type v}
(m₁ m₂ : Raw α fun (x : α) => β)
:
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.equiv_emptyWithCapacity_iff_isEmpty (since := "2025-03-12")]
abbrev
Std.DHashMap.Internal.Raw₀.equiv_empty_iff_isEmpty
{α : Type u_1}
{β : α → Type u_2}
(m : Raw₀ α β)
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(h : m.val.WF)
{c : Nat}
:
Equations
Instances For
theorem
Std.DHashMap.Internal.Raw₀.insertIfNew_equiv_congr
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m₁ m₂ : Raw₀ α β)
[EquivBEq α]
[LawfulHashable α]
(h₁ : m₁.val.WF)
(h₂ : m₂.val.WF)
(h : m₁.val.Equiv m₂.val)
{k : α}
{v : β k}
:
(m₁.insertIfNew k v).val.Equiv (m₂.insertIfNew k v).val
theorem
Std.DHashMap.Internal.Raw₀.insertMany_list_equiv_congr
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m₁ m₂ : Raw₀ α β)
[EquivBEq α]
[LawfulHashable α]
(h₁ : m₁.val.WF)
(h₂ : m₂.val.WF)
(h : m₁.val.Equiv m₂.val)
{l : List ((a : α) × β a)}
:
(m₁.insertMany l).val.val.Equiv (m₂.insertMany l).val.val
theorem
Std.DHashMap.Internal.Raw₀.Const.insertMany_list_equiv_congr
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
(m₁ m₂ : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
(h₁ : m₁.val.WF)
(h₂ : m₂.val.WF)
(h : m₁.val.Equiv m₂.val)
{l : List (α × β)}
:
(insertMany m₁ l).val.val.Equiv (insertMany m₂ l).val.val
theorem
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_list_equiv_congr
{α : Type u}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m₁ m₂ : Raw₀ α fun (x : α) => Unit}
(h₁ : m₁.val.WF)
(h₂ : m₂.val.WF)
(h : m₁.val.Equiv m₂.val)
{l : List α}
:
(insertManyIfNewUnit m₁ l).val.val.Equiv (insertManyIfNewUnit m₂ l).val.val
@[deprecated Std.DHashMap.Internal.Raw₀.Const.equiv_of_forall_getKey_eq_of_forall_get?_eq (since := "2025-04-25")]
theorem
Std.DHashMap.Internal.Raw₀.Const.toList_filterMap
{β : Type v}
{γ : Type w}
{α : Type u}
(m : Raw₀ α fun (x : α) => β)
{f : α → β → Option γ}
:
(Raw.Const.toList (filterMap f m).val).Perm
(List.filterMap (fun (p : α × β) => Option.map (fun (x : γ) => (p.fst, x)) (f p.fst p.snd)) (Raw.Const.toList m.val))
theorem
Std.DHashMap.Internal.Raw₀.Const.toList_filter
{β : Type v}
{α : Type u}
(m : Raw₀ α fun (x : α) => β)
{f : α → β → Bool}
:
(Raw.Const.toList (filter f m).val).Perm (List.filter (fun (p : α × β) => f p.fst p.snd) (Raw.Const.toList m.val))
theorem
Std.DHashMap.Internal.Raw₀.Const.get_map'
{α : Type u}
[BEq α]
[Hashable α]
{β : Type v}
{γ : Type w}
(m : Raw₀ α fun (x : α) => β)
[EquivBEq α]
[LawfulHashable α]
{f : α → β → γ}
{k : α}
(h : m.val.WF)
{h' : (map f m).contains k = true}
:
Variant of get_map
that holds with EquivBEq
(i.e. without LawfulBEq
).