diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index e2052fa530..ad615d0ad2 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -838,9 +838,10 @@ theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α}
   cases as
   simp
 
-theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true := by
+theorem contains_eq_true_of_mem [BEq α] [ReflBEq α] {a : α} {as : Array α} (h : a ∈ as) :
+    as.contains a = true := by
   cases as
-  simpa using h
+  simpa using List.elem_eq_true_of_mem (Array.mem_toList_iff.mpr h)
 
 @[simp] theorem elem_eq_contains [BEq α] {a : α} {xs : Array α} :
     elem a xs = xs.contains a := by
diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean
index 62dae9482c..5ed7a58f06 100644
--- a/src/Std/Data/DHashMap/Basic.lean
+++ b/src/Std/Data/DHashMap/Basic.lean
@@ -298,6 +298,18 @@ This function ensures that the value is used linearly.
   ⟨(Raw₀.Const.insertManyIfNewUnit ⟨m.1, m.2.size_buckets_pos⟩ l).1,
    (Raw₀.Const.insertManyIfNewUnit ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insertIfNew₀ m.2⟩
 
+@[inline, inherit_doc Raw.toArray] def toArray (m : DHashMap α β) :
+    Array ((a : α) × β a) :=
+  m.1.toArray
+
+@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v}
+    (m : DHashMap α (fun _ => β)) : Array (α × β) :=
+  Raw.Const.toArray m.1
+
+@[inline, inherit_doc Raw.keysArray] def keysArray (m : DHashMap α β) :
+    Array α :=
+  m.1.keysArray
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -311,18 +323,6 @@ section Unverified
     else
       (l, r.insert a b)
 
-@[inline, inherit_doc Raw.toArray] def toArray (m : DHashMap α β) :
-    Array ((a : α) × β a) :=
-  m.1.toArray
-
-@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v}
-    (m : DHashMap α (fun _ => β)) : Array (α × β) :=
-  Raw.Const.toArray m.1
-
-@[inline, inherit_doc Raw.keysArray] def keysArray (m : DHashMap α β) :
-    Array α :=
-  m.1.keysArray
-
 @[inline, inherit_doc Raw.values] def values {β : Type v}
     (m : DHashMap α (fun _ => β)) : List β :=
   m.1.values
diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
index 59339f99ce..41520c66de 100644
--- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
@@ -271,4 +271,13 @@ theorem foldr_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a
       (l.toList.map (fun p => f p.1 p.2)) ++ acc := by
   induction l generalizing acc <;> simp_all [AssocList.foldr, AssocList.foldrM]
 
+theorem foldl_push_apply {l : AssocList α β} {acc : Array δ} (f : (a : α) → β a → δ) :
+    l.foldl (fun acc k v => acc.push (f k v)) acc =
+      acc ++ (l.toList.toArray.map (fun p => f p.1 p.2)) := by
+  simp [foldl]
+  induction l generalizing acc with
+  | nil => simp [foldlM]
+  | cons k v tl ih =>
+    simp [foldlM, ih]
+
 end Std.DHashMap.Internal.AssocList
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index ffc2663059..26e9789b32 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -163,6 +163,9 @@ private def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (TSynta
      ⟨`foldRev, (``Raw.foldRev_eq_foldr_toListModel, #[])⟩,
      ⟨`forIn, (``Raw.forIn_eq_forIn_toListModel, #[])⟩,
      ⟨`forM, (``Raw.forM_eq_forM_toListModel, #[])⟩,
+     ⟨`toArray, (``Raw.toArray_eq_toArray_toListModel, #[])⟩,
+     ⟨`keysArray, (``Raw.keysArray_eq_toArray_keys_toListModel, #[])⟩,
+     ⟨`Const.toArray, (``Raw.Const.toArray_eq_toArray_map_toListModel, #[])⟩,
      ⟨`Equiv, (``Raw.equiv_iff_toListModel_perm,
       #[`(_root_.List.Perm.congr_left), `(_root_.List.Perm.congr_right)])⟩]
 
@@ -1108,6 +1111,137 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
 
 end Const
 
+omit [Hashable α] [BEq α] in
+theorem toArray_keys_eq_keysArray :
+    m.1.keys.toArray = m.1.keysArray := by
+  simp_to_model
+
+omit [Hashable α] [BEq α] in
+theorem toList_keysArray_eq_keys :
+    m.1.keysArray.toList = m.1.keys := by
+  simp_to_model
+
+@[simp]
+theorem size_keysArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.keysArray.size = m.1.size := by
+  simp [← toArray_keys_eq_keysArray, h]
+
+@[simp]
+theorem isEmpty_keysArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.keysArray.isEmpty = m.1.isEmpty := by
+  simp [← toArray_keys_eq_keysArray, h]
+
+@[simp]
+theorem contains_keysArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
+    m.1.keysArray.contains k = m.contains k := by
+  simp [← toArray_keys_eq_keysArray, h]
+
+@[simp]
+theorem mem_keysArray [LawfulBEq α] (h : m.1.WF) {k : α} :
+    k ∈ m.1.keysArray ↔ m.contains k := by
+  simp [← toArray_keys_eq_keysArray, h]
+
+theorem forall_mem_keysArray_iff_forall_contains_getKey [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {p : α → Prop} :
+    (∀ k ∈ m.1.keysArray, p k) ↔ ∀ (k : α) (h : m.contains k), p (m.getKey k h) := by
+  simp [← toArray_keys_eq_keysArray, h, forall_mem_keys_iff_forall_contains_getKey]
+
+theorem contains_of_mem_keysArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α}
+    (h' : k ∈ m.1.keysArray) : m.contains k :=
+  (contains_keysArray m h).symm.trans (Array.contains_eq_true_of_mem h')
+
+omit [Hashable α] [BEq α] in
+theorem toArray_toList_eq_toArray :
+    m.1.toList.toArray = m.1.toArray := by
+  simp_to_model
+
+omit [Hashable α] [BEq α] in
+theorem toList_toArray_eq_toList :
+    m.1.toArray.toList = m.1.toList := by
+  simp_to_model
+
+theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] :
+    m.1.toArray.map Sigma.fst = m.1.keysArray := by
+  simp [← toArray_keys_eq_keysArray, ← toArray_toList_eq_toArray, map_fst_toList_eq_keys]
+
+theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.toArray.size = m.1.size := by
+  simp [← toArray_toList_eq_toArray, length_toList, h]
+
+theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.toArray.isEmpty = m.1.isEmpty := by
+  simp [← toArray_toList_eq_toArray, isEmpty_toList, h]
+
+theorem mem_toArray_iff_get?_eq_some [LawfulBEq α] (h : m.1.WF)
+    {k : α} {v : β k} :
+    ⟨k, v⟩ ∈ m.1.toArray ↔ m.get? k = some v := by
+  simp [← toArray_toList_eq_toArray, mem_toList_iff_get?_eq_some, h]
+
+theorem find?_toArray_eq_some_iff_get?_eq_some [LawfulBEq α]
+    (h : m.1.WF) {k : α} {v : β k} :
+    m.1.toArray.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v := by
+  simp [← toArray_toList_eq_toArray, find?_toList_eq_some_iff_get?_eq_some, h]
+
+theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {k : α} :
+    m.1.toArray.find? (·.1 == k) = none ↔ m.contains k = false := by
+  -- does not work if removing the only because it rewrites it away
+  simp only [← toArray_toList_eq_toArray, List.find?_toArray, find?_toList_eq_none_iff_contains_eq_false, h]
+
+namespace Const
+
+variable {β : Type v} (m : Raw₀ α (fun _ => β))
+
+omit [Hashable α] [BEq α] in
+theorem toArray_toList_eq_toArray :
+    (Raw.Const.toList m.1).toArray = Raw.Const.toArray m.1 := by
+  simp_to_model
+
+omit [Hashable α] [BEq α] in
+theorem toList_toArray_eq_toList :
+    (Raw.Const.toArray m.1).toList = Raw.Const.toList m.1 := by
+  simp_to_model
+
+theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] :
+    (Raw.Const.toArray m.1).map Prod.fst = m.1.keysArray := by
+  simp [← toArray_toList_eq_toArray, List.map_toArray, ← toArray_keys_eq_keysArray, map_fst_toList_eq_keys]
+
+theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    (Raw.Const.toArray m.1).size = m.1.size := by
+  simp [← toArray_toList_eq_toArray, length_toList, h]
+
+theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    (Raw.Const.toArray m.1).isEmpty = m.1.isEmpty := by
+  simp [← toArray_toList_eq_toArray, isEmpty_toList, h]
+
+theorem mem_toArray_iff_get?_eq_some [LawfulBEq α] (h : m.1.WF)
+    {k : α} {v : β} :
+    (k, v) ∈ Raw.Const.toArray m.1 ↔ get? m k = some v := by
+  simp [← toArray_toList_eq_toArray, mem_toList_iff_get?_eq_some, h]
+
+theorem get?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {k : α} {v : β} :
+    get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ Raw.Const.toArray m.1 := by
+  simp [← toArray_toList_eq_toArray, get?_eq_some_iff_exists_beq_and_mem_toList, h]
+
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k k' : α} {v : β} :
+    (Raw.Const.toArray m.1).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ get? m k = some v := by
+  simp [← toArray_toList_eq_toArray, List.find?_toArray, find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some, h]
+
+theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {k : α} :
+    (Raw.Const.toArray m.1).find? (·.1 == k) = none ↔ m.contains k = false := by
+  simp only [← toArray_toList_eq_toArray, List.find?_toArray, h, find?_toList_eq_none_iff_contains_eq_false]
+
+theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {k: α} {v : β} :
+    (k, v) ∈ (Raw.Const.toArray m.1) ↔ m.getKey? k = some k ∧ get? m k = some v := by
+  simp [← toArray_toList_eq_toArray, h, mem_toList_iff_getKey?_eq_some_and_get?_eq_some]
+
+end Const
+
 section monadic
 
 -- The types are redefined because fold/for does not need BEq/Hashable
@@ -1203,6 +1337,99 @@ theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
 
 end Const
 
+theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β a → m' δ} {init : δ} :
+    m.1.foldM f init = m.1.toArray.foldlM (fun a b => f a b.1 b.2) init := by
+  simp [← toArray_toList_eq_toArray, foldM_eq_foldlM_toList]
+
+theorem fold_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} :
+    m.1.fold f init = m.1.toArray.foldl (fun a b => f a b.1 b.2) init := by
+  simp [← toArray_toList_eq_toArray, fold_eq_foldl_toList]
+
+theorem foldRevM_eq_foldrM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β a → m' δ} {init : δ} :
+    Raw.Internal.foldRevM f init m.1 = m.1.toArray.foldrM (fun a b => f b a.1 a.2) init := by
+  simp [← toArray_toList_eq_toArray, foldRevM_eq_foldrM_toList]
+
+theorem foldRev_eq_foldr_toArray {f : δ → (a : α) → β a → δ} {init : δ} :
+    Raw.Internal.foldRev f init m.1 = m.1.toArray.foldr (fun a b => f b a.1 a.2) init := by
+  simp [← toArray_toList_eq_toArray, foldRev_eq_foldr_toList]
+
+theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit} :
+    m.1.forM f = m.1.toArray.forM (fun a => f a.1 a.2) := by
+  rw [← toArray_toList_eq_toArray, List.forM_toArray', forM_eq_forM_toList]
+  rfl
+
+theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} :
+    m.1.forIn f init = ForIn.forIn m.1.toArray init (fun a b => f a.1 a.2 b) := by
+  simp [← toArray_toList_eq_toArray, forIn_eq_forIn_toList]
+
+theorem foldM_eq_foldlM_keysArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} :
+    m.1.foldM (fun d a _ => f d a) init = m.1.keysArray.foldlM f init := by
+  simp [← toArray_keys_eq_keysArray, foldM_eq_foldlM_keys]
+
+theorem fold_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
+    m.1.fold (fun d a _ => f d a) init = m.1.keysArray.foldl f init := by
+  simp [← toArray_keys_eq_keysArray, fold_eq_foldl_keys]
+
+theorem foldRevM_eq_foldrM_keysArray [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → m' δ} {init : δ} :
+    Raw.Internal.foldRevM (fun d a _ => f d a) init m.1 =
+      m.1.keysArray.foldrM (fun a b => f b a) init := by
+  simp [← toArray_keys_eq_keysArray, foldRevM_eq_foldrM_keys]
+
+theorem foldRev_eq_foldr_keysArray {f : δ → (a : α) → δ} {init : δ} :
+    Raw.Internal.foldRev (fun d a _ => f d a) init m.1 =
+      m.1.keysArray.foldr (fun a b => f b a) init := by
+  simp [← toArray_keys_eq_keysArray, foldRev_eq_foldr_keys]
+
+theorem forM_eq_forM_keysArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
+    m.1.forM (fun a _ => f a) = m.1.keysArray.forM f := by
+  rw [← toArray_keys_eq_keysArray, List.forM_toArray', forM_eq_forM_keys]
+  rfl
+
+theorem forIn_eq_forIn_keysArray [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.1.forIn (fun a _ d => f a d) init = ForIn.forIn m.1.keysArray init f := by
+  simp [← toArray_keys_eq_keysArray, forIn_eq_forIn_keys]
+
+namespace Const
+
+variable {β : Type v} (m : Raw₀ α (fun _ => β))
+
+theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → β → m' δ} {init : δ} :
+    m.1.foldM f init = (Raw.Const.toArray m.1).foldlM (fun a b => f a b.1 b.2) init := by
+  simp [← toArray_toList_eq_toArray, foldM_eq_foldlM_toList]
+
+theorem fold_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} :
+    m.1.fold f init = (Raw.Const.toArray m.1).foldl (fun a b => f a b.1 b.2) init := by
+  simp [← toArray_toList_eq_toArray, fold_eq_foldl_toList]
+
+theorem foldRevM_eq_foldrM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → β → m' δ} {init : δ} :
+    Raw.Internal.foldRevM f init m.1 =
+      (Raw.Const.toArray m.1).foldrM (fun a b => f b a.1 a.2) init := by
+  simp [← toArray_toList_eq_toArray, foldRevM_eq_foldrM_toList]
+
+theorem foldRev_eq_foldr_toArray {f : δ → α → β → δ} {init : δ} :
+    Raw.Internal.foldRev f init m.1 = (Raw.Const.toArray m.1).foldr (fun a b => f b a.1 a.2) init := by
+  simp [← toArray_toList_eq_toArray, foldRev_eq_foldr_toList]
+
+theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} :
+    m.1.forM f = (Raw.Const.toArray m.1).forM (fun a => f a.1 a.2) := by
+  rw [← toArray_toList_eq_toArray, List.forM_toArray', forM_eq_forM_toList]
+  rfl
+
+theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
+    {f : α → β → δ → m' (ForInStep δ)} {init : δ} :
+    m.1.forIn f init = ForIn.forIn (Raw.Const.toArray m.1) init (fun a b => f a.1 a.2 b) := by
+  simp [← toArray_toList_eq_toArray, forIn_eq_forIn_toList]
+
+end Const
+
 end monadic
 
 section insertMany
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index a9cee5789a..746c7f2db2 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -112,6 +112,16 @@ theorem foldRev_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β
       rw [foldr_cons, ih, AssocList.foldr_apply]
       simp
 
+theorem fold_push_apply {l : Raw α β} {acc : Array γ} (f : (a : α) → β a → γ) :
+    Raw.fold (fun acc k v => acc.push (f k v)) acc l =
+      acc ++ ((toListModel l.buckets).toArray.map (fun p => f p.1 p.2)) := by
+  rw [fold_eq, ← Array.foldl_toList, toListModel]
+  induction l.buckets.toList generalizing acc with
+  | nil => simp
+  | cons x xs ih =>
+      rw [foldl_cons, ih, AssocList.foldl_push_apply]
+      simp
+
 theorem foldRev_cons {l : Raw α β} {acc : List ((a : α) × β a)} :
     Raw.Internal.foldRev (fun acc k v => ⟨k, v⟩ :: acc) acc l = toListModel l.buckets ++ acc := by
   simp [foldRev_cons_apply]
@@ -126,6 +136,20 @@ theorem foldRev_cons_key {l : Raw α β} {acc : List α} :
       List.keys (toListModel l.buckets) ++ acc := by
   rw [foldRev_cons_apply, keys_eq_map]
 
+theorem fold_push {l : Raw α β} {acc : Array ((a : α) × β a)} :
+    Raw.fold (fun acc k v => acc.push ⟨k, v⟩) acc l = acc ++ (toListModel l.buckets).toArray := by
+  simp [fold_push_apply]
+
+theorem fold_push_mk {β : Type v} {l : Raw α (fun _ => β)} {acc : Array (α × β)} :
+    Raw.fold (fun acc k v => acc.push (k, v)) acc l =
+      acc ++ ((toListModel l.buckets).map (fun ⟨k, v⟩ => (k, v))).toArray := by
+  simp [fold_push_apply]
+
+theorem fold_push_key {l : Raw α β} {acc : Array α} :
+    Raw.fold (fun acc k _ => acc.push k) acc l =
+      acc ++ (List.keys (toListModel l.buckets)).toArray := by
+  simp [fold_push_apply, keys_eq_map]
+
 theorem foldM_eq_foldlM_toListModel {δ : Type w} {m : Type w → Type w } [Monad m] [LawfulMonad m]
     {f : δ → (a : α) → β a → m δ} {init : δ} {b : Raw α β} :
     b.foldM f init = (toListModel b.buckets).foldlM (fun a b => f a b.1 b.2) init := by
@@ -177,10 +201,21 @@ theorem Const.toList_eq_toListModel_map {β : Type v} {m : Raw α (fun _ => β)}
     Raw.Const.toList m = (toListModel m.buckets).map (fun ⟨k, v⟩ => ⟨k, v⟩) := by
   simp [Raw.Const.toList, foldRev_cons_mk]
 
-theorem keys_eq_keys_toListModel {m : Raw α β }:
+theorem toArray_eq_toArray_toListModel {m : Raw α β} : m.toArray = (toListModel m.buckets).toArray := by
+  simp [Raw.toArray, fold_push]
+
+theorem Const.toArray_eq_toArray_map_toListModel {β : Type v} {m : Raw α (fun _ => β)} :
+    Raw.Const.toArray m = ((toListModel m.buckets).map (fun ⟨k, v⟩ => (k,v))).toArray := by
+  simp [Raw.Const.toArray, fold_push_mk]
+
+theorem keys_eq_keys_toListModel {m : Raw α β} :
     m.keys = List.keys (toListModel m.buckets) := by
   simp [Raw.keys, foldRev_cons_key, keys_eq_map]
 
+theorem keysArray_eq_toArray_keys_toListModel {m : Raw α β} :
+    m.keysArray = (List.keys (toListModel m.buckets)).toArray := by
+  simp [Raw.keysArray, fold_push_key]
+
 theorem forM_eq_forM_toListModel {l: Raw α β} {m : Type w → Type w} [Monad m] [LawfulMonad m]
     {f : (a : α) → β a → m PUnit} :
     l.forM f = (toListModel l.buckets).forM (fun a => f a.1 a.2) := by
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 0bdabafeb4..1436c5ca56 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -1166,6 +1166,46 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   Raw₀.distinct_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
+@[simp]
+theorem toArray_keys :
+    m.keys.toArray = m.keysArray :=
+  Raw₀.toArray_keys_eq_keysArray ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem toList_keysArray :
+    m.keysArray.toList = m.keys :=
+  Raw₀.toList_keysArray_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem size_keysArray [EquivBEq α] [LawfulHashable α] :
+    m.keysArray.size = m.size :=
+  Raw₀.size_keysArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem isEmpty_keysArray [EquivBEq α] [LawfulHashable α] :
+    m.keysArray.isEmpty = m.isEmpty :=
+  Raw₀.isEmpty_keysArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem contains_keysArray [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.keysArray.contains k = m.contains k :=
+  Raw₀.contains_keysArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem mem_keysArray [LawfulBEq α] {k : α} :
+    k ∈ m.keysArray ↔ k ∈ m :=
+  Raw₀.mem_keysArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem forall_mem_keysArray_iff_forall_mem_getKey [EquivBEq α] [LawfulHashable α]
+    {p : α → Prop} :
+    (∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h) :=
+  Raw₀.forall_mem_keysArray_iff_forall_contains_getKey ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem contains_of_mem_keysArray [EquivBEq α] [LawfulHashable α] {k : α}
+    (h' : k ∈ m.keysArray) : m.contains k :=
+  Raw₀.contains_of_mem_keysArray ⟨m.1, m.2.size_buckets_pos⟩ m.2 h'
+
 @[simp, grind _=_]
 theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
     m.toList.map Sigma.fst = m.keys :=
@@ -1279,6 +1319,103 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
 
 end Const
 
+@[simp]
+theorem toArray_toList :
+    m.toList.toArray = m.toArray :=
+  Raw₀.toArray_toList_eq_toArray ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem toList_toArray :
+    m.toArray.toList = m.toList :=
+  Raw₀.toList_toArray_eq_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] :
+    m.toArray.map Sigma.fst = m.keysArray :=
+  Raw₀.map_fst_toArray_eq_keysArray ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem size_toArray [EquivBEq α] [LawfulHashable α] :
+    m.toArray.size = m.size :=
+  Raw₀.size_toArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] :
+    m.toArray.isEmpty = m.isEmpty :=
+  Raw₀.isEmpty_toArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem mem_toArray_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β k} :
+    ⟨k, v⟩ ∈ m.toArray ↔ m.get? k = some v :=
+  Raw₀.mem_toArray_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toArray_eq_some_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β k} :
+    m.toArray.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v :=
+  Raw₀.find?_toArray_eq_some_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.toArray.find? (·.1 == k) = none ↔ m.contains k = false :=
+  Raw₀.find?_toArray_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+namespace Const
+
+variable {β : Type v} {m : DHashMap α (fun _ => β)}
+
+@[simp]
+theorem toArray_toList :
+    (DHashMap.Const.toList m).toArray = DHashMap.Const.toArray m :=
+  Raw₀.Const.toArray_toList_eq_toArray ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem toList_toArray :
+    (DHashMap.Const.toArray m).toList = DHashMap.Const.toList m :=
+  Raw₀.Const.toList_toArray_eq_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] :
+    (DHashMap.Const.toArray m).map Prod.fst = m.keysArray :=
+  Raw₀.Const.map_fst_toArray_eq_keysArray ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem size_toArray [EquivBEq α] [LawfulHashable α] :
+    (DHashMap.Const.toArray m).size = m.size :=
+  Raw₀.Const.size_toArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] :
+    (DHashMap.Const.toArray m).isEmpty = m.isEmpty :=
+  Raw₀.Const.isEmpty_toArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem mem_toArray_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β} :
+    (k, v) ∈ DHashMap.Const.toArray m ↔ get? m k = some v :=
+  Raw₀.Const.mem_toArray_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem get?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} :
+    get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ DHashMap.Const.toArray m :=
+  Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    [EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
+    (DHashMap.Const.toArray m).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ get? m k = some v :=
+  Raw₀.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    (DHashMap.Const.toArray m).find? (·.1 == k) = none ↔ m.contains k = false :=
+  Raw₀.Const.find?_toArray_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
+    {k: α} {v : β} :
+    (k, v) ∈ DHashMap.Const.toArray m ↔ m.getKey? k = some k ∧ get? m k = some v := by
+  simp [← toArray_toList, mem_toList_iff_getKey?_eq_some_and_get?_eq_some]
+
+end Const
+
 section monadic
 
 variable {m : DHashMap α β} {δ : Type w} {m' : Type w → Type w}
@@ -1399,6 +1536,66 @@ theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m']
 
 end Const
 
+theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β a → m' δ} {init : δ} :
+    m.foldM f init = m.toArray.foldlM (fun a b => f a b.1 b.2) init :=
+  Raw₀.foldM_eq_foldlM_toArray ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem fold_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} :
+    m.fold f init = m.toArray.foldl (fun a b => f a b.1 b.2) init :=
+  Raw₀.fold_eq_foldl_toArray ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit} :
+    m.forM f = m.toArray.forM (fun a => f a.1 a.2) :=
+  Raw₀.forM_eq_forM_toArray ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn f init = ForIn.forIn m.toArray init (fun a b => f a.1 a.2 b) :=
+  Raw₀.forIn_eq_forIn_toArray ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem foldM_eq_foldlM_keysArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} :
+    m.foldM (fun d a _ => f d a) init = m.keysArray.foldlM f init :=
+  Raw₀.foldM_eq_foldlM_keysArray ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem fold_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
+    m.fold (fun d a _ => f d a) init = m.keysArray.foldl f init :=
+  Raw₀.fold_eq_foldl_keysArray ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem forM_eq_forM_keysArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
+    m.forM (fun a _ => f a) = m.keysArray.forM f :=
+  Raw₀.forM_eq_forM_keysArray ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem forIn_eq_forIn_keysArray [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keysArray init f :=
+  Raw₀.forIn_eq_forIn_keysArray ⟨m.1, m.2.size_buckets_pos⟩
+
+namespace Const
+
+variable {β : Type v} {m : DHashMap α (fun _ => β)}
+
+theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → β → m' δ} {init : δ} :
+    m.foldM f init = (DHashMap.Const.toArray m).foldlM (fun a b => f a b.1 b.2) init :=
+  Raw₀.Const.foldM_eq_foldlM_toArray ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem fold_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} :
+    m.fold f init = (DHashMap.Const.toArray m).foldl (fun a b => f a b.1 b.2) init :=
+  Raw₀.Const.fold_eq_foldl_toArray ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} :
+    m.forM f = (DHashMap.Const.toArray m).forM (fun a => f a.1 a.2) :=
+  Raw₀.Const.forM_eq_forM_toArray ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
+    {f : α → β → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn f init = ForIn.forIn (DHashMap.Const.toArray m) init (fun a b => f a.1 a.2 b) :=
+  Raw₀.Const.forIn_eq_forIn_toArray ⟨m.1, m.2.size_buckets_pos⟩
+
+end Const
+
 end monadic
 
 variable {ρ : Type w} [ForIn Id ρ ((a : α) × β a)]
diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean
index ca6b941b36..a27849d46f 100644
--- a/src/Std/Data/DHashMap/Raw.lean
+++ b/src/Std/Data/DHashMap/Raw.lean
@@ -435,10 +435,6 @@ define the `ForM` and `ForIn` instances for `HashMap.Raw`.
 
 end Const
 
-section Unverified
-
-/-! We currently do not provide lemmas for the functions below. -/
-
 /--
 Updates the values of the hash map by applying the given function to all mappings, keeping
 only those mappings where the function returns `some` value.
@@ -473,6 +469,10 @@ only those mappings where the function returns `some` value.
 @[inline] def keysArray (m : Raw α β) : Array α :=
   m.fold (fun acc k _ => acc.push k) (.emptyWithCapacity m.size)
 
+section Unverified
+
+/-! We currently do not provide lemmas for the functions below. -/
+
 /-- Returns a list of all values present in the hash map in some order. -/
 @[inline] def values {β : Type v} (m : Raw α (fun _ => β)) : List β :=
   Internal.foldRev (fun acc _ v => v :: acc) [] m
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 3ee0a5d48d..b3c71fc2a6 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1241,6 +1241,49 @@ theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF
     m.toList.map Sigma.fst = m.keys := by
   apply Raw₀.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩
 
+@[simp]
+theorem toArray_keys (h : m.WF) :
+    m.keys.toArray = m.keysArray :=
+  Raw₀.toArray_keys_eq_keysArray ⟨m, h.size_buckets_pos⟩
+
+@[simp]
+theorem toList_keysArray (h : m.WF) :
+    m.keysArray.toList = m.keys :=
+  Raw₀.toList_keysArray_eq_keys ⟨m, h.size_buckets_pos⟩
+
+@[simp]
+theorem size_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keysArray.size = m.size :=
+  Raw₀.size_keysArray ⟨m, h.size_buckets_pos⟩ h
+
+@[simp]
+theorem isEmpty_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keysArray.isEmpty = m.isEmpty :=
+  Raw₀.isEmpty_keysArray ⟨m, h.size_buckets_pos⟩ h
+
+@[simp]
+theorem contains_keysArray [EquivBEq α] [LawfulHashable α]
+    {k : α} (h : m.WF) :
+    m.keysArray.contains k = m.contains k := by
+  simp_to_raw using Raw₀.contains_keysArray ⟨m, h.size_buckets_pos⟩ h
+
+@[simp]
+theorem mem_keysArray [LawfulBEq α] {k : α} (h : m.WF) :
+    k ∈ m.keysArray ↔ k ∈ m := by
+  rw [mem_iff_contains]
+  simp_to_raw using Raw₀.mem_keysArray ⟨m, h.size_buckets_pos⟩ h
+
+theorem forall_mem_keysArray_iff_forall_mem_getKey [EquivBEq α] [LawfulHashable α]
+    {p : α → Prop} (h : m.WF) :
+    (∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h) := by
+  simp only [mem_iff_contains]
+  simp_to_raw using
+    Raw₀.forall_mem_keysArray_iff_forall_contains_getKey ⟨m, h.size_buckets_pos⟩ h
+
+theorem contains_of_mem_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
+    (h' : k ∈ m.keysArray) : m.contains k := by
+  simp_to_raw using Raw₀.contains_of_mem_keysArray ⟨m, h.size_buckets_pos⟩ h h'
+
 @[simp, grind =]
 theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.length = m.size := by
@@ -1347,6 +1390,105 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
 
 end Const
 
+@[simp]
+theorem toArray_toList (h : m.WF) :
+    m.toList.toArray = m.toArray :=
+  Raw₀.toArray_toList_eq_toArray ⟨m, h.size_buckets_pos⟩
+
+@[simp]
+theorem toList_toArray (h : m.WF) :
+    m.toArray.toList = m.toList :=
+  Raw₀.toList_toArray_eq_toList ⟨m, h.size_buckets_pos⟩
+
+@[simp]
+theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toArray.map Sigma.fst = m.keysArray :=
+  Raw₀.map_fst_toArray_eq_keysArray ⟨m, h.size_buckets_pos⟩
+
+@[simp]
+theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toArray.size = m.size :=
+  Raw₀.size_toArray ⟨m, h.size_buckets_pos⟩ h
+
+@[simp]
+theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toArray.isEmpty = m.isEmpty :=
+  Raw₀.isEmpty_toArray ⟨m, h.size_buckets_pos⟩ h
+
+theorem mem_toArray_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β k} (h : m.WF) :
+    ⟨k, v⟩ ∈ m.toArray ↔ m.get? k = some v := by
+  simp_to_raw using Raw₀.mem_toArray_iff_get?_eq_some ⟨m, h.size_buckets_pos⟩ h
+
+theorem find?_toArray_eq_some_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β k} (h : m.WF) :
+    m.toArray.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v := by
+  simp_to_raw using
+    Raw₀.find?_toArray_eq_some_iff_get?_eq_some ⟨m, h.size_buckets_pos⟩ h
+
+theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} (h : m.WF) :
+    m.toArray.find? (·.1 == k) = none ↔ m.contains k = false := by
+  simp_to_raw using Raw₀.find?_toArray_eq_none_iff_contains_eq_false ⟨m, h.size_buckets_pos⟩ h
+
+namespace Const
+
+variable {β : Type v} {m : Raw α (fun _ => β)}
+
+@[simp]
+theorem toArray_toList (h : m.WF) :
+    (Raw.Const.toList m).toArray = Raw.Const.toArray m :=
+  Raw₀.Const.toArray_toList_eq_toArray ⟨m, h.size_buckets_pos⟩
+
+@[simp]
+theorem toList_toArray (h : m.WF) :
+    (Raw.Const.toArray m).toList = Raw.Const.toList m :=
+  Raw₀.Const.toList_toArray_eq_toList ⟨m, h.size_buckets_pos⟩
+
+@[simp]
+theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    (Raw.Const.toArray m).map Prod.fst = m.keysArray :=
+  Raw₀.Const.map_fst_toArray_eq_keysArray ⟨m, h.size_buckets_pos⟩
+
+@[simp]
+theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    (Raw.Const.toArray m).size = m.size :=
+  Raw₀.Const.size_toArray ⟨m, h.size_buckets_pos⟩ h
+
+@[simp]
+theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    (Raw.Const.toArray m).isEmpty = m.isEmpty :=
+  Raw₀.Const.isEmpty_toArray ⟨m, h.size_buckets_pos⟩ h
+
+theorem mem_toArray_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β} (h : m.WF) :
+    (k, v) ∈ Raw.Const.toArray m ↔ get? m k = some v := by
+  simp_to_raw using Raw₀.Const.mem_toArray_iff_get?_eq_some ⟨m, h.size_buckets_pos⟩ h
+
+theorem get?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} (h : m.WF) :
+    get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ Raw.Const.toArray m := by
+  simp_to_raw using Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toArray ⟨m, h.size_buckets_pos⟩ h
+
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} {v : β} :
+    (Raw.Const.toArray m).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ get? m k = some v := by
+  simp_to_raw using
+    Raw₀.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some ⟨m, h.size_buckets_pos⟩ h
+
+theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} (h : m.WF) :
+    (Raw.Const.toArray m).find? (·.1 == k) = none ↔ m.contains k = false := by
+  simp_to_raw using Raw₀.Const.find?_toArray_eq_none_iff_contains_eq_false ⟨m, h.size_buckets_pos⟩ h
+
+theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {k: α} {v : β} :
+    (k, v) ∈ Raw.Const.toArray m ↔ m.getKey? k = some k ∧ get? m k = some v := by
+  simp [← toArray_toList, h, mem_toList_iff_getKey?_eq_some_and_get?_eq_some]
+
+end Const
+
 section monadic
 
 variable {m : Raw α β} {δ : Type w} {m' : Type w → Type w}
@@ -1476,6 +1618,66 @@ theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m'] (h : m.WF)
 
 end Const
 
+theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β a → m' δ} {init : δ} (h : m.WF) :
+    m.foldM f init = m.toArray.foldlM (fun a b => f a b.1 b.2) init :=
+  Raw₀.foldM_eq_foldlM_toArray ⟨m, h.size_buckets_pos⟩
+
+theorem fold_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} (h : m.WF) :
+    m.fold f init = m.toArray.foldl (fun a b => f a b.1 b.2) init :=
+  Raw₀.fold_eq_foldl_toArray ⟨m, h.size_buckets_pos⟩
+
+theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit} (h : m.WF) :
+    m.forM f = m.toArray.forM (fun a => f a.1 a.2) :=
+  Raw₀.forM_eq_forM_toArray ⟨m, h.size_buckets_pos⟩
+
+theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
+    m.forIn f init = ForIn.forIn m.toArray init (fun a b => f a.1 a.2 b) :=
+  Raw₀.forIn_eq_forIn_toArray ⟨m, h.size_buckets_pos⟩
+
+theorem foldM_eq_foldlM_keysArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} (h : m.WF) :
+    m.foldM (fun d a _ => f d a) init = m.keysArray.foldlM f init :=
+  Raw₀.foldM_eq_foldlM_keysArray ⟨m, h.size_buckets_pos⟩
+
+theorem fold_eq_foldl_keysArray {f : δ → α → δ} {init : δ} (h : m.WF) :
+    m.fold (fun d a _ => f d a) init = m.keysArray.foldl f init :=
+  Raw₀.fold_eq_foldl_keysArray ⟨m, h.size_buckets_pos⟩
+
+theorem forM_eq_forM_keysArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} (h : m.WF) :
+    m.forM (fun a _ => f a) = m.keysArray.forM f :=
+  Raw₀.forM_eq_forM_keysArray ⟨m, h.size_buckets_pos⟩
+
+theorem forIn_eq_forIn_keysArray [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
+    m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keysArray init f :=
+  Raw₀.forIn_eq_forIn_keysArray ⟨m, h.size_buckets_pos⟩
+
+namespace Const
+
+variable {β : Type v} {m : Raw α (fun _ => β)}
+
+theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → β → m' δ} {init : δ} (h : m.WF) :
+    m.foldM f init = (Raw.Const.toArray m).foldlM (fun a b => f a b.1 b.2) init :=
+  Raw₀.Const.foldM_eq_foldlM_toArray ⟨m, h.size_buckets_pos⟩
+
+theorem fold_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} (h : m.WF) :
+    m.fold f init = (Raw.Const.toArray m).foldl (fun a b => f a b.1 b.2) init :=
+  Raw₀.Const.fold_eq_foldl_toArray ⟨m, h.size_buckets_pos⟩
+
+theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} (h : m.WF) :
+    m.forM f = (Raw.Const.toArray m).forM (fun a => f a.1 a.2) :=
+  Raw₀.Const.forM_eq_forM_toArray ⟨m, h.size_buckets_pos⟩
+
+theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
+    {f : α → β → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
+    m.forIn f init = ForIn.forIn (Raw.Const.toArray m) init (fun a b => f a.1 a.2 b) :=
+  Raw₀.Const.forIn_eq_forIn_toArray ⟨m, h.size_buckets_pos⟩
+
+end Const
+
 end monadic
 
 section insertMany
diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index 90371fbf8d..0db258bab1 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -247,6 +247,13 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     {ρ : Type w} [ForIn Id ρ α] (m : HashMap α Unit) (l : ρ) : HashMap α Unit :=
   ⟨DHashMap.Const.insertManyIfNewUnit m.inner l⟩
 
+@[inline, inherit_doc DHashMap.Const.toArray] def toArray (m : HashMap α β) :
+    Array (α × β) :=
+  DHashMap.Const.toArray m.inner
+
+@[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
+    Array α :=
+  m.inner.keysArray
 
 section Unverified
 
@@ -257,14 +264,6 @@ section Unverified
   let ⟨l, r⟩ := m.inner.partition f
   ⟨⟨l⟩, ⟨r⟩⟩
 
-@[inline, inherit_doc DHashMap.Const.toArray] def toArray (m : HashMap α β) :
-    Array (α × β) :=
-  DHashMap.Const.toArray m.inner
-
-@[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
-    Array α :=
-  m.inner.keysArray
-
 @[inline, inherit_doc DHashMap.values] def values (m : HashMap α β) : List β :=
   m.inner.values
 
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index dcd63a1d9b..69901c39e7 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -859,6 +859,46 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   DHashMap.distinct_keys
 
+@[simp]
+theorem toArray_keys :
+    m.keys.toArray = m.keysArray :=
+  DHashMap.toArray_keys
+
+@[simp]
+theorem toList_keysArray :
+    m.keysArray.toList = m.keys :=
+  DHashMap.toList_keysArray
+
+@[simp]
+theorem size_keysArray [EquivBEq α] [LawfulHashable α] :
+    m.keysArray.size = m.size :=
+  DHashMap.size_keysArray
+
+@[simp]
+theorem isEmpty_keysArray [EquivBEq α] [LawfulHashable α] :
+    m.keysArray.isEmpty = m.isEmpty :=
+  DHashMap.isEmpty_keysArray
+
+@[simp]
+theorem contains_keysArray [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.keysArray.contains k = m.contains k :=
+  DHashMap.contains_keysArray
+
+@[simp]
+theorem mem_keysArray [LawfulBEq α] {k : α} :
+    k ∈ m.keysArray ↔ k ∈ m :=
+  DHashMap.mem_keysArray
+
+theorem forall_mem_keysArray_iff_forall_mem_getKey [EquivBEq α] [LawfulHashable α]
+    {p : α → Prop} :
+    (∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h) :=
+  DHashMap.forall_mem_keysArray_iff_forall_mem_getKey
+
+theorem contains_of_mem_keysArray [EquivBEq α] [LawfulHashable α] {k : α}
+    (h' : k ∈ m.keysArray) : m.contains k :=
+  DHashMap.contains_of_mem_keysArray h'
+
 @[simp, grind _=_]
 theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
     m.toList.map Prod.fst = m.keys :=
@@ -921,6 +961,57 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
     m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
   DHashMap.Const.distinct_keys_toList
 
+@[simp]
+theorem toArray_toList :
+    m.toList.toArray = m.toArray :=
+  DHashMap.Const.toArray_toList
+
+@[simp]
+theorem toList_toArray :
+    m.toArray.toList = m.toList :=
+  DHashMap.Const.toList_toArray
+
+@[simp]
+theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] :
+    m.toArray.map Prod.fst = m.keysArray :=
+  DHashMap.Const.map_fst_toArray_eq_keysArray
+
+@[simp]
+theorem size_toArray [EquivBEq α] [LawfulHashable α] :
+    m.toArray.size = m.size :=
+  DHashMap.Const.size_toArray
+
+@[simp]
+theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] :
+    m.toArray.isEmpty = m.isEmpty :=
+  DHashMap.Const.isEmpty_toArray
+
+theorem mem_toArray_iff_getElem?_eq_some [LawfulBEq α]
+    {k : α} {v : β} :
+    (k, v) ∈ m.toArray ↔ m[k]? = some v :=
+  DHashMap.Const.mem_toArray_iff_get?_eq_some
+
+theorem getElem?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} :
+    m[k]? = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ m.toArray :=
+  DHashMap.Const.get?_eq_some_iff_exists_beq_and_mem_toArray
+
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    [EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
+    m.toArray.find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ get? m k = some v :=
+  DHashMap.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+
+theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.toArray.find? (·.1 == k) = none ↔ m.contains k = false :=
+  DHashMap.Const.find?_toArray_eq_none_iff_contains_eq_false
+
+theorem mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some [EquivBEq α] [LawfulHashable α]
+    {k: α} {v : β} :
+    (k, v) ∈ m.toArray ↔ m.getKey? k = some k ∧ m[k]? = some v := by
+  simp [← toArray_toList, mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some]
+
 section monadic
 
 variable {m : HashMap α β} {δ : Type w} {m' : Type w → Type w}
@@ -970,6 +1061,42 @@ theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m']
     ForIn.forIn m init (fun a d => f a.1 d) = ForIn.forIn m.keys init f :=
   DHashMap.forIn_eq_forIn_keys
 
+theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → β → m' δ} {init : δ} :
+    m.foldM f init = m.toArray.foldlM (fun a b => f a b.1 b.2) init :=
+  DHashMap.Const.foldM_eq_foldlM_toArray
+
+theorem fold_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} :
+    m.fold f init = m.toArray.foldl (fun a b => f a b.1 b.2) init :=
+  DHashMap.Const.fold_eq_foldl_toArray
+
+theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} :
+    m.forM f = m.toArray.forM (fun a => f a.1 a.2) :=
+  DHashMap.Const.forM_eq_forM_toArray
+
+theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
+    {f : α → β → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn f init = ForIn.forIn m.toArray init (fun a b => f a.1 a.2 b) :=
+  DHashMap.Const.forIn_eq_forIn_toArray
+
+theorem foldM_eq_foldlM_keysArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} :
+    m.foldM (fun d a _ => f d a) init = m.keysArray.foldlM f init :=
+  DHashMap.foldM_eq_foldlM_keysArray
+
+theorem fold_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
+    m.fold (fun d a _ => f d a) init = m.keysArray.foldl f init :=
+  DHashMap.fold_eq_foldl_keysArray
+
+theorem forM_eq_forM_keysArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
+    m.forM (fun a _ => f a) = m.keysArray.forM f :=
+  DHashMap.forM_eq_forM_keysArray
+
+theorem forIn_eq_forIn_keysArray [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keysArray init f :=
+  DHashMap.forIn_eq_forIn_keysArray
+
 end monadic
 
 variable {ρ : Type w} [ForIn Id ρ (α × β)]
diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean
index 23d9a407e8..70a2ceb953 100644
--- a/src/Std/Data/HashMap/Raw.lean
+++ b/src/Std/Data/HashMap/Raw.lean
@@ -230,8 +230,6 @@ instance {m : Type w → Type w} : ForIn m (Raw α β) (α × β) where
 
 section Unverified
 
-/-! We currently do not provide lemmas for the functions below. -/
-
 @[inline, inherit_doc DHashMap.Raw.filterMap] def filterMap {γ : Type w} (f : α → β → Option γ)
     (m : Raw α β) : Raw α γ :=
   ⟨m.inner.filterMap f⟩
@@ -249,6 +247,8 @@ section Unverified
 @[inline, inherit_doc DHashMap.Raw.keysArray] def keysArray (m : Raw α β) : Array α :=
   m.inner.keysArray
 
+/-! We currently do not provide lemmas for the functions below. -/
+
 @[inline, inherit_doc DHashMap.Raw.values] def values (m : Raw α β) : List β :=
 m.inner.values
 
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 4d5140802b..3705b99a75 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -874,6 +874,46 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   DHashMap.Raw.distinct_keys h.out
 
+@[simp]
+theorem toArray_keys (h : m.WF) :
+    m.keys.toArray = m.keysArray :=
+  DHashMap.Raw.toArray_keys h.out
+
+@[simp]
+theorem toList_keysArray (h : m.WF) :
+    m.keysArray.toList = m.keys :=
+  DHashMap.Raw.toList_keysArray h.out
+
+@[simp]
+theorem size_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keysArray.size = m.size :=
+  DHashMap.Raw.size_keysArray h.out
+
+@[simp]
+theorem isEmpty_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keysArray.isEmpty = m.isEmpty :=
+  DHashMap.Raw.isEmpty_keysArray h.out
+
+@[simp]
+theorem contains_keysArray [EquivBEq α] [LawfulHashable α]
+    {k : α} (h : m.WF) :
+    m.keysArray.contains k = m.contains k :=
+  DHashMap.Raw.contains_keysArray h.out
+
+@[simp]
+theorem mem_keysArray [LawfulBEq α] {k : α} (h : m.WF) :
+    k ∈ m.keysArray ↔ k ∈ m :=
+  DHashMap.Raw.mem_keysArray h.out
+
+theorem forall_mem_keysArray_iff_forall_mem_getKey [EquivBEq α] [LawfulHashable α]
+    {p : α → Prop} (h : m.WF) :
+    (∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h) :=
+  DHashMap.Raw.forall_mem_keysArray_iff_forall_mem_getKey h.out
+
+theorem contains_of_mem_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
+    (h' : k ∈ m.keysArray) : m.contains k :=
+  DHashMap.Raw.contains_of_mem_keysArray h.out h'
+
 @[simp, grind _=_]
 theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.map Prod.fst = m.keys :=
@@ -937,6 +977,57 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
   DHashMap.Raw.Const.distinct_keys_toList h.out
 
+@[simp]
+theorem toArray_toList (h : m.WF) :
+    m.toList.toArray = m.toArray :=
+  DHashMap.Raw.Const.toArray_toList h.out
+
+@[simp]
+theorem toList_toArray (h : m.WF) :
+    m.toArray.toList = m.toList :=
+  DHashMap.Raw.Const.toList_toArray h.out
+
+@[simp]
+theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toArray.map Prod.fst = m.keysArray :=
+  DHashMap.Raw.Const.map_fst_toArray_eq_keysArray h.out
+
+@[simp]
+theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toArray.size = m.size :=
+  DHashMap.Raw.Const.size_toArray h.out
+
+@[simp]
+theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toArray.isEmpty = m.isEmpty :=
+  DHashMap.Raw.Const.isEmpty_toArray h.out
+
+theorem mem_toArray_iff_getElem?_eq_some [LawfulBEq α]
+    {k : α} {v : β} (h : m.WF) :
+    (k, v) ∈ m.toArray ↔ m[k]? = some v :=
+  DHashMap.Raw.Const.mem_toArray_iff_get?_eq_some h.out
+
+theorem get?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} (h : m.WF) :
+    get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ m.toArray :=
+  DHashMap.Raw.Const.get?_eq_some_iff_exists_beq_and_mem_toArray h.out
+
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some
+    [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} {v : β} :
+    m.toArray.find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ m[k]? = some v :=
+  DHashMap.Raw.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some h.out
+
+theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} (h : m.WF) :
+    m.toArray.find? (·.1 == k) = none ↔ m.contains k = false :=
+  DHashMap.Raw.Const.find?_toArray_eq_none_iff_contains_eq_false h.out
+
+theorem mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {k: α} {v : β} :
+    (k, v) ∈ m.toArray ↔ m.getKey? k = some k ∧ m[k]? = some v := by
+  simp [← toArray_toList, h, mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some]
+
 section monadic
 
 variable {m : Raw α β} {δ : Type w} {m' : Type w → Type w}
@@ -988,6 +1079,42 @@ theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m'] (h : m.WF)
     ForIn.forIn m init (fun a d => f a.1 d) = ForIn.forIn m.keys init f :=
   DHashMap.Raw.forIn_eq_forIn_keys h.out
 
+theorem foldM_eq_foldlM_keysArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} (h : m.WF) :
+    m.foldM (fun d a _ => f d a) init = m.keysArray.foldlM f init :=
+  DHashMap.Raw.foldM_eq_foldlM_keysArray h.out
+
+theorem fold_eq_foldl_keysArray {f : δ → α → δ} {init : δ} (h : m.WF) :
+    m.fold (fun d a _ => f d a) init = m.keysArray.foldl f init :=
+  DHashMap.Raw.fold_eq_foldl_keysArray h.out
+
+theorem forM_eq_forM_keysArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} (h : m.WF) :
+    m.forM (fun a _ => f a) = m.keysArray.forM f :=
+  DHashMap.Raw.forM_eq_forM_keysArray h.out
+
+theorem forIn_eq_forIn_keysArray [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
+    m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keysArray init f :=
+  DHashMap.Raw.forIn_eq_forIn_keysArray h.out
+
+theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → β → m' δ} {init : δ} (h : m.WF) :
+    m.foldM f init = m.toArray.foldlM (fun a b => f a b.1 b.2) init :=
+  DHashMap.Raw.Const.foldM_eq_foldlM_toArray h.out
+
+theorem fold_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} (h : m.WF) :
+    m.fold f init = m.toArray.foldl (fun a b => f a b.1 b.2) init :=
+  DHashMap.Raw.Const.fold_eq_foldl_toArray h.out
+
+theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} (h : m.WF) :
+    m.forM f = m.toArray.forM (fun a => f a.1 a.2) :=
+  DHashMap.Raw.Const.forM_eq_forM_toArray h.out
+
+theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
+    {f : α → β → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
+    m.forIn f init = ForIn.forIn m.toArray init (fun a b => f a.1 a.2 b) :=
+  DHashMap.Raw.Const.forIn_eq_forIn_toArray h.out
+
 end monadic
 
 variable {ρ : Type w} [ForIn Id ρ (α × β)]
diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean
index a30654e27f..d5625833ac 100644
--- a/src/Std/Data/HashSet/Basic.lean
+++ b/src/Std/Data/HashSet/Basic.lean
@@ -231,6 +231,10 @@ appearance.
     HashSet α :=
   ⟨m.inner.insertManyIfNewUnit l⟩
 
+/-- Transforms the hash set into an array of elements in some order. -/
+@[inline] def toArray (m : HashSet α) : Array α :=
+  m.inner.keysArray
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -252,11 +256,6 @@ section Unverified
     if p a then return true
   return false
 
-
-/-- Transforms the hash set into an array of elements in some order. -/
-@[inline] def toArray (m : HashSet α) : Array α :=
-  m.inner.keysArray
-
 /--
 Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the
 collection contains multiple elements that are equal (with regard to `==`), then the last element
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index 03c4961a32..20c6560adf 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -482,6 +482,46 @@ theorem distinct_toList [EquivBEq α] [LawfulHashable α]:
     m.toList.Pairwise (fun a b => (a == b) = false) :=
   HashMap.distinct_keys
 
+@[simp]
+theorem toArray_toList :
+    m.toList.toArray = m.toArray :=
+  HashMap.toArray_keys
+
+@[simp]
+theorem toList_toArray :
+    m.toArray.toList = m.toList :=
+  HashMap.toList_keysArray
+
+@[simp]
+theorem size_toArray [EquivBEq α] [LawfulHashable α] :
+    m.toArray.size = m.size :=
+  HashMap.size_keysArray
+
+@[simp]
+theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] :
+    m.toArray.isEmpty = m.isEmpty :=
+  HashMap.isEmpty_keysArray
+
+@[simp]
+theorem contains_toArray [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.toArray.contains k = m.contains k :=
+  HashMap.contains_keysArray
+
+@[simp]
+theorem mem_toArray [LawfulBEq α] {k : α} :
+    k ∈ m.toArray ↔ k ∈ m :=
+  HashMap.mem_keysArray
+
+theorem forall_mem_toArray_iff_forall_mem_get [EquivBEq α] [LawfulHashable α]
+    {p : α → Prop} :
+    (∀ k ∈ m.toArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.get k h) :=
+  HashMap.forall_mem_keysArray_iff_forall_mem_getKey
+
+theorem contains_of_mem_toArray [EquivBEq α] [LawfulHashable α] {k : α}
+    (h' : k ∈ m.toArray) : m.contains k :=
+  HashMap.contains_of_mem_keysArray h'
+
 section monadic
 
 variable {δ : Type v} {m' : Type v → Type v}
@@ -513,6 +553,24 @@ theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
     ForIn.forIn m init f = ForIn.forIn m.toList init f :=
   HashMap.forIn_eq_forIn_keys
 
+theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} :
+    m.foldM (fun d a => f d a) init = m.toArray.foldlM f init :=
+  HashMap.foldM_eq_foldlM_keysArray
+
+theorem fold_eq_foldl_toArray {f : δ → α → δ} {init : δ} :
+    m.fold (fun d a => f d a) init = m.toArray.foldl f init :=
+  HashMap.fold_eq_foldl_keysArray
+
+theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
+    m.forM (fun a => f a) = m.toArray.forM f :=
+  HashMap.forM_eq_forM_keysArray
+
+theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn (fun a d => f a d) init = ForIn.forIn m.toArray init f :=
+  HashMap.forIn_eq_forIn_keysArray
+
 end monadic
 
 variable {ρ : Type v} [ForIn Id ρ α]
diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean
index 4635a7a2be..3eb9dccc93 100644
--- a/src/Std/Data/HashSet/Raw.lean
+++ b/src/Std/Data/HashSet/Raw.lean
@@ -216,14 +216,18 @@ instance {m : Type v → Type v} : ForM m (Raw α) α where
 instance {m : Type v → Type v} : ForIn m (Raw α) α where
   forIn m init f := m.forIn f init
 
-section Unverified
-
-/-! We currently do not provide lemmas for the functions below. -/
-
 /-- Removes all elements from the hash set for which the given function returns `false`. -/
 @[inline] def filter [BEq α] [Hashable α] (f : α → Bool) (m : Raw α) : Raw α :=
   ⟨m.inner.filter fun a _ => f a⟩
 
+/-- Transforms the hash set into an array of elements in some order. -/
+@[inline] def toArray (m : Raw α) : Array α :=
+  m.inner.keysArray
+
+section Unverified
+
+/-! We currently do not provide lemmas for the functions below. -/
+
 /-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/
 @[inline] def all (m : Raw α) (p : α → Bool) : Bool := Id.run do
   for a in m do
@@ -236,11 +240,6 @@ section Unverified
     if p a then return true
   return false
 
-
-/-- Transforms the hash set into an array of elements in some order. -/
-@[inline] def toArray (m : Raw α) : Array α :=
-  m.inner.keysArray
-
 /--
 Inserts multiple mappings into the hash set by iterating over the given collection and calling
 `insert`. If the same key appears multiple times, the first occurrence takes precedence.
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index 58f56b9cac..ef9de07580 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -506,6 +506,46 @@ theorem distinct_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.Pairwise (fun a b => (a == b) = false) :=
   HashMap.Raw.distinct_keys h.1
 
+@[simp]
+theorem toArray_toList (h : m.WF) :
+    m.toList.toArray = m.toArray :=
+  HashMap.Raw.toArray_keys h.out
+
+@[simp]
+theorem toList_toArray (h : m.WF) :
+    m.toArray.toList = m.toList :=
+  HashMap.Raw.toList_keysArray h.out
+
+@[simp]
+theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toArray.size = m.size :=
+  HashMap.Raw.size_keysArray h.out
+
+@[simp]
+theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toArray.isEmpty = m.isEmpty :=
+  HashMap.Raw.isEmpty_keysArray h.out
+
+@[simp]
+theorem contains_toArray [EquivBEq α] [LawfulHashable α]
+    {k : α} (h : m.WF) :
+    m.toArray.contains k = m.contains k :=
+  HashMap.Raw.contains_keysArray h.out
+
+@[simp]
+theorem mem_toArray [LawfulBEq α] {k : α} (h : m.WF) :
+    k ∈ m.toArray ↔ k ∈ m :=
+  HashMap.Raw.mem_keysArray h.out
+
+theorem forall_mem_toArray_iff_forall_mem_get [EquivBEq α] [LawfulHashable α]
+    {p : α → Prop} (h : m.WF) :
+    (∀ k ∈ m.toArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.get k h) :=
+  HashMap.Raw.forall_mem_keysArray_iff_forall_mem_getKey h.out
+
+theorem contains_of_mem_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
+    (h' : k ∈ m.toArray) : m.contains k :=
+  HashMap.Raw.contains_of_mem_keysArray h.out h'
+
 section monadic
 
 variable {m : Raw α} {δ : Type v} {m' : Type v → Type v}
@@ -539,6 +579,24 @@ theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
     ForIn.forIn m init f = ForIn.forIn m.toList init f :=
   HashMap.Raw.forIn_eq_forIn_keys h.out
 
+theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} (h : m.WF) :
+    m.foldM (fun d a => f d a) init = m.toArray.foldlM f init :=
+  HashMap.Raw.foldM_eq_foldlM_keysArray h.out
+
+theorem fold_eq_foldl_toArray {f : δ → α → δ} {init : δ} (h : m.WF) :
+    m.fold (fun d a => f d a) init = m.toArray.foldl f init :=
+  HashMap.Raw.fold_eq_foldl_keysArray h.out
+
+theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} (h : m.WF) :
+    m.forM (fun a => f a) = m.toArray.forM f :=
+  HashMap.Raw.forM_eq_forM_keysArray h.out
+
+theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
+    m.forIn (fun a d => f a d) init = ForIn.forIn m.toArray init f :=
+  HashMap.Raw.forIn_eq_forIn_keysArray h.out
+
 end monadic
 
 variable {ρ : Type v} [ForIn Id ρ α]