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

@[simp]

theorem Std.DHashMap.Internal.toListModel_mkArray_nil {α : Type u} {β : α → Type v} {c : Nat} : toListModel (mkArray c AssocList.nil) = []

@[simp]

theorem Std.DHashMap.Internal.computeSize_eq {α : Type u} {β : α → Type v} {buckets : Array (AssocList α β)} : computeSize buckets = (toListModel buckets).length

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

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

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

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

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

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

theorem Std.DHashMap.Internal.Raw.foldRev_eq {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} : Raw.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

theorem Std.DHashMap.Internal.Raw.foldRev_cons_apply {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) : Raw.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

theorem Std.DHashMap.Internal.Raw.foldRev_cons {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List ((a : α) × β a)} : Raw.foldRev (fun (acc : List ((a : α) × β a)) (k : α) (v : β k) => ⟨k, v⟩ :: acc) acc l = toListModel l.buckets ++ acc

theorem Std.DHashMap.Internal.Raw.foldRev_cons_mk {α : Type u} {β : Type v} {l : Raw α fun (x : α) => β} {acc : List (α × β)} : Raw.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

theorem Std.DHashMap.Internal.Raw.foldRev_cons_key {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List α} : Raw.foldRev (fun (acc : List α) (k : α) (x : β k) => k :: acc) acc l = Internal.List.keys (toListModel l.buckets) ++ acc

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)

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)

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.foldRevM f init b = List.foldrM (fun (a : (a : α) × β a) (b : δ) => f b a.fst a.snd) init (toListModel b.buckets)

theorem Std.DHashMap.Internal.Raw.foldRev_eq_foldr_toListModel {α : Type u} {β : α → Type v} {γ : Type w} {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} : Raw.foldRev f init l = List.foldr (fun (a : (a : α) × β a) (b : γ) => f b a.fst a.snd) init (toListModel l.buckets)

theorem Std.DHashMap.Internal.Raw.toList_eq_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} : m.toList = toListModel m.buckets

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)

theorem Std.DHashMap.Internal.Raw.keys_eq_keys_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} : m.keys = Internal.List.keys (toListModel m.buckets)

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

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

@[simp]

theorem Std.DHashMap.Internal.Raw₀.toListModel_buckets_empty {α : Type u} {β : α → Type v} {c : Nat} : toListModel (empty c).val.buckets = []

theorem Std.DHashMap.Internal.Raw₀.wfImp_empty {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c : Nat} : Raw.WFImp (empty c).val

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

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)

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

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)

theorem Std.DHashMap.Internal.Raw₀.expand.go_pos {α : Type u} {β : α → Type v} [Hashable α] {i : Nat} {source : Array (AssocList α β)} {target : { d : Array (AssocList α β) // 0 < d.size }} (h : i < source.size) : go i source target = go (i + 1) (source.set i AssocList.nil h) (AssocList.foldl (reinsertAux hash) target source[i])

theorem Std.DHashMap.Internal.Raw₀.expand.go_neg {α : Type u} {β : α → Type v} [Hashable α] {i : Nat} {source : Array (AssocList α β)} {target : { d : Array (AssocList α β) // 0 < d.size }} (h : ¬i < source.size) : go i source target = target

theorem Std.DHashMap.Internal.Raw₀.expand.go_eq {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array (AssocList α β)) (target : { d : Array (AssocList α β) // 0 < d.size }) : go 0 source target = List.foldl (fun (acc : { d : Array (AssocList α β) // 0 < d.size }) (p : (a : α) × β a) => reinsertAux hash acc p.fst p.snd) target (toListModel 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

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)

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)

@[simp]

theorem Std.DHashMap.Internal.Raw₀.size_expandIfNecessary {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Raw₀ α β} : m.expandIfNecessary.val.size = m.val.size

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

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)

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)

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)

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)

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) ⋯

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) ⋯

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)

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)

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

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

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)

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)

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) ⋯

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) ⋯

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)

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)

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

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

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)

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)

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) ⋯

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) ⋯

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)

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)

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

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ₘ

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))

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

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ₘ

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)

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

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

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))

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

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))

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

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))

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))

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)))

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

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))

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))

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

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

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))

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))

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)))

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

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))

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))

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

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

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))

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

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

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))

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

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

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))

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ₘ

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))

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

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))

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

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))

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?

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))

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?

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))

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ₘ

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))

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

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

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))

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))

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

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))

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

filterMapₘ

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))

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

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

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))

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

mapₘ

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))

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

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

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))

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

filterₘ

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))

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

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

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))

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ₘ

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)

theorem Std.DHashMap.Internal.Raw.WF.out {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashable α] {m : Raw α β} (h : m.WF) : WFImp m

insertMany

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

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)

Const.insertListₘ

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

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)

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

Const.insertListIfNewUnitₘ

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

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)

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