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} :
@[simp]
theorem Std.DHashMap.Internal.Raw.buckets_emptyWithCapacity {α : Type u} {β : α → Type v} {c i : Nat} {h : i < (Raw.emptyWithCapacity c).buckets.size} :
@[simp]
@[simp]
theorem Std.DHashMap.Internal.Raw₀.Const.toList_emptyWithCapacity {α : Type u} {c : Nat} {β : Type v} :
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.Raw₀.tacticWf_trivial = Lean.ParserDescr.node `Std.DHashMap.Internal.Raw₀.tacticWf_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "wf_trivial" false)
Instances For
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.Raw₀.tacticEmpty = Lean.ParserDescr.node `Std.DHashMap.Internal.Raw₀.tacticEmpty 1024 (Lean.ParserDescr.nonReservedSymbol "empty" false)
Instances For
Internal implementation detail of the hash map
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem Std.DHashMap.Internal.Raw₀.toList_insert_perm {α : Type u} {β : α → Type v} (m : Raw₀ α β) [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k : α} {v : β k} :
theorem Std.DHashMap.Internal.Raw₀.Const.toList_insert_perm {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun (x : α) => β) [EquivBEq α] [LawfulHashable α] (h : m.val.WF) {k : α} {v : β} :
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₀.Const.toArray_toList_eq_toArray {α : Type u} {β : Type v} (m : Raw₀ α fun (x : α) => β) :
theorem Std.DHashMap.Internal.Raw₀.Const.toList_toArray_eq_toList {α : Type u} {β : Type v} (m : Raw₀ α fun (x : α) => β) :
theorem Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toArray {α : 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?_toArray_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?_toArray_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_toArray_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₀.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₀.foldM_eq_foldlM_toArray {α : 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_toArray {α : 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 = Array.foldrM (fun (a : (a : α) × β a) (b : δ) => f b a.fst a.snd) init m.val.toArray
theorem Std.DHashMap.Internal.Raw₀.foldRev_eq_foldr_toArray {α : Type u} {β : α → Type v} (m : Raw₀ α β) {δ : Type w} {f : δ → (a : α) → β a → δ} {init : δ} :
Raw.Internal.foldRev f init m.val = Array.foldr (fun (a : (a : α) × β a) (b : δ) => f b a.fst a.snd) init m.val.toArray
theorem Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_toArray {α : 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₀.foldM_eq_foldlM_keysArray {α : Type u} {β : α → Type v} (m : Raw₀ α β) {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ} :
theorem Std.DHashMap.Internal.Raw₀.foldRevM_eq_foldrM_keysArray {α : 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 = Array.foldrM (fun (a : α) (b : δ) => f b a) init m.val.keysArray
theorem Std.DHashMap.Internal.Raw₀.foldRev_eq_foldr_keysArray {α : Type u} {β : α → Type v} (m : Raw₀ α β) {δ : Type w} {f : δ → α → δ} {init : δ} :
Raw.Internal.foldRev (fun (d : δ) (a : α) (x : β a) => f d a) init m.val = Array.foldr (fun (a : α) (b : δ) => f b a) init m.val.keysArray
theorem Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_keysArray {α : 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_toArray {α : 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 = Array.foldlM (fun (a : δ) (b : α × β) => f a b.fst b.snd) init (Raw.Const.toArray m.val)
theorem Std.DHashMap.Internal.Raw₀.Const.fold_eq_foldl_toArray {α : Type u} {δ : Type w} {β : Type v} (m : Raw₀ α fun (x : α) => β) {f : δ → α → β → δ} {init : δ} :
Raw.fold f init m.val = Array.foldl (fun (a : δ) (b : α × β) => f a b.fst b.snd) init (Raw.Const.toArray m.val)
theorem Std.DHashMap.Internal.Raw₀.Const.foldRevM_eq_foldrM_toArray {α : 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 = Array.foldrM (fun (a : α × β) (b : δ) => f b a.fst a.snd) init (Raw.Const.toArray m.val)
theorem Std.DHashMap.Internal.Raw₀.Const.foldRev_eq_foldr_toArray {α : Type u} {δ : Type w} {β : Type v} (m : Raw₀ α fun (x : α) => β) {f : δ → α → β → δ} {init : δ} :
Raw.Internal.foldRev f init m.val = Array.foldr (fun (a : α × β) (b : δ) => f b a.fst a.snd) init (Raw.Const.toArray m.val)
theorem Std.DHashMap.Internal.Raw₀.Const.forM_eq_forM_toArray {α : Type u} {m' : Type w → Type w'} {β : Type v} (m : Raw₀ α fun (x : α) => β) [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} :
theorem Std.DHashMap.Internal.Raw₀.Const.forIn_eq_forIn_toArray {α : 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.toArray 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.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 α] :
@[simp]
theorem Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_singleton {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {k : α} {v : β k} :
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
theorem Std.DHashMap.Internal.Raw₀.contains_insertMany_emptyWithCapacity_list {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} :
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) :
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} :
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) :
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) :
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) :
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} :
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) :
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) :
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) :
theorem Std.DHashMap.Internal.Raw₀.size_insertMany_emptyWithCapacity_list_le {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
theorem Std.DHashMap.Internal.Raw₀.isEmpty_insertMany_emptyWithCapacity_list {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
@[simp]
theorem Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_nil {α : Type u} [BEq α] [Hashable α] {β : Type v} :
@[simp]
theorem Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_singleton {α : Type u} [BEq α] [Hashable α] {β : Type v} {k : α} {v : β} :
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
theorem Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_emptyWithCapacity_list {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} :
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) :
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} :
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) :
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) :
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) :
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} :
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) :
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) :
theorem Std.DHashMap.Internal.Raw₀.Const.size_insertMany_emptyWithCapacity_list_le {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
theorem Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
@[simp]
@[simp]
theorem Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_singleton {α : Type u} [BEq α] [Hashable α] {k : α} :
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
theorem Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_emptyWithCapacity_list {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
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) :
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) :
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} :
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) :
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) :
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) :
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) :
theorem Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list_le {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} :
theorem Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertManyIfNewUnit_emptyWithCapacity_list {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} :
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} :
theorem Std.DHashMap.Internal.Raw₀.Const.get!_insertManyIfNewUnit_emptyWithCapacity_list {α : Type u} [BEq α] [Hashable α] {l : List α} {k : α} :
theorem Std.DHashMap.Internal.Raw₀.getKey_union_of_contains_eq_false_left {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m₁ m₂ : Raw₀ α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₁.contains k = false) {h' : (m₁.union m₂).contains k = true} :
theorem Std.DHashMap.Internal.Raw₀.getKey_union_of_contains_eq_false_right {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m₁ m₂ : Raw₀ α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₂.contains k = false) {h' : (m₁.union m₂).contains k = true} :
theorem Std.DHashMap.Internal.Raw₀.Const.get_union_of_contains_eq_false_left {α : Type u} [BEq α] [Hashable α] {β : Type v} {m₁ m₂ : Raw₀ α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₁.contains k = false) {h' : (m₁.union m₂).contains k = true} :
theorem Std.DHashMap.Internal.Raw₀.Const.get_union_of_contains_eq_false_right {α : Type u} [BEq α] [Hashable α] {β : Type v} {m₁ m₂ : Raw₀ α fun (x : α) => β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₂.contains k = false) {h' : (m₁.union m₂).contains k = true} :
@[simp]
@[simp]
@[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₀.insertManyIfNew_list_equiv_foldl {α : Type u} {β : α → Type v} (m₁ : Raw₀ α β) [BEq α] [Hashable α] {l : List ((a : α) × β a)} :
(m₁.insertManyIfNew l).val.val.Equiv
(List.foldl (fun (acc : Raw α β) (p : (a : α) × β a) => acc.insertIfNew p.fst p.snd) m₁.val l)
theorem Std.DHashMap.Internal.Raw₀.Const.equiv_iff_toList_perm_toList {α : Type u} {β : Type v} (m₁ m₂ : Raw α fun (x : α) => β) :
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.insertManyIfNewUnit_list_equiv_foldl {α : Type u} [BEq α] [Hashable α] (m₁ : Raw₀ α fun (x : α) => Unit) {l : List α} :
(insertManyIfNewUnit m₁ l).val.val.Equiv
(List.foldl (fun (acc : Raw α fun (a : α) => Unit) (a : α) => acc.insertIfNew a ()) m₁.val l)
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
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).
def Std.DHashMap.Internal.Raw₀.decidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [(k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)] (m₁ m₂ : Raw₀ α β) (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) :
Internal implementation detail
Equations
- m₁.decidableEquiv m₂ h₁ h₂ = decidable_of_iff (m₁.beq m₂ = true) ⋯