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: proof that all hash map operations preserve `WFImp` to show `WF.out : WF → WFImp`

source
@[simp]
theorem Std.DHashMap.Internal.toListModel_replicate_nil {α : Type u} {β : α → Type v} {c : Nat} :
toListModel (Array.replicate c AssocList.nil) = []
source
@[reducible, inline, deprecated Std.DHashMap.Internal.toListModel_replicate_nil (since := "2025-03-18")]
abbrev Std.DHashMap.Internal.toListModel_mkArray_nil {α : Type u_1} {β : α → Type u_2} {c : Nat} :
toListModel (Array.replicate c AssocList.nil) = []
Equations

- @Std.DHashMap.Internal.toListModel_mkArray_nil = @Std.DHashMap.Internal.toListModel_replicate_nil

Instances For

source
@[simp]
theorem Std.DHashMap.Internal.computeSize_eq {α : Type u} {β : α → Type v} {buckets : Array (AssocList α β)} :
computeSize buckets = (toListModel buckets).length
source
theorem Std.DHashMap.Internal.Raw.equiv_iff_toListModel_perm {α : Type u} {β : α → Type v} {m₁ m₂ : Raw α β} :
m₁.Equiv m₂ ↔ (toListModel m₁.buckets).Perm (toListModel m₂.buckets)
source
theorem Std.DHashMap.Internal.Raw.size_eq_length {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : WFImp m) :
m.size = (toListModel m.buckets).length
source
theorem Std.DHashMap.Internal.Raw.isEmpty_eq_isEmpty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw α β} (h : WFImp m) :
m.isEmpty = (toListModel m.buckets).isEmpty
source
theorem Std.DHashMap.Internal.Raw.fold_eq {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
Raw.fold f init l = Array.foldl (fun (acc : γ) (l : AssocList α β) => AssocList.foldl f acc l) init l.buckets
source
theorem Std.DHashMap.Internal.Raw.fold_cons_apply {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
Raw.fold (fun (acc : List γ) (k : α) (v : β k) => f k v :: acc) acc l = List.map (fun (p : (a : α) × β a) => f p.fst p.snd) (toListModel l.buckets).reverse ++ acc
source
theorem Std.DHashMap.Internal.Raw.fold_cons {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List ((a : α) × β a)} :
Raw.fold (fun (acc : List ((a : α) × β a)) (k : α) (v : β k) => ⟨k, v⟩ :: acc) acc l = (toListModel l.buckets).reverse ++ acc
source
theorem Std.DHashMap.Internal.Raw.fold_cons_key {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List α} :
Raw.fold (fun (acc : List α) (k : α) (x : β k) => k :: acc) acc l = Internal.List.keys (toListModel l.buckets).reverse ++ acc
source
theorem Std.DHashMap.Internal.Raw.foldRev_eq {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
Raw.Internal.foldRev f init l = Array.foldr (fun (l : AssocList α β) (acc : γ) => AssocList.foldr (fun (a : α) (b : β a) (g : γ) => f g a b) acc l) init l.buckets
source
theorem Std.DHashMap.Internal.Raw.foldRev_cons_apply {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
Raw.Internal.foldRev (fun (acc : List γ) (k : α) (v : β k) => f k v :: acc) acc l = List.map (fun (p : (a : α) × β a) => f p.fst p.snd) (toListModel l.buckets) ++ acc
source
theorem Std.DHashMap.Internal.Raw.fold_push_apply {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {acc : Array γ} (f : (a : α) → β a → γ) :
Raw.fold (fun (acc : Array γ) (k : α) (v : β k) => acc.push (f k v)) acc l = acc ++ Array.map (fun (p : (a : α) × β a) => f p.fst p.snd) (toListModel l.buckets).toArray
source
theorem Std.DHashMap.Internal.Raw.foldRev_cons {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List ((a : α) × β a)} :
Raw.Internal.foldRev (fun (acc : List ((a : α) × β a)) (k : α) (v : β k) => ⟨k, v⟩ :: acc) acc l = toListModel l.buckets ++ acc
source
theorem Std.DHashMap.Internal.Raw.foldRev_cons_mk {α : Type u} {β : Type v} {l : Raw α fun (x : α) => β} {acc : List (α × β)} :
Raw.Internal.foldRev (fun (acc : List (α × β)) (k : α) (v : β) => (k, v) :: acc) acc l = List.map (fun (x : (_ : α) × β) => match x with | ⟨k, v⟩ => (k, v)) (toListModel l.buckets) ++ acc
source
theorem Std.DHashMap.Internal.Raw.foldRev_cons_key {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List α} :
Raw.Internal.foldRev (fun (acc : List α) (k : α) (x : β k) => k :: acc) acc l = Internal.List.keys (toListModel l.buckets) ++ acc
source
theorem Std.DHashMap.Internal.Raw.fold_push {α : Type u} {β : α → Type v} {l : Raw α β} {acc : Array ((a : α) × β a)} :
Raw.fold (fun (acc : Array ((a : α) × β a)) (k : α) (v : β k) => acc.push ⟨k, v⟩) acc l = acc ++ (toListModel l.buckets).toArray
source
theorem Std.DHashMap.Internal.Raw.fold_push_mk {α : Type u} {β : Type v} {l : Raw α fun (x : α) => β} {acc : Array (α × β)} :
Raw.fold (fun (acc : Array (α × β)) (k : α) (v : β) => acc.push (k, v)) acc l = acc ++ (List.map (fun (x : (_ : α) × β) => match x with | ⟨k, v⟩ => (k, v)) (toListModel l.buckets)).toArray
source
theorem Std.DHashMap.Internal.Raw.fold_push_key {α : Type u} {β : α → Type v} {l : Raw α β} {acc : Array α} :
Raw.fold (fun (acc : Array α) (k : α) (x : β k) => acc.push k) acc l = acc ++ (Internal.List.keys (toListModel l.buckets)).toArray
source
theorem Std.DHashMap.Internal.Raw.foldM_eq_foldlM_toListModel {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} {b : Raw α β} :
Raw.foldM f init b = List.foldlM (fun (a : δ) (b : (a : α) × β a) => f a b.fst b.snd) init (toListModel b.buckets)
source
theorem Std.DHashMap.Internal.Raw.fold_eq_foldl_toListModel {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
Raw.fold f init l = List.foldl (fun (a : γ) (b : (a : α) × β a) => f a b.fst b.snd) init (toListModel l.buckets)
source
theorem Std.DHashMap.Internal.Raw.foldRevM_eq_foldrM_toListModel {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} {b : Raw α β} :
Raw.Internal.foldRevM f init b = List.foldrM (fun (a : (a : α) × β a) (b : δ) => f b a.fst a.snd) init (toListModel b.buckets)
source
theorem Std.DHashMap.Internal.Raw.foldRev_eq_foldr_toListModel {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
Raw.Internal.foldRev f init l = List.foldr (fun (a : (a : α) × β a) (b : γ) => f b a.fst a.snd) init (toListModel l.buckets)
source
theorem Std.DHashMap.Internal.Raw.toList_eq_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} :
m.toList = toListModel m.buckets
source
theorem Std.DHashMap.Internal.Raw.Const.toList_eq_toListModel_map {α : Type u} {β : Type v} {m : Raw α fun (x : α) => β} :
Raw.Const.toList m = List.map (fun (x : (_ : α) × β) => match x with | ⟨k, v⟩ => (k, v)) (toListModel m.buckets)
source
theorem Std.DHashMap.Internal.Raw.toArray_eq_toArray_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} :
m.toArray = (toListModel m.buckets).toArray
source
theorem Std.DHashMap.Internal.Raw.Const.toArray_eq_toArray_map_toListModel {α : Type u} {β : Type v} {m : Raw α fun (x : α) => β} :
Raw.Const.toArray m = (List.map (fun (x : (_ : α) × β) => match x with | ⟨k, v⟩ => (k, v)) (toListModel m.buckets)).toArray
source
theorem Std.DHashMap.Internal.Raw.keys_eq_keys_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} :
m.keys = Internal.List.keys (toListModel m.buckets)
source
theorem Std.DHashMap.Internal.Raw.keysArray_eq_toArray_keys_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} :
m.keysArray = (Internal.List.keys (toListModel m.buckets)).toArray
source
theorem Std.DHashMap.Internal.Raw.forM_eq_forM_toListModel {α : Type u} {β : α → Type v} {l : Raw α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → m PUnit} :
Raw.forM f l = (toListModel l.buckets).forM fun (a : (a : α) × β a) => f a.fst a.snd
source
theorem Std.DHashMap.Internal.Raw.forIn_eq_forIn_toListModel {α : Type u} {β : α → Type v} {δ : Type w} {l : Raw α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} :
Raw.forIn f init l = ForIn.forIn (toListModel l.buckets) init fun (a : (a : α) × β a) (d : δ) => f a.fst a.snd d

# Raw₀.empty #

source
@[simp]
theorem Std.DHashMap.Internal.Raw₀.toListModel_buckets_emptyWithCapacity {α : Type u} {β : α → Type v} {c : Nat} :
toListModel (emptyWithCapacity c).val.buckets = []
source
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.toListModel_buckets_emptyWithCapacity (since := "2025-03-12")]
abbrev Std.DHashMap.Internal.Raw₀.toListModel_buckets_empty {α : Type u_1} {β : α → Type u_2} {c : Nat} :
toListModel (emptyWithCapacity c).val.buckets = []
Equations

- @Std.DHashMap.Internal.Raw₀.toListModel_buckets_empty = @Std.DHashMap.Internal.Raw₀.toListModel_buckets_emptyWithCapacity

Instances For

source
theorem Std.DHashMap.Internal.Raw₀.wfImp_emptyWithCapacity {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c : Nat} :
Raw.WFImp (emptyWithCapacity c).val
source
@[reducible, inline, deprecated Std.DHashMap.Internal.Raw₀.wfImp_emptyWithCapacity (since := "2025-03-12")]
abbrev Std.DHashMap.Internal.Raw₀.wfImp_empty {α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] {c : Nat} :
Raw.WFImp (emptyWithCapacity c).val
Equations

- @Std.DHashMap.Internal.Raw₀.wfImp_empty = @Std.DHashMap.Internal.Raw₀.wfImp_emptyWithCapacity

Instances For

source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_reinsertAux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (data : { d : Array (AssocList α β) // 0 < d.size }) (a : α) (b : β a) (h : IsHashSelf data.val) :
IsHashSelf (reinsertAux hash data a b).val

# expandIfNecessary #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_reinsertAux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] (data : { d : Array (AssocList α β) // 0 < d.size }) (a : α) (b : β a) :
(toListModel (reinsertAux hash data a b).val).Perm (⟨a, b⟩ :: toListModel data.val)
source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_foldl_reinsertAux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (l : List ((a : α) × β a)) (target : { d : Array (AssocList α β) // 0 < d.size }) :
IsHashSelf target.val → IsHashSelf (List.foldl (fun (acc : { d : Array (AssocList α β) // 0 < d.size }) (p : (a : α) × β a) => reinsertAux hash acc p.fst p.snd) target l).val
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_foldl_reinsertAux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] (l : List ((a : α) × β a)) (target : { d : Array (AssocList α β) // 0 < d.size }) :
(toListModel (List.foldl (fun (acc : { d : Array (AssocList α β) // 0 < d.size }) (p : (a : α) × β a) => reinsertAux hash acc p.fst p.snd) target l).val).Perm (l ++ toListModel target.val)
source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_expand {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulHashable α] [EquivBEq α] {buckets : { d : Array (AssocList α β) // 0 < d.size }} :
IsHashSelf (expand buckets).val
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_expand {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] {buckets : { d : Array (AssocList α β) // 0 < d.size }} :
(toListModel (expand buckets).val).Perm (toListModel buckets.val)
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_expandIfNecessary {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] (m : Raw₀ α β) :
(toListModel m.expandIfNecessary.val.buckets).Perm (toListModel m.val.buckets)
source
@[simp]
theorem Std.DHashMap.Internal.Raw₀.size_expandIfNecessary {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} :
m.expandIfNecessary.val.size = m.val.size
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_expandIfNecessary {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) :
Raw.WFImp m.expandIfNecessary.val

# Access operations #

source
theorem Std.DHashMap.Internal.Raw₀.containsₘ_eq_containsKey {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :
m.containsₘ a = Internal.List.containsKey a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.contains_eq_containsKey {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :
m.contains a = Internal.List.containsKey a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.get?ₘ_eq_getValueCast? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :
m.get?ₘ a = Internal.List.getValueCast? a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.get?_eq_getValueCast? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :
m.get? a = Internal.List.getValueCast? a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.getₘ_eq_getValue {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {h : m.containsₘ a = true} :
m.getₘ a h = Internal.List.getValueCast a (toListModel m.val.buckets) ⋯
source
theorem Std.DHashMap.Internal.Raw₀.get_eq_getValueCast {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {h : m.contains a = true} :
m.get a h = Internal.List.getValueCast a (toListModel m.val.buckets) ⋯
source
theorem Std.DHashMap.Internal.Raw₀.get!ₘ_eq_getValueCast! {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} [Inhabited (β a)] :
m.get!ₘ a = Internal.List.getValueCast! a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.get!_eq_getValueCast! {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} [Inhabited (β a)] :
m.get! a = Internal.List.getValueCast! a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.getDₘ_eq_getValueCastD {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {fallback : β a} :
m.getDₘ a fallback = Internal.List.getValueCastD a (toListModel m.val.buckets) fallback
source
theorem Std.DHashMap.Internal.Raw₀.getD_eq_getValueCastD {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {fallback : β a} :
m.getD a fallback = Internal.List.getValueCastD a (toListModel m.val.buckets) fallback
source
theorem Std.DHashMap.Internal.Raw₀.getKey?ₘ_eq_getKey? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :
m.getKey?ₘ a = Internal.List.getKey? a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.getKey?_eq_getKey? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :
m.getKey? a = Internal.List.getKey? a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.getKeyₘ_eq_getKey {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {h : m.contains a = true} :
m.getKeyₘ a h = Internal.List.getKey a (toListModel m.val.buckets) ⋯
source
theorem Std.DHashMap.Internal.Raw₀.getKey_eq_getKey {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} {h : m.contains a = true} :
m.getKey a h = Internal.List.getKey a (toListModel m.val.buckets) ⋯
source
theorem Std.DHashMap.Internal.Raw₀.getKey!ₘ_eq_getKey! {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :
m.getKey!ₘ a = Internal.List.getKey! a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.getKey!_eq_getKey! {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a : α} :
m.getKey! a = Internal.List.getKey! a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.getKeyDₘ_eq_getKeyD {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a fallback : α} :
m.getKeyDₘ a fallback = Internal.List.getKeyD a (toListModel m.val.buckets) fallback
source
theorem Std.DHashMap.Internal.Raw₀.getKeyD_eq_getKeyD {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.val) {a fallback : α} :
m.getKeyD a fallback = Internal.List.getKeyD a (toListModel m.val.buckets) fallback
source
theorem Std.DHashMap.Internal.Raw₀.Const.get?ₘ_eq_getValue? {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} :
get?ₘ m a = Internal.List.getValue? a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.Const.get?_eq_getValue? {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} :
get? m a = Internal.List.getValue? a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.Const.getₘ_eq_getValue {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} {h : m.containsₘ a = true} :
getₘ m a h = Internal.List.getValue a (toListModel m.val.buckets) ⋯
source
theorem Std.DHashMap.Internal.Raw₀.Const.get_eq_getValue {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} {h : m.contains a = true} :
get m a h = Internal.List.getValue a (toListModel m.val.buckets) ⋯
source
theorem Std.DHashMap.Internal.Raw₀.Const.get!ₘ_eq_getValue! {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] [Inhabited β] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} :
get!ₘ m a = Internal.List.getValue! a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.Const.get!_eq_getValue! {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] [Inhabited β] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} :
get! m a = Internal.List.getValue! a (toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.Const.getDₘ_eq_getValueD {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} {fallback : β} :
getDₘ m a fallback = Internal.List.getValueD a (toListModel m.val.buckets) fallback
source
theorem Std.DHashMap.Internal.Raw₀.Const.getD_eq_getValueD {α : Type u} {β : Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (hm : Raw.WFImp m.val) {a : α} {fallback : β} :
getD m a fallback = Internal.List.getValueD a (toListModel m.val.buckets) fallback

# `replaceₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_replaceₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) :
(toListModel (m.replaceₘ a b).val.buckets).Perm (Internal.List.replaceEntry a b (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_replaceₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) :
IsHashSelf (m.replaceₘ a b).val.buckets
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_replaceₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) :
Raw.WFImp (m.replaceₘ a b).val

# `insertₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_consₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) :
(toListModel (m.consₘ a b).val.buckets).Perm (⟨a, b⟩ :: toListModel m.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_consₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) :
IsHashSelf (m.consₘ a b).val.buckets
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_consₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (b : β a) (hc : m.containsₘ a = false) :
Raw.WFImp (m.consₘ a b).val
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_insertₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
(toListModel (m.insertₘ a b).val.buckets).Perm (Internal.List.insertEntry a b (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_insertₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
Raw.WFImp (m.insertₘ a b).val

# `insert` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_insert {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
(toListModel (m.insert a b).val.buckets).Perm (Internal.List.insertEntry a b (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_insert {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
Raw.WFImp (m.insert a b).val

# `alter` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_updateBucket_alter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :
(toListModel (updateBucket m.val.buckets ⋯ a (AssocList.alter a f))).Perm (Internal.List.alterKey a f (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_updateBucket_alter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :
IsHashSelf (updateBucket m.val.buckets ⋯ a (AssocList.alter a f))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_updateBucket_alter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :
Raw.WFImp (withComputedSize (updateBucket m.val.buckets ⋯ a (AssocList.alter a f)))
source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_alterₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (h : Raw.WFImp m.val) (a : α) (f : Option (β a) → Option (β a)) :
IsHashSelf (m.alterₘ a f).val.buckets
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_alterₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :
(toListModel (m.alterₘ a f).val.buckets).Perm (Internal.List.alterKey a f (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_alter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :
(toListModel (m.alter a f).val.buckets).Perm (Internal.List.alterKey a f (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_alterₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :
Raw.WFImp (m.alterₘ a f).val
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_alter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : Option (β a) → Option (β a)} :
Raw.WFImp (m.alter a f).val
source
theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_updateBucket_alter {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :
(toListModel (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))).Perm (Internal.List.Const.alterKey a f (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.Const.isHashSelf_updateBucket_alter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :
IsHashSelf (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f))
source
theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_updateBucket_alter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :
Raw.WFImp (withComputedSize (updateBucket m.val.buckets ⋯ a (AssocList.Const.alter a f)))
source
theorem Std.DHashMap.Internal.Raw₀.Const.isHashSelf_alterₘ {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (m : Raw₀ α fun (x : α) => β) (h : Raw.WFImp m.val) (a : α) (f : Option β → Option β) :
IsHashSelf (alterₘ m a f).val.buckets
source
theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_alterₘ {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :
(toListModel (alterₘ m a f).val.buckets).Perm (Internal.List.Const.alterKey a f (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_alter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :
(toListModel (alter m a f).val.buckets).Perm (Internal.List.Const.alterKey a f (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_alterₘ {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :
Raw.WFImp (alterₘ m a f).val
source
theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_alter {α : Type u} {β : Type v} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} (h : Raw.WFImp m.val) {a : α} {f : Option β → Option β} :
Raw.WFImp (alter m a f).val

# `modify` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_modify {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : β a → β a} :
(toListModel (m.modify a f).val.buckets).Perm (Internal.List.modifyKey a f (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_modifyₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : β a → β a} :
Raw.WFImp (m.modifyₘ a f).val
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_modify {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {f : β a → β a} :
Raw.WFImp (m.modify a f).val
source
theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_modify {α : Type u} {β : Type v} {m : Raw₀ α fun (x : α) => β} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (h : Raw.WFImp m.val) {a : α} {f : β → β} :
(toListModel (modify m a f).val.buckets).Perm (Internal.List.Const.modifyKey a f (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_modifyₘ {α : Type u} {β : Type v} {m : Raw₀ α fun (x : α) => β} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (h : Raw.WFImp m.val) {a : α} {f : β → β} :
Raw.WFImp (modifyₘ m a f).val
source
theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_modify {α : Type u} {β : Type v} {m : Raw₀ α fun (x : α) => β} [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (h : Raw.WFImp m.val) {a : α} {f : β → β} :
Raw.WFImp (modify m a f).val

# `containsThenInsert` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_containsThenInsert {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
(toListModel (m.containsThenInsert a b).snd.val.buckets).Perm (Internal.List.insertEntry a b (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_containsThenInsert {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
Raw.WFImp (m.containsThenInsert a b).snd.val

# `insertIfNewₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_insertIfNewₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
(toListModel (m.insertIfNewₘ a b).val.buckets).Perm (Internal.List.insertEntryIfNew a b (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_insertIfNewₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
Raw.WFImp (m.insertIfNewₘ a b).val

# `insertIfNew` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_insertIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
(toListModel (m.insertIfNew a b).val.buckets).Perm (Internal.List.insertEntryIfNew a b (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_insertIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
Raw.WFImp (m.insertIfNew a b).val

# `containsThenInsertIfNew` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_containsThenInsertIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
(toListModel (m.containsThenInsertIfNew a b).snd.val.buckets).Perm (Internal.List.insertEntryIfNew a b (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_containsThenInsertIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (h : Raw.WFImp m.val) {a : α} {b : β a} :
Raw.WFImp (m.containsThenInsertIfNew a b).snd.val

# `getThenInsertIfNew?` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_getThenInsertIfNew? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} {b : β a} (h : Raw.WFImp m.val) :
(toListModel (m.getThenInsertIfNew? a b).snd.val.buckets).Perm (Internal.List.insertEntryIfNew a b (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_getThenInsertIfNew? {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} {b : β a} (h : Raw.WFImp m.val) :
Raw.WFImp (m.getThenInsertIfNew? a b).snd.val

# `Const.getThenInsertIfNew?` #

source
theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_getThenInsertIfNew? {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} {a : α} {b : β} (h : Raw.WFImp m.val) :
(toListModel (getThenInsertIfNew? m a b).snd.val.buckets).Perm (Internal.List.insertEntryIfNew a b (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_getThenInsertIfNew? {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} {a : α} {b : β} (h : Raw.WFImp m.val) :
Raw.WFImp (getThenInsertIfNew? m a b).snd.val

# `eraseₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_eraseₘaux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.val) :
(toListModel (m.eraseₘaux a).val.buckets).Perm (Internal.List.eraseKey a (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_eraseₘaux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.val) :
IsHashSelf (m.eraseₘaux a).val.buckets
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_eraseₘaux {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.val) (h' : m.containsₘ a = true) :
Raw.WFImp (m.eraseₘaux a).val
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_perm_eraseKey_of_containsₘ_eq_false {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.val) (h' : m.containsₘ a = false) :
(toListModel m.val.buckets).Perm (Internal.List.eraseKey a (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_eraseₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α} (h : Raw.WFImp m.val) :
(toListModel (m.eraseₘ a).val.buckets).Perm (Internal.List.eraseKey a (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_eraseₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α} (h : Raw.WFImp m.val) :
Raw.WFImp (m.eraseₘ a).val

# `erase` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_erase {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α} (h : Raw.WFImp m.val) :
(toListModel (m.erase a).val.buckets).Perm (Internal.List.eraseKey a (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_erase {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α} (h : Raw.WFImp m.val) :
Raw.WFImp (m.erase a).val

# `filterₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_filterₘ {α : Type u} {β : α → Type v} {m : Raw₀ α β} {f : (a : α) → β a → Bool} :
(toListModel (m.filterₘ f).val.buckets).Perm (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_filterₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Bool} (h : Raw.WFImp m.val) :
IsHashSelf (m.filterₘ f).val.buckets
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_filterₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Bool} (h : Raw.WFImp m.val) :
Raw.WFImp (m.filterₘ f).val

# `filter` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_filter {α : Type u} {β : α → Type v} {m : Raw₀ α β} {f : (a : α) → β a → Bool} :
(toListModel (filter f m).val.buckets).Perm (List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_filter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Bool} (h : Raw.WFImp m.val) :
Raw.WFImp (filter f m).val

# `insertListₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_insertListₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.val) :
(toListModel (m.insertListₘ l).val.buckets).Perm (Internal.List.insertList (toListModel m.val.buckets) l)

# `insertListₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_insertListIfNewₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.val) :
(toListModel (m.insertListIfNewₘ l).val.buckets).Perm (Internal.List.insertListIfNew (toListModel m.val.buckets) l)

# `unionₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.insertMany_eq_insertListₘ_toListModel {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m m₂ : Raw₀ α β) :
(m.insertMany m₂.val).val = m.insertListₘ (toListModel m₂.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.insertManyIfNew_eq_insertListIfNewₘ_toListModel {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m m₂ : Raw₀ α β) :
(m.insertManyIfNew m₂.val).val = m.insertListIfNewₘ (toListModel m₂.val.buckets)
source
theorem Std.DHashMap.Internal.Raw₀.union_eq_unionₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) :
m₁.union m₂ = m₁.unionₘ m₂
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_unionₘ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw₀ α β} (h₁ : Raw.WFImp m₁.val) (h₂ : Raw.WFImp m₂.val) :
(toListModel (m₁.unionₘ m₂).val.buckets).Perm (Internal.List.insertList (toListModel m₁.val.buckets) (toListModel m₂.val.buckets))
source
theorem Std.DHashMap.Internal.Raw.WF.out {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashable α] {m : Raw α β} (h : m.WF) :
WFImp m

# `filterMapₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_filterMapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :
(toListModel (m.filterMapₘ f).val.buckets).Perm (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : δ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_filterMapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.val) :
IsHashSelf (m.filterMapₘ f).val.buckets
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_filterMapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.val) :
Raw.WFImp (m.filterMapₘ f).val

# `filterMap` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_filterMap {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :
(toListModel (filterMap f m).val.buckets).Perm (List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : δ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd)) (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_filterMap {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.val) :
Raw.WFImp (filterMap f m).val
source
theorem Std.DHashMap.Internal.Raw₀.wf_filterMap₀ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw₀ α β} (h : m.val.WF) {f : (a : α) → β a → Option (δ a)} :
(filterMap f m).val.WF
source
theorem Std.DHashMap.Internal.Raw₀.filterMap_eq_filter {α : Type u} {β : α → Type v} {m : Raw₀ α β} {f : (a : α) → β a → Bool} :
filterMap (fun (k : α) => Option.guard fun (v : β k) => f k v) m = filter f m
source
theorem Std.DHashMap.Internal.Raw₀.filterMap_eq_map {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {γ : α → Type w} (m : Raw₀ α β) (f : (a : α) → β a → γ a) (h : m.val.WF) :
filterMap (fun (k : α) (v : β k) => some (f k v)) m = map f m

# `mapₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_mapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Raw₀ α β} {f : (a : α) → β a → δ a} :
(toListModel (m.mapₘ f).val.buckets).Perm (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.isHashSelf_mapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → δ a} (h : Raw.WFImp m.val) :
IsHashSelf (m.mapₘ f).val.buckets
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_mapₘ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → δ a} (h : Raw.WFImp m.val) :
Raw.WFImp (m.mapₘ f).val

# `map` #

source
theorem Std.DHashMap.Internal.Raw₀.toListModel_map {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Raw₀ α β} {f : (a : α) → β a → δ a} :
(toListModel (map f m).val.buckets).Perm (List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) (toListModel m.val.buckets))
source
theorem Std.DHashMap.Internal.Raw₀.wfImp_map {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {f : (a : α) → β a → δ a} (h : Raw.WFImp m.val) :
Raw.WFImp (map f m).val
source
theorem Std.DHashMap.Internal.Raw₀.wf_map₀ {α : Type u} {β : α → Type v} {δ : α → Type w} [BEq α] [Hashable α] {m : Raw₀ α β} (h : m.val.WF) {f : (a : α) → β a → δ a} :
(map f m).val.WF

# `insertMany` #

source
theorem Std.DHashMap.Internal.Raw₀.wfImp_insertMany {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw₀ α β} {l : ρ} (h : Raw.WFImp m.val) :
Raw.WFImp (m.insertMany l).val.val
source
theorem Std.DHashMap.Internal.Raw₀.wf_insertMany₀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw α β} {h : 0 < m.buckets.size} {l : ρ} (h' : m.WF) :
(insertMany ⟨m, h⟩ l).val.val.WF
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_insertMany_list {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.val) :
(toListModel (m.insertMany l).val.val.buckets).Perm (Internal.List.insertList (toListModel m.val.buckets) l)

# `insertManyIfNew` #

source
theorem Std.DHashMap.Internal.Raw₀.wfImp_insertManyIfNew {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw₀ α β} {l : ρ} (h : Raw.WFImp m.val) :
Raw.WFImp (m.insertManyIfNew l).val.val
source
theorem Std.DHashMap.Internal.Raw₀.wf_insertManyIfNew₀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw α β} {h : 0 < m.buckets.size} {l : ρ} (h' : m.WF) :
(insertManyIfNew ⟨m, h⟩ l).val.val.WF
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_insertManyIfNew_list {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.val) :
(toListModel (m.insertManyIfNew l).val.val.buckets).Perm (Internal.List.insertListIfNew (toListModel m.val.buckets) l)

# `union` #

source
theorem Std.DHashMap.Internal.Raw₀.wf_union₀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw α β} {h₁ : 0 < m₁.buckets.size} {h₂ : 0 < m₂.buckets.size} (h'₁ : m₁.WF) (h'₂ : m₂.WF) :
(union ⟨m₁, h₁⟩ ⟨m₂, h₂⟩).val.WF
source
theorem Std.DHashMap.Internal.Raw₀.toListModel_union {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw₀ α β} (h₁ : Raw.WFImp m₁.val) (h₂ : Raw.WFImp m₂.val) :
(toListModel (m₁.union m₂).val.buckets).Perm (Internal.List.insertList (toListModel m₁.val.buckets) (toListModel m₂.val.buckets))

# `Const.insertListₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_insertListₘ {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} {l : List (α × β)} (h : Raw.WFImp m.val) :
(toListModel (insertListₘ m l).val.buckets).Perm (Internal.List.insertListConst (toListModel m.val.buckets) l)

# `Const.insertMany` #

source
theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_insertMany_list {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => β} {l : List (α × β)} (h : Raw.WFImp m.val) :
(toListModel (insertMany m l).val.val.buckets).Perm (Internal.List.insertListConst (toListModel m.val.buckets) l)
source
theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_insertMany {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ (α × β)] {m : Raw₀ α fun (x : α) => β} {l : ρ} (h : Raw.WFImp m.val) :
Raw.WFImp (insertMany m l).val.val
source
theorem Std.DHashMap.Internal.Raw₀.Const.wf_insertMany₀ {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ (α × β)] {m : Raw α fun (x : α) => β} {h : 0 < m.buckets.size} {l : ρ} (h' : m.WF) :
(insertMany ⟨m, h⟩ l).val.val.WF

# `Const.insertListIfNewUnitₘ` #

source
theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_insertListIfNewUnitₘ {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => Unit} {l : List α} (h : Raw.WFImp m.val) :
(toListModel (insertListIfNewUnitₘ m l).val.buckets).Perm (Internal.List.insertListIfNewUnit (toListModel m.val.buckets) l)

# `Const.insertManyIfNewUnit` #

source
theorem Std.DHashMap.Internal.Raw₀.Const.toListModel_insertManyIfNewUnit_list {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α fun (x : α) => Unit} {l : List α} (h : Raw.WFImp m.val) :
(toListModel (insertManyIfNewUnit m l).val.val.buckets).Perm (Internal.List.insertListIfNewUnit (toListModel m.val.buckets) l)
source
theorem Std.DHashMap.Internal.Raw₀.Const.wfImp_insertManyIfNewUnit {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ α] {m : Raw₀ α fun (x : α) => Unit} {l : ρ} (h : Raw.WFImp m.val) :
Raw.WFImp (insertManyIfNewUnit m l).val.val
source
theorem Std.DHashMap.Internal.Raw₀.Const.wf_insertManyIfNewUnit₀ {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ α] {m : Raw α fun (x : α) => Unit} {h : 0 < m.buckets.size} {l : ρ} (h' : m.WF) :
(insertManyIfNewUnit ⟨m, h⟩ l).val.val.WF