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 = 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_key {α : Type u} {β : α → Type v} {l : Raw α β} {acc : List α} : Raw.foldRev (fun (acc : List α) (k : α) (x : β k) => k :: acc) acc l = List.keys (toListModel l.buckets) ++ acc

theorem Std.DHashMap.Internal.Raw.toList_perm_toListModel {α : Type u} {β : α → Type v} {m : Raw α β} : m.toList.Perm (toListModel m.buckets)

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

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

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

theorem Std.DHashMap.Internal.Raw.contains_keys_eq_contains_keys {α : Type u} {β : α → Type v} [BEq α] {m : Raw α β} {k : α} : m.keys.contains k = (List.keys (toListModel m.buckets)).contains k

theorem Std.DHashMap.Internal.Raw.mem_keys_iff_contains_keys {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] {m : Raw α β} {k : α} : k ∈ m.keys ↔ (List.keys (toListModel m.buckets)).contains k = true

theorem Std.DHashMap.Internal.Raw.pairwise_keys_iff_pairwise_keys {α : Type u} {β : α → Type v} [BEq α] [PartialEquivBEq α] {m : Raw α β} : List.Pairwise (fun (a b : α) => (a == b) = false) m.keys ↔ List.Pairwise (fun (a b : α) => (a == b) = false) (List.keys (toListModel m.buckets))

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)

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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 = 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 (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 (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 (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

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

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

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₀.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

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