@[simp]

theorem Std.DHashMap.nodup_keys' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : mp.keys.Nodup

@[simp]

theorem Std.DHashMap.nodup_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : mp.toList.Nodup

theorem Std.DHashMap.equiv_iff_get? {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : DHashMap α β} : m₁.Equiv m₂ ↔ ∀ (i : α), m₁.get? i = m₂.get? i

theorem Std.DHashMap.toList_ofList_perm {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List ((i : α) × β i)} (h : (List.map (fun (x : (i : α) × β i) => x.fst) xs).Nodup) : (ofList xs).toList.Perm xs

@[simp]

theorem Std.DHashMap.ofList_toList_equiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : (ofList mp.toList).Equiv mp

@[instance_reducible]

instance Std.DHashMap.instHasEquiv_projects {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : HasEquiv (DHashMap α β)

Equations

• Std.DHashMap.instHasEquiv_projects = { Equiv := Std.DHashMap.Equiv }

theorem Std.DHashMap.equiv_def {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : DHashMap α β} : m₁ ≈ m₂ ↔ m₁.Equiv m₂

def Std.DHashMap.toSortedList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] (m : DHashMap α β) : List ((i : α) × β i)

Equations

• m.toSortedList = m.toList.mergeSort fun (x1 x2 : (a : α) × β a) => decide (x1.fst ≤ x2.fst)

theorem Std.DHashMap.toSortedList_eq_of {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] {m₁ m₂ : DHashMap α β} (h : m₁.Equiv m₂) : m₁.toSortedList = m₂.toSortedList

@[simp]

theorem Std.DHashMap.toSortedList_eq {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] {m₁ m₂ : DHashMap α β} : m₁.toSortedList = m₂.toSortedList ↔ m₁.Equiv m₂

@[simp]

theorem Std.DHashMap.nodup_toSortedList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [LinearOrder α] : mp.toSortedList.Nodup

@[simp]

theorem Std.DHashMap.pairwise_toSortedList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [LinearOrder α] : List.Pairwise (fun (x1 x2 : (i : α) × β i) => x1.fst ≤ x2.fst) mp.toSortedList

@[simp]

theorem Std.DHashMap.ofList_snoc {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List ((a : α) × β a)} {x : (i : α) × β i} : ofList (xs ++ [x]) = (ofList xs).insert x.fst x.snd

@[simp]

theorem Std.DHashMap.toList_eq_nil_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : mp.toList = [] ↔ mp.Equiv ∅

theorem Std.DHashMap.fold_assoc_aux {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {m₁ m₂ : DHashMap α β} {xs ys : List ((a : α) × β a)} {f : γ → (i : α) → β i → γ} (h : ∀ {acc : γ} {i : α} {x : β i} {j : α} {y : β j}, i ≠ j → f (f acc i x) j y = f (f acc j y) i x) (hx : m₁.toList = xs) (hy : m₂.toList = ys) {acc : γ} {x y : (a : α) × β a} : x ∈ xs ∧ y ∈ xs ∨ x ∈ ys ∧ y ∈ ys → f (f acc x.fst x.snd) y.fst y.snd = f (f acc y.fst y.snd) x.fst x.snd

theorem Std.DHashMap.fold_eq_fold_of_equiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {f : γ → (i : α) → β i → γ} {z : γ} {m₁ m₂ : DHashMap α β} (h_assoc : ∀ {acc : γ} {i : α} {x : β i} {j : α} {y : β j}, i ≠ j → f (f acc i x) j y = f (f acc j y) i x) (h : m₁.Equiv m₂) : fold f z m₁ = fold f z m₂

def Std.DHashMap.decideEquiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [(i : α) → DecidableEq (β i)] (m₁ m₂ : DHashMap α β) : Bool

Equations

• m₁.decideEquiv m₂ = decide (m₁.size = m₂.size ∧ Std.DHashMap.fold (fun (acc : Bool) (i : α) (x : β i) => acc && decide (m₂.get? i = some x)) true m₁ = true)

theorem Std.DHashMap.mem_of_get?_eq_some {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} {x : β i} (h : mp.get? i = some x) : i ∈ mp

theorem Std.DHashMap.get?_eq_some_iff_find?_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} {x : β i} : mp.get? i = some x ↔ List.find? (fun (x : (i : α) × β i) => decide (x.fst = i)) mp.toList = some ⟨i, x⟩

@[simp]

theorem Std.DHashMap.get_keys_eq_get_keys_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i j : ℕ} {h₁ : i < mp.keys.length} {h₂ : j < mp.keys.length} : mp.keys[i] = mp.keys[j] ↔ i = j

@[simp]

theorem Std.DHashMap.fst_get_toList_eq_fst_get_toList_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i j : ℕ} {h₁ : i < mp.toList.length} {h₂ : j < mp.toList.length} : mp.toList[i].fst = mp.toList[j].fst ↔ i = j

theorem Std.DHashMap.equiv_iff_decideEquiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hb : (i : α) → DecidableEq (β i)] {m₁ m₂ : DHashMap α β} : m₁.Equiv m₂ ↔ m₁.decideEquiv m₂ = true

@[instance_reducible]

instance Std.DHashMap.instDecidableEquivOfDecidableEq_projects {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hh : (i : α) → DecidableEq (β i)] {m₁ m₂ : DHashMap α β} : Decidable (m₁.Equiv m₂)

Equations

• Std.DHashMap.instDecidableEquivOfDecidableEq_projects = match h : m₁.decideEquiv m₂ with | true => isTrue ⋯ | false => isFalse ⋯

@[simp]

theorem Std.DHashMap.decideEquiv_eq {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hh : (i : α) → DecidableEq (β i)] {m₁ m₂ : DHashMap α β} : m₁.decideEquiv m₂ = decide (m₁.Equiv m₂)

def Std.DHashMap.toSortedKeys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] (m : DHashMap α β) : List α

Equations

• m.toSortedKeys = List.map (fun (x : (i : α) × β i) => x.fst) m.toSortedList

@[simp]

theorem Std.DHashMap.nodup_toSortedKeys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [LinearOrder α] : mp.toSortedKeys.Nodup

@[simp]

theorem Std.DHashMap.sortedLE_toSortedKeys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [LinearOrder α] : mp.toSortedKeys.SortedLE

@[simp]

theorem Std.DHashMap.toSortedList_perm_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [LinearOrder α] : mp.toSortedList.Perm mp.toList

@[simp]

theorem Std.DHashMap.toList_perm_toSortedList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [LinearOrder α] : mp.toList.Perm mp.toSortedList

@[simp]

theorem Std.DHashMap.mem_toSortedList_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {x : (i : α) × β i} [LinearOrder α] : x ∈ mp.toSortedList ↔ x ∈ mp.toList

theorem Std.DHashMap.equiv_iff_toSortedList_perm {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] {m₁ m₂ : DHashMap α β} : m₁.Equiv m₂ ↔ m₁.toSortedList.Perm m₂.toSortedList

@[simp]

theorem Std.DHashMap.nodup_map_fst_toSortedList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [LinearOrder α] : (List.map (fun (x : (i : α) × β i) => x.fst) mp.toSortedList).Nodup

@[simp]

theorem Std.DHashMap.mem_toSortedKeys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} [LinearOrder α] : i ∈ mp.toSortedKeys ↔ i ∈ mp

@[simp]

theorem Std.DHashMap.toSortedList_perm_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] {m₁ m₂ : DHashMap α β} : m₁.toSortedList.Perm m₂.toSortedList ↔ m₁.Equiv m₂

theorem Std.DHashMap.toSortedKeys_eq_of_equiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] {m₁ m₂ : DHashMap α β} (h : m₁.Equiv m₂) : m₁.toSortedKeys = m₂.toSortedKeys

@[simp]

theorem Std.DHashMap.toSortedKeys_eq_iff_of_subsingleton {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] {m₁ m₂ : DHashMap α β} [hb : ∀ (i : α), Subsingleton (β i)] : m₁.toSortedKeys = m₂.toSortedKeys ↔ m₁.Equiv m₂

@[simp]

theorem Std.DHashMap.toSortedList_eq_nil_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [LinearOrder α] : mp.toSortedList = [] ↔ mp.Equiv ∅

@[simp]

theorem Std.DHashMap.toSortedKeys_eq_nil_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [LinearOrder α] : mp.toSortedKeys = [] ↔ mp.Equiv ∅

@[simp]

theorem Std.DHashMap.all_def {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (a : α) → β a → Bool} : mp.all p = decide (∀ x ∈ mp.toList, p x.fst x.snd = true)

@[simp]

theorem Std.DHashMap.mem_toList_iff_get?_eq_some' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} (x : (i : α) × β i) : x ∈ mp.toList ↔ mp.get? x.fst = some x.snd

def Std.DHashMap.modifyMany {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : DHashMap α β) : List ((i : α) × (β i → β i)) → DHashMap α β

Equations

• mp.modifyMany [] = mp
• mp.modifyMany (⟨i, f⟩ :: xs) = (mp.modify i f).modifyMany xs

theorem Std.DHashMap.modify_equiv_modify_of_equiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : DHashMap α β} {i : α} {x : β i → β i} (h : m₁.Equiv m₂) : (m₁.modify i x).Equiv (m₂.modify i x)

theorem Std.DHashMap.modifyMany_equiv_modifyMany_of_equiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : DHashMap α β} {xs : List ((i : α) × (β i → β i))} (h : m₁.Equiv m₂) : (m₁.modifyMany xs).Equiv (m₂.modifyMany xs)

theorem Std.DHashMap.mem_iff_get?_eq_some {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} : i ∈ mp ↔ ∃ (x : β i), mp.get? i = some x

theorem Std.DHashMap.get?_eq_ite {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} [hb : Inhabited (β i)] : mp.get? i = if i ∈ mp then some (mp.get! i) else none

theorem Std.DHashMap.get?_ofList_eq_some_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List ((i : α) × β i)} {i : α} {x : β i} (h : (List.map (fun (x : (i : α) × β i) => x.fst) xs).Nodup) : (ofList xs).get? i = some x ↔ ⟨i, x⟩ ∈ xs

@[simp]

theorem Std.DHashMap.get?_eq_some_get!_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} [hb : Inhabited (β i)] : mp.get? i = some (mp.get! i) ↔ i ∈ mp

@[simp]

theorem Std.DHashMap.get?_eq_some_get?_get! {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} [hb : Inhabited (β i)] : mp.get? i = some (mp.get? i).get! ↔ i ∈ mp

theorem Std.DHashMap.ofList_equiv_ofList_of_nodup_and_perm {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs ys : List ((i : α) × β i)} (hx : (List.map (fun (x : (i : α) × β i) => x.fst) xs).Nodup) (hy : (List.map (fun (x : (i : α) × β i) => x.fst) ys).Nodup) (h : xs.Perm ys) : (ofList xs).Equiv (ofList ys)

@[simp]

theorem Std.DHashMap.ofList_toSortedList_equiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [ha : LinearOrder α] : (ofList mp.toSortedList).Equiv mp

theorem Std.DHashMap.Internal.distinctKeys_def {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] {xs : List ((i : α) × β i)} : Internal.List.DistinctKeys xs ↔ List.Pairwise (fun (a b : α) => (a == b) = false) (Internal.List.keys xs)

theorem Std.DHashMap.Internal.distinctKeys_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] {xs : List ((i : α) × β i)} : Internal.List.DistinctKeys xs ↔ (List.map (fun (x : (i : α) × β i) => x.fst) xs).Nodup

def Std.DHashMap.Internal.AssocList.foldlWith {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] {γ : Sort u_4} (xs : AssocList α β) (f : γ → (i : α) → (x : β i) → getCast? i xs = some x → γ) (z : γ) (h : (List.map (fun (x : (a : α) × β a) => x.fst) xs.toList).Nodup) : γ

Equations

• Std.DHashMap.Internal.AssocList.nil.foldlWith f_2 z h_2 = z
• (Std.DHashMap.Internal.AssocList.cons i x ys).foldlWith f_2 z h_2 = ys.foldlWith (fun (acc : γ) (j : α) (y : β j) (h₂ : Std.DHashMap.Internal.AssocList.getCast? j ys = some y) => f_2 acc j y ⋯) (f_2 z i x ⋯) ⋯

theorem Std.DHashMap.Internal.foldlWith_eq_foldl {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] {γ : Type u_4} [hb : (i : α) → DecidableEq (β i)] {xs : AssocList α β} {f : γ → (i : α) → (x : β i) → AssocList.getCast? i xs = some x → γ} {z : γ} (h : (List.map (fun (x : (a : α) × β a) => x.fst) xs.toList).Nodup) : xs.foldlWith f z h = AssocList.foldl (fun (acc : γ) (i : α) (x : β i) => if h : AssocList.getCast? i xs = some x then f acc i x h else z) z xs

theorem Std.DHashMap.Internal.toList_eq_flat_buckets {α : Type u_1} {β : α → Type u_2} {mp : Raw α β} : mp.toList = List.flatMap (fun (x : AssocList α β) => x.toList) mp.buckets.toList

theorem Std.DHashMap.Internal.bucket_nodup_keys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) {b : AssocList α β} (h : b ∈ mp.buckets) : (List.map (fun (x : (a : α) × β a) => x.fst) b.toList).Nodup

theorem Std.DHashMap.Internal.mem_toList_of_mem_bucket {α : Type u_1} {β : α → Type u_2} {mp : Raw α β} {x : (a : α) × β a} {b : AssocList α β} (h₁ : b ∈ mp.buckets) (h₂ : x ∈ b.toList) : x ∈ mp.toList

theorem Std.DHashMap.Raw.WF.get?_eq {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) : mp.get? = { inner := mp, wf := wf }.get?

theorem Std.DHashMap.Raw.WF.get?_eq_some_iff_mem_bucket {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) {i : α} {x : β i} : mp.get? i = some x ↔ ∃ b ∈ mp.buckets, ⟨i, x⟩ ∈ b.toList

theorem Std.DHashMap.Raw.WF.get?_eq_some_of_mem_bucket {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) {b : Internal.AssocList α β} {i : α} {x : β i} (h₁ : b ∈ mp.buckets) (h₂ : ⟨i, x⟩ ∈ b.toList) : mp.get? i = some x

theorem Std.DHashMap.Raw.WF.mem_bucket_of_get?_eq_some {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) {i : α} {x : β i} (h : mp.get? i = some x) : ∃ b ∈ mp.buckets, ⟨i, x⟩ ∈ b.toList

def Std.DHashMap.Internal.AssocList.ofList {α : Type u_1} {β : α → Type u_2} : List ((i : α) × β i) → AssocList α β

Equations

• Std.DHashMap.Internal.AssocList.ofList [] = Std.DHashMap.Internal.AssocList.nil
• Std.DHashMap.Internal.AssocList.ofList (x_1 :: xs) = Std.DHashMap.Internal.AssocList.cons x_1.fst x_1.snd (Std.DHashMap.Internal.AssocList.ofList xs)

@[simp]

theorem Std.DHashMap.Internal.AssocList.ofList_toList {α : Type u_1} {β : α → Type u_2} {xs : AssocList α β} : ofList xs.toList = xs

@[simp]

theorem Std.DHashMap.Internal.AssocList.toList_ofList {α : Type u_1} {β : α → Type u_2} {xs : List ((i : α) × β i)} : (ofList xs).toList = xs

def Std.DHashMap.Raw.foldWith {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} (mp : Raw α β) (wf : mp.WF) (f : γ → (i : α) → (x : β i) → mp.get? i = some x → γ) (z : γ) : γ

Equations

• mp.foldWith wf f z = (fun (x : γ → (x : Std.DHashMap.Internal.AssocList α β) → x ∈ mp.buckets → γ) => mp.buckets.foldlWith x z) fun (acc : γ) (xs : Std.DHashMap.Internal.AssocList α β) (h₁ : xs ∈ mp.buckets) => xs.foldlWith (fun (acc' : γ) (i' : α) (x : β i') (h₂ : Std.DHashMap.Internal.AssocList.getCast? i' xs = some x) => f acc' i' x ⋯) acc ⋯

theorem Std.DHashMap.Raw.WF.distinctKeys_bucket {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) {b : Internal.AssocList α β} (hb : b ∈ mp.buckets) : Internal.List.DistinctKeys b.toList

theorem Std.DHashMap.Raw.WF.distinctKeys_getElem_buckets {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) {i : ℕ} {h : i < mp.buckets.size} : Internal.List.DistinctKeys mp.buckets[i].toList

theorem Std.DHashMap.Raw.WF.nodup_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) : mp.toList.Nodup

theorem Std.DHashMap.Raw.WF.index_eq_of_mem_bucket {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) {i j : ℕ} {x : (a : α) × β a} {hh₃ : i < mp.buckets.size} {hh₄ : j < mp.buckets.size} (h₁ : x ∈ mp.buckets[i].toList) (h₂ : x ∈ mp.buckets[j].toList) : i = j

theorem Std.DHashMap.Raw.foldWith_eq_foldl_toList' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {mp : Raw α β} {wf : mp.WF} {f : γ → (i : α) → (x : β i) → mp.get? i = some x → γ} {z : γ} [hh₃ : (i : α) → DecidableEq (β i)] : mp.foldWith wf f z = List.foldl (fun (acc : γ) (x : (a : α) × β a) => if h : mp.get? x.fst = some x.snd then f acc x.fst x.snd h else z) z mp.toList

theorem Std.DHashMap.Raw.foldWith_eq_fold {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {mp : Raw α β} {wf : mp.WF} {f : γ → (i : α) → (x : β i) → mp.get? i = some x → γ} {z : γ} [hb : (i : α) → DecidableEq (β i)] : mp.foldWith wf f z = fold (fun (acc : γ) (i : α) (x : β i) => if h : mp.get? i = some x then f acc i x h else z) z mp

@[simp]

theorem Std.DHashMap.Raw.fold_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {z : γ} {f : γ → (i : α) → β i → γ} : fold f z ∅ = z

@[simp]

theorem Std.DHashMap.Raw.foldWith_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {z : γ} {wf : ∅.WF} {f : γ → (i : α) → (x : β i) → ∅.get? i = some x → γ} : ∅.foldWith wf f z = z

theorem Std.DHashMap.Raw.foldWith_eq_foldl_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {mp : Raw α β} {wf : mp.WF} {f : γ → (i : α) → (x : β i) → mp.get? i = some x → γ} {z : γ} [(i : α) → DecidableEq (β i)] : mp.foldWith wf f z = List.foldl (fun (acc : γ) (x : (a : α) × β a) => if h : x ∈ mp.toList then f acc x.fst x.snd ⋯ else z) z mp.toList

theorem Std.DHashMap.Raw.foldWith_eq_foldlWith_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {mp : Raw α β} {wf : mp.WF} {f : γ → (i : α) → (x : β i) → mp.get? i = some x → γ} {z : γ} [(i : α) → DecidableEq (β i)] : mp.foldWith wf f z = mp.toList.foldlWith (fun (acc : γ) (x : (a : α) × β a) (h : x ∈ mp.toList) => f acc x.fst x.snd ⋯) z

theorem Std.DHashMap.Raw.size_eq_size_of_mem_iff_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : Raw α β} (wf₁ : mp₁.WF) (wf₂ : mp₂.WF) (h : ∀ (k : α), k ∈ mp₁ ↔ k ∈ mp₂) : mp₁.size = mp₂.size

theorem Std.DHashMap.Raw.mem_of_get?_eq_some {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} {k : α} {x : β k} (wf : mp.WF) (h : mp.get? k = some x) : k ∈ mp

theorem Std.DHashMap.Raw.subset_of_size_eq_and_subset {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : Raw α β} {x : α} (wf₁ : mp₁.WF) (wf₂ : mp₂.WF) (h₁ : mp₁.size = mp₂.size) (h₂ : ∀ x ∈ mp₁, x ∈ mp₂) (hx : x ∈ mp₂) : x ∈ mp₁

theorem Std.DHashMap.Raw.foldWith_and_iff_forall {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} {f : (i : α) → (x : β i) → mp.get? i = some x → Prop} (wf : mp.WF) : mp.foldWith wf (fun (acc : Prop) (i : α) (x : β i) (h : mp.get? i = some x) => acc ∧ f i x h) True ↔ ∀ (i : α) (x : β i) (h : mp.get? i = some x), f i x h

theorem Std.DHashMap.Raw.foldWith_bool_and_iff_forall {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} {f : (i : α) → (x : β i) → mp.get? i = some x → Bool} (wf : mp.WF) : mp.foldWith wf (fun (acc : Bool) (i : α) (x : β i) (h : mp.get? i = some x) => acc && f i x h) true = true ↔ ∀ (i : α) (x : β i) (h : mp.get? i = some x), f i x h = true

theorem Std.DHashMap.equiv_iff_mem_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : DHashMap α β} : mp₁.Equiv mp₂ ↔ ∀ (x : (a : α) × β a), x ∈ mp₁.toList ↔ x ∈ mp₂.toList

theorem Std.DHashMap.mem_toList_insert {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i j : α} {x : β i} {y : β j} : ⟨i, x⟩ ∈ (mp.insert j y).toList ↔ if i = j then x ≍ y else ⟨i, x⟩ ∈ mp.toList

theorem Std.DHashMap.mem_toList_erase {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i j : α} {x : β i} : ⟨i, x⟩ ∈ (mp.erase j).toList ↔ i ≠ j ∧ ⟨i, x⟩ ∈ mp.toList

theorem Std.DHashMap.mem_toList_insert_erase {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i j : α} {x : β i} {y : β j} : ⟨i, x⟩ ∈ ((mp.erase j).insert j y).toList ↔ if i = j then x ≍ y else ⟨i, x⟩ ∈ mp.toList

theorem Std.DHashMap.keys_eq_map_fst_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : mp.keys = List.map (fun (x : (a : α) × β a) => x.fst) mp.toList

theorem Std.DHashMap.ind {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {p : DHashMap α β → Prop} (h₁ : ∀ (mp : DHashMap α β), mp.isEmpty = true → p mp) (h₂ : ∀ (mp₁ mp₂ : DHashMap α β) (i : α) (x : β i), i ∉ mp₁ → (mp₁.insert i x).Equiv mp₂ → p mp₁ → p mp₂) (mp : DHashMap α β) : p mp

theorem Std.DHashMap.isEmpty_iff_equiv_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : mp.isEmpty = true ↔ mp.Equiv ∅

theorem Std.DHashMap.toList_eq_nil_iff_isEmpty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : mp.toList = [] ↔ mp.isEmpty = true

theorem Std.DHashMap.toList_eq_nil_of_isEmpty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} (h : mp.isEmpty = true) : mp.toList = []

theorem Std.DHashMap.fold_eq_of_isEmpty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {γ : Type u_4} {f : γ → (i : α) → β i → γ} {z : γ} (h : mp.isEmpty = true) : fold f z mp = z

@[simp]

theorem Std.DHashMap.fold_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {f : γ → (i : α) → β i → γ} {z : γ} : fold f z ∅ = z

@[simp]

theorem Std.DHashMap.size_eq_zero_iff_isEmpty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : mp.size = 0 ↔ mp.isEmpty = true

@[simp]

theorem Std.DHashMap.size_eq_zero_of_isEmpty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} (h : mp.isEmpty = true) : mp.size = 0

theorem Std.DHashMap.toList_insert_eq_of_isEmpty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} {x : β i} (h : mp.isEmpty = true) : (mp.insert i x).toList = [⟨i, x⟩]

theorem Std.DHashMap.toList_insert_perm_cons_of_not_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} {x : β i} (h : i ∉ mp) : (mp.insert i x).toList.Perm (⟨i, x⟩ :: mp.toList)

@[simp]

theorem Std.DHashMap.keys_eq_nil_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : mp.keys = [] ↔ mp.isEmpty = true

def Std.DHashMap.count {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : DHashMap α β) (p : (i : α) → β i → Bool) : ℕ

Equations

• mp.count p = Std.DHashMap.fold (fun (acc : ℕ) (i : α) (x : β i) => if p i x = true then acc + 1 else acc) 0 mp

theorem Std.DHashMap.isEmpty_filter_of_isEmpty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (a : α) → β a → Bool} (h : mp.isEmpty = true) : (filter p mp).isEmpty = true

theorem Std.DHashMap.count_eq_zero_of_isEmpty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (i : α) → β i → Bool} (h : mp.isEmpty = true) : mp.count p = 0

theorem Std.DHashMap.insert_erase_equiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} {x : β i} (h : mp.get? i = some x) : ((mp.erase i).insert i x).Equiv mp

theorem Std.DHashMap.equiv_of_insert_equiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : DHashMap α β} {i : α} {x : β i} (h₁ : (mp₁.insert i x).Equiv (mp₂.insert i x)) (h₂ : i ∉ mp₁) (h₃ : i ∉ mp₂) : mp₁.Equiv mp₂

theorem Std.DHashMap.size_filter_congr_of_equiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : DHashMap α β} {p : (a : α) → β a → Bool} (h : mp₁.Equiv mp₂) : (filter p mp₁).size = (filter p mp₂).size

theorem Std.DHashMap.filter_insert_equiv_of_not_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (a : α) → β a → Bool} {i : α} {x : β i} (h : i ∉ mp) : (filter p (mp.insert i x)).Equiv (if p i x = true then (filter p mp).insert i x else filter p mp)

theorem Std.DHashMap.size_filter_insert_of_not_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (a : α) → β a → Bool} {i : α} {x : β i} (h : i ∉ mp) : (filter p (mp.insert i x)).size = (filter p mp).size + if p i x = true then 1 else 0

theorem Std.DHashMap.get?_eq_some_iff_mem_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} {x : β i} : mp.get? i = some x ↔ ⟨i, x⟩ ∈ mp.toList

theorem Std.DHashMap.get?_eq_some_iff_toList_eq_append {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} {x : β i} : mp.get? i = some x ↔ ∃ (xs : List ((a : α) × β a)) (ys : List ((a : α) × β a)), ⟨i, x⟩ ∉ xs ∧ ⟨i, x⟩ ∉ ys ∧ mp.toList = xs ++ ⟨i, x⟩ :: ys

theorem Std.DHashMap.count_eq_sum_map_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (i : α) → β i → Bool} : mp.count p = (List.map (fun (x : (a : α) × β a) => if p x.fst x.snd = true then 1 else 0) mp.toList).sum

theorem Std.DHashMap.equiv_erase_of_insert_equiv {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : DHashMap α β} {i : α} {x : β i} (h₁ : (mp₁.insert i x).Equiv mp₂) (h₂ : i ∉ mp₁) : mp₁.Equiv (mp₂.erase i)

theorem Std.DHashMap.toList_erase_perm {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [hb : (i : α) → DecidableEq (β i)] {i : α} {x : β i} (h : mp.get? i = some x) : (mp.erase i).toList.Perm (mp.toList.erase ⟨i, x⟩)

@[simp]

theorem Std.DHashMap.size_filter_eq_count {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (a : α) → β a → Bool} : (filter p mp).size = mp.count p

theorem Std.DHashMap.count_eq_size_filter {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (i : α) → β i → Bool} : mp.count p = (filter p mp).size

@[simp]

theorem Std.DHashMap.count_le_size {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (i : α) → β i → Bool} : mp.count p ≤ mp.size

theorem Std.DHashMap.count_eq_zero_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (i : α) → β i → Bool} : mp.count p = 0 ↔ ∀ (i : α) (x : β i), mp.get? i = some x → ¬p i x = true

@[simp]

theorem Std.DHashMap.count_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {p : (i : α) → β i → Bool} : ∅.count p = 0

theorem Std.DHashMap.count_insert {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {p : (i : α) → β i → Bool} {i : α} {x : β i} (h : i ∉ mp) : (mp.insert i x).count p = mp.count p + if p i x = true then 1 else 0

theorem Std.DHashMap.count_eq_of_perm {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : DHashMap α β} {p : (i : α) → β i → Bool} (h : mp₁.Equiv mp₂) : mp₁.count p = mp₂.count p

@[simp]

theorem Std.DHashMap.length_toSortedList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [ha : LinearOrder α] : mp.toSortedList.length = mp.size

@[simp]

theorem Std.DHashMap.length_toSortedKeys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} [ha : LinearOrder α] : mp.toSortedKeys.length = mp.size

theorem Std.DHashMap.eq_iff_inner {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : DHashMap α β} : mp₁ = mp₂ ↔ mp₁.inner = mp₂.inner

theorem Std.DHashMap.modify_of_notMem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} {f : β i → β i} (h : i ∉ mp) : mp.modify i f = mp

theorem Std.DHashMap.mem_iff_mem_inner {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {x : α} : x ∈ mp ↔ x ∈ mp.inner

@[simp]

theorem Std.DHashMap.mem_mk_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {x : α} {mp : Raw α β} {wf : mp.WF} : x ∈ { inner := mp, wf := wf } ↔ x ∈ mp

@[simp]

theorem Std.DHashMap.mk_equiv_mk_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : Raw α β} {wf₁ : mp₁.WF} {wf₂ : mp₂.WF} : { inner := mp₁, wf := wf₁ }.Equiv { inner := mp₂, wf := wf₂ } ↔ mp₁.Equiv mp₂

@[simp]

theorem Std.DHashMap.insert_mk {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} {wf : mp.WF} {i : α} {x : β i} : { inner := mp, wf := wf }.insert i x = { inner := mp.insert i x, wf := ⋯ }

@[simp]

theorem Std.DHashMap.toList_mk {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} {wf : mp.WF} : { inner := mp, wf := wf }.toList = mp.toList

theorem Std.DHashMap.Raw.ind {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {p : (mp : Raw α β) → mp.WF → Prop} (h₁ : ∀ (mp : Raw α β) (wf : mp.WF), mp.isEmpty = true → p mp wf) (h₂ : ∀ (mp₁ mp₂ : Raw α β) (wf₁ : mp₁.WF) (wf₂ : mp₂.WF) (i : α) (x : β i), i ∉ mp₁ → (mp₁.insert i x).Equiv mp₂ → p mp₁ wf₁ → p mp₂ wf₂) (mp : Raw α β) (wf : mp.WF) : p mp wf

theorem Std.DHashMap.Raw.toList_eq_nil_iff_isEmpty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) : mp.toList = [] ↔ mp.isEmpty = true

theorem Std.DHashMap.Raw.toList_eq_nil_of_isEmpty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} (wf : mp.WF) (h₁ : mp.isEmpty = true) : mp.toList = []

theorem Std.DHashMap.Raw.le_foldWith_max {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {mp : Raw α β} [hh : LinearOrder γ] {i : α} {x : β i} {z : γ} {f : (i : α) → (x : β i) → mp.get? i = some x → γ} (wf : mp.WF) (h : mp.get? i = some x) : f i x h ≤ mp.foldWith wf (fun (acc : γ) (i : α) (x : β i) (h : mp.get? i = some x) => max acc (f i x h)) z

@[simp]

theorem Std.DHashMap.Raw.assocList_foldr_nil {α : Type u_1} {β : α → Type u_2} {γ : Type u_4} {f : (x : α) → β x → γ → γ} {z : γ} : Internal.AssocList.foldr f z Internal.AssocList.nil = z

@[simp]

theorem Std.DHashMap.Raw.assocList_foldr_cons {α : Type u_1} {β : α → Type u_2} {γ : Type u_4} {f : (x : α) → β x → γ → γ} {k : α} {x : β k} {z : γ} {bs : Internal.AssocList α β} : Internal.AssocList.foldr f z (Internal.AssocList.cons k x bs) = f k x (Internal.AssocList.foldr f z bs)

@[simp]

theorem Std.DHashMap.Raw.assocList_foldr_eq_foldr_toList {α : Type u_1} {β : α → Type u_2} {γ : Type u_4} {bs : Internal.AssocList α β} {f : (x : α) → β x → γ → γ} {z : γ} : Internal.AssocList.foldr f z bs = List.foldr (fun (x : (a : α) × β a) => f x.fst x.snd) z bs.toList

theorem Std.DHashMap.Raw.foldr_foldr_eq_foldr_flatMap_buckets_list {α : Type u_1} {β : α → Type u_2} {bs : List (Internal.AssocList α β)} : List.foldr (fun (x : Internal.AssocList α β) (y : List (Sigma β)) => Internal.AssocList.foldr (fun (a : α) (b : β a) (d : List (Sigma β)) => ⟨a, b⟩ :: d) y x) [] bs = List.flatMap (fun (x : Internal.AssocList α β) => x.toList) bs

theorem Std.DHashMap.Raw.foldr_foldr_eq_foldr_flatMap_buckets_array {α : Type u_1} {β : α → Type u_2} {bs : Array (Internal.AssocList α β)} : Array.foldr (fun (x : Internal.AssocList α β) (y : List (Sigma β)) => Internal.AssocList.foldr (fun (a : α) (b : β a) (d : List (Sigma β)) => ⟨a, b⟩ :: d) y x) [] bs = List.flatMap (fun (x : Internal.AssocList α β) => x.toList) bs.toList

@[simp]

theorem Std.DHashMap.Raw.assocList_foldrM_Id_eq_foldr_toList {α : Type u_1} {β : α → Type u_2} {γ : Type u_4} {bs : Internal.AssocList α β} {f : (x : α) → β x → γ → γ} {z : γ} : Internal.AssocList.foldrM f z bs = List.foldr (fun (x : (a : α) × β a) => f x.fst x.snd) z bs.toList

theorem Std.DHashMap.Raw.assocList_foldrM_eq! : @Internal.AssocList.foldrM = fun (α : Type u) (β : α → Type v) (γ : Type w) (m : Type w → Type w) [H : Monad m] (f : (x : α) → β x → γ → m γ) (z : γ) (bs : Internal.AssocList α β) => if h : m = Id ∧ H ≍ Id.instMonad then And.casesOn h fun (left : m = Id) (right : H ≍ Id.instMonad) => Eq.ndrec (motive := fun (m : Type w → Type w) => [H : Monad m] → ((x : α) → β x → γ → m γ) → H ≍ Id.instMonad → m γ) (fun [Monad Id] (f : (x : α) → β x → γ → Id γ) (right : H ≍ Id.instMonad) => List.foldr (fun (x : (a : α) × β a) => f x.fst x.snd) z bs.toList) ⋯ f right else Internal.AssocList.foldrM f z bs

theorem Std.DHashMap.Raw.toList_eq_flatMap_buckets {α : Type u_1} {β : α → Type u_2} {mp : Raw α β} : mp.toList = List.flatMap (fun (x : Internal.AssocList α β) => x.toList) mp.buckets.toList

theorem Std.DHashMap.Raw.of_getCast?_eq_some {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] {xs : Internal.AssocList α β} {k : α} {x : β k} (h : Internal.AssocList.getCast? k xs = some x) : ⟨k, x⟩ ∈ xs.toList

theorem Std.DHashMap.Raw.distinct_keys_of_mem_buckets {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} {xs : Internal.AssocList α β} (wf : mp.WF) (h : xs ∈ mp.buckets) (k : α) (x y : β k) : ⟨k, x⟩ ∈ xs.toList → ⟨k, y⟩ ∈ xs.toList → x = y

theorem Std.DHashMap.Raw.distinct_keys_of_mem_toList_buckets {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} {xs : Internal.AssocList α β} (wf : mp.WF) (h : xs ∈ mp.buckets.toList) (k : α) (x y : β k) : ⟨k, x⟩ ∈ xs.toList → ⟨k, y⟩ ∈ xs.toList → x = y

theorem Std.DHashMap.Raw.getCast?_eq_some_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] {xs : Internal.AssocList α β} {k : α} {x : β k} (h : ∀ (k : α) (x y : β k), ⟨k, x⟩ ∈ xs.toList → ⟨k, y⟩ ∈ xs.toList → x = y) : Internal.AssocList.getCast? k xs = some x ↔ ⟨k, x⟩ ∈ xs.toList

theorem Std.DHashMap.Raw.getCast?_eq_some_iff_of_mem_buckets {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} {xs : Internal.AssocList α β} {k : α} {x : β k} (wf : mp.WF) (h : xs ∈ mp.buckets) : Internal.AssocList.getCast? k xs = some x ↔ ⟨k, x⟩ ∈ xs.toList

theorem Std.DHashMap.Raw.get?_eq_some_iff_mem_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Raw α β} {k : α} {x : β k} (wf : mp.WF) : mp.get? k = some x ↔ ⟨k, x⟩ ∈ mp.toList

@[simp]

theorem Std.DHashMap.Raw.assocList_toList_eq_nil_iff {α : Type u_1} {β : α → Type u_2} {xs : Internal.AssocList α β} : xs.toList = [] ↔ xs = Internal.AssocList.nil

@[simp]

theorem Std.DHashMap.empty_union {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : (∅ ∪ mp).Equiv mp

@[simp]

theorem Std.DHashMap.union_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} : (mp ∪ ∅).Equiv mp