diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean
index a28a345f43..1285aa667c 100644
--- a/src/Std/Data/DHashMap/Basic.lean
+++ b/src/Std/Data/DHashMap/Basic.lean
@@ -188,14 +188,6 @@ end
     (m : DHashMap α (fun _ => β)) : List (α × β) :=
   Raw.Const.toList m.1
 
-section Unverified
-
-/-! We currently do not provide lemmas for the functions below. -/
-
-@[inline, inherit_doc Raw.filter] def filter (f : (a : α) → β a → Bool)
-    (m : DHashMap α β) : DHashMap α β :=
-  ⟨Raw₀.filter f ⟨m.1, m.2.size_buckets_pos⟩, .filter₀ m.2⟩
-
 @[inline, inherit_doc Raw.foldM] def foldM (f : δ → (a : α) → β a → m δ)
     (init : δ) (b : DHashMap α β) : m δ :=
   b.1.foldM f init
@@ -204,15 +196,6 @@ section Unverified
     (init : δ) (b : DHashMap α β) : δ :=
   b.1.fold f init
 
-/-- Partition a hash map into two hash map based on a predicate. -/
-@[inline] def partition (f : (a : α) → β a → Bool)
-    (m : DHashMap α β) : DHashMap α β × DHashMap α β :=
-  m.fold (init := (∅, ∅)) fun ⟨l, r⟩  a b =>
-    if f a b then
-      (l.insert a b, r)
-    else
-      (l, r.insert a b)
-
 @[inline, inherit_doc Raw.forM] def forM (f : (a : α) → β a → m PUnit)
     (b : DHashMap α β) : m PUnit :=
   b.1.forM f
@@ -227,6 +210,23 @@ instance [BEq α] [Hashable α] : ForM m (DHashMap α β) ((a : α) × β a) whe
 instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
+section Unverified
+
+/-! We currently do not provide lemmas for the functions below. -/
+
+@[inline, inherit_doc Raw.filter] def filter (f : (a : α) → β a → Bool)
+    (m : DHashMap α β) : DHashMap α β :=
+  ⟨Raw₀.filter f ⟨m.1, m.2.size_buckets_pos⟩, .filter₀ m.2⟩
+
+/-- Partition a hash map into two hash map based on a predicate. -/
+@[inline] def partition (f : (a : α) → β a → Bool)
+    (m : DHashMap α β) : DHashMap α β × DHashMap α β :=
+  m.fold (init := (∅, ∅)) fun ⟨l, r⟩  a b =>
+    if f a b then
+      (l.insert a b, r)
+    else
+      (l, r.insert a b)
+
 @[inline, inherit_doc Raw.toArray] def toArray (m : DHashMap α β) :
     Array ((a : α) × β a) :=
   m.1.toArray
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 366485a465..393c6f6d4a 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -19,7 +19,7 @@ set_option autoImplicit false
 open Std.Internal.List
 open Std.Internal
 
-universe u v
+universe u v w
 
 variable {α : Type u} {β : α → Type v}
 
@@ -90,7 +90,10 @@ private def queryNames : Array Name :=
     ``Const.get!_eq_getValue!, ``Const.getD_eq_getValueD, ``getKey?_eq_getKey?,
     ``getKey_eq_getKey, ``getKeyD_eq_getKeyD, ``getKey!_eq_getKey!,
     ``Raw.toList_eq_toListModel, ``Raw.keys_eq_keys_toListModel,
-    ``Raw.Const.toList_eq_toListModel_map]
+    ``Raw.Const.toList_eq_toListModel_map, ``Raw.foldM_eq_foldlM_toListModel,
+    ``Raw.fold_eq_foldl_toListModel, ``Raw.foldRevM_eq_foldrM_toListModel,
+    ``Raw.foldRev_eq_foldr_toListModel, ``Raw.forIn_eq_forIn_toListModel,
+    ``Raw.forM_eq_forM_toListModel]
 
 private def modifyMap : Std.DHashMap Name (fun _ => Name) :=
   .ofList
@@ -936,6 +939,102 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
 
 end Const
 
+section monadic
+
+-- The types are redefined because fold/for does not need BEq/Hashable
+variable {α : Type u} {β : α → Type v} (m : Raw₀ α β) {δ : Type w} {m' : Type w → Type w}
+
+theorem foldM_eq_foldlM_toList [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β a → m' δ} {init : δ} :
+    m.1.foldM f init = m.1.toList.foldlM (fun a b => f a b.1 b.2) init := by
+  simp_to_model
+
+theorem fold_eq_foldl_toList {f : δ → (a : α) → β a → δ} {init : δ} :
+    m.1.fold f init = m.1.toList.foldl (fun a b => f a b.1 b.2) init := by
+  simp_to_model
+
+theorem foldRevM_eq_foldrM_toList [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β a → m' δ} {init : δ} :
+    m.1.foldRevM f init = m.1.toList.foldrM (fun a b => f b a.1 a.2) init := by
+  simp_to_model
+
+theorem foldRev_eq_foldr_toList {f : δ → (a : α) → β a → δ} {init : δ} :
+    m.1.foldRev f init = m.1.toList.foldr (fun a b => f b a.1 a.2) init := by
+  simp_to_model
+
+theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit} :
+    m.1.forM f = m.1.toList.forM (fun a => f a.1 a.2) := by
+  simp_to_model
+
+theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} :
+    m.1.forIn f init = ForIn.forIn m.1.toList init (fun a b => f a.1 a.2 b) := by
+  simp_to_model
+
+namespace Const
+
+variable {β : Type v} (m : Raw₀ α (fun _ => β))
+
+theorem foldM_eq_foldlM_toList [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β → m' δ} {init : δ} :
+    m.1.foldM f init = (Raw.Const.toList m.1).foldlM (fun a b => f a b.1 b.2) init := by
+  simp_to_model using List.foldlM_eq_foldlM_toProd
+
+theorem fold_eq_foldl_toList {f : δ → (a : α) → β → δ} {init : δ} :
+    m.1.fold f init = (Raw.Const.toList m.1).foldl (fun a b => f a b.1 b.2) init := by
+  simp_to_model using List.foldl_eq_foldl_toProd
+
+theorem foldRevM_eq_foldrM_toList [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β → m' δ} {init : δ} :
+    m.1.foldRevM f init = (Raw.Const.toList m.1).foldrM (fun a b => f b a.1 a.2) init := by
+  simp_to_model using List.foldrM_eq_foldrM_toProd
+
+theorem foldRev_eq_foldr_toList {f : δ → (a : α) → β → δ} {init : δ} :
+    m.1.foldRev f init = (Raw.Const.toList m.1).foldr (fun a b => f b a.1 a.2) init := by
+  simp_to_model using List.foldr_eq_foldr_toProd
+
+theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : (a : α) → β → m' PUnit} :
+    m.1.forM f = (Raw.Const.toList m.1).forM (fun a => f a.1 a.2) := by
+  simp_to_model using List.forM_eq_forM_toProd
+
+theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β → δ → m' (ForInStep δ)} {init : δ} :
+    m.1.forIn f init = ForIn.forIn (Raw.Const.toList m.1) init (fun a b => f a.1 a.2 b) := by
+  simp_to_model using List.forIn_eq_forIn_toProd
+
+variable (m : Raw₀ α (fun _ => Unit))
+
+theorem foldM_eq_foldlM_keys [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} :
+    m.1.foldM (fun d a _ => f d a) init = m.1.keys.foldlM f init := by
+  simp_to_model using List.foldlM_eq_foldlM_keys
+
+theorem fold_eq_foldl_keys {f : δ → α → δ} {init : δ} :
+    m.1.fold (fun d a _ => f d a) init = m.1.keys.foldl f init := by
+  simp_to_model using List.foldl_eq_foldl_keys
+
+theorem foldRevM_eq_foldrM_keys [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → m' δ} {init : δ} :
+    m.1.foldRevM (fun d a _ => f d a) init = m.1.keys.foldrM (fun a b => f b a) init := by
+  simp_to_model using List.foldrM_eq_foldrM_keys
+
+theorem foldRev_eq_foldr_keys {f : δ → (a : α) → δ} {init : δ} :
+    m.1.foldRev (fun d a _ => f d a) init = m.1.keys.foldr (fun a b => f b a) init := by
+  simp_to_model using List.foldr_eq_foldr_keys
+
+theorem forM_eq_forM_keys [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
+    m.1.forM (fun a _ => f a) = m.1.keys.forM f := by
+  simp_to_model using List.forM_eq_forM_keys
+
+theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.1.forIn (fun a _ d => f a d) init = ForIn.forIn m.1.keys init f := by
+  simp_to_model using List.forIn_eq_forIn_keys
+
+end Const
+
+end monadic
+
 @[simp]
 theorem insertMany_nil :
     m.insertMany [] = m := by
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 14d24f7476..081bde6465 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -111,6 +111,48 @@ theorem foldRev_cons_key {l : Raw α β} {acc : List α} :
     l.foldRev (fun acc k _ => k :: acc) acc = List.keys (toListModel l.buckets) ++ acc := by
   rw [foldRev_cons_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
+  simp only [Raw.foldM, ← Array.foldlM_toList, toListModel]
+  induction b.buckets.toList generalizing init with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [foldlM_cons, ih, flatMap_cons, foldlM_append]
+    congr
+    induction hd generalizing init with
+    | nil => simp [AssocList.foldlM]
+    | cons hda hdb tl ih =>
+      simp only [AssocList.foldlM, AssocList.toList_cons, foldlM_cons]
+      congr
+      funext init'
+      rw [ih]
+
+theorem fold_eq_foldl_toListModel {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
+    l.fold f init = (toListModel l.buckets).foldl (fun a b => f a b.1 b.2) init := by
+  simp [Raw.fold, foldM_eq_foldlM_toListModel]
+
+theorem foldRevM_eq_foldrM_toListModel {δ : Type w} {m : Type w → Type w } [Monad m] [LawfulMonad m]
+    {f : δ → (a : α) → β a → m δ} {init : δ} {b : Raw α β} :
+    b.foldRevM f init = (toListModel b.buckets).foldrM (fun a b => f b a.1 a.2) init := by
+  simp only [Raw.foldRevM, ← Array.foldrM_toList, toListModel]
+  induction b.buckets.toList generalizing init with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [foldrM_cons, ih, flatMap_cons, foldrM_append]
+    congr
+    funext init'
+    induction hd generalizing init' with
+    | nil => simp [AssocList.foldrM]
+    | cons hda hdb tl ih =>
+      simp only [AssocList.foldrM, AssocList.toList_cons, foldrM_cons]
+      congr
+      rw [ih]
+
+theorem foldRev_eq_foldr_toListModel {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
+    l.foldRev f init = (toListModel l.buckets).foldr (fun a b => f b a.1 a.2) init := by
+  simp [Raw.foldRev, foldRevM_eq_foldrM_toListModel]
+
 theorem toList_eq_toListModel {m : Raw α β} : m.toList = toListModel m.buckets := by
   simp [Raw.toList, foldRev_cons]
 
@@ -122,6 +164,44 @@ 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 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
+  simp only [Raw.forM, Array.forM, ← Array.foldlM_toList, toListModel]
+  induction l.buckets.toList with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [foldlM_cons, flatMap_cons, forM_eq_forM, forM_append]
+    congr
+    · simp [AssocList.forM]
+      induction hd with
+      | nil => simp [AssocList.forM, AssocList.foldlM]
+      | cons hda hdb tl ih =>
+        simp only [AssocList.foldlM, AssocList.toList_cons, forM_cons]
+        congr
+        funext x
+        rw [ih]
+    · funext x
+      simp [ih]
+
+theorem forIn_eq_forIn_toListModel {δ : Type w} {l : Raw α β} {m : Type w → Type w} [Monad m] [LawfulMonad m]
+    {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} :
+    l.forIn f init = ForIn.forIn (toListModel l.buckets) init (fun a d => f a.1 a.2 d) := by
+  rw [Raw.forIn, ← Array.forIn_toList, toListModel]
+  induction l.buckets.toList generalizing init with
+  | nil => simp
+  | cons hd tl ih =>
+    induction hd generalizing init with
+    | nil => simpa [AssocList.forInStep, AssocList.forInStep.go] using ih
+    | cons k v tl' ih' =>
+      simp only [AssocList.forInStep, forIn_cons, AssocList.forInStep.go, LawfulMonad.bind_assoc,
+        flatMap_cons, AssocList.toList_cons, cons_append]
+      congr
+      apply funext
+      rintro (⟨d⟩|⟨d⟩)
+      · simp
+      · simpa using ih'
+
 end Raw
 
 namespace Raw₀
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index e5549b23f5..3d31b7a2b1 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -20,7 +20,7 @@ open Std.DHashMap.Internal
 set_option linter.missingDocs true
 set_option autoImplicit false
 
-universe u v
+universe u v w
 
 variable {α : Type u} {β : α → Type v} {_ : BEq α} {_ : Hashable α}
 
@@ -1066,6 +1066,83 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
 
 end Const
 
+section monadic
+
+variable {m : DHashMap α β} {δ : Type w} {m' : Type w → Type w}
+
+theorem foldM_eq_foldlM_toList [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β a → m' δ} {init : δ} :
+    m.foldM f init = m.toList.foldlM (fun a b => f a b.1 b.2) init :=
+  Raw₀.foldM_eq_foldlM_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem fold_eq_foldl_toList {f : δ → (a : α) → β a → δ} {init : δ} :
+    m.fold f init = m.toList.foldl (fun a b => f a b.1 b.2) init :=
+  Raw₀.fold_eq_foldl_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem forM_eq_forM [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit} :
+    DHashMap.forM f m = ForM.forM m (fun a => f a.1 a.2):= rfl
+
+theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : (a : α) × β a → m' PUnit} :
+    ForM.forM m f = ForM.forM m.toList f :=
+  Raw₀.forM_eq_forM_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem forIn_eq_forIn [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} :
+    DHashMap.forIn f init m = ForIn.forIn m init (fun a b => f a.1 a.2 b) := rfl
+
+theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
+    {f : (a : α) × β a → δ → m' (ForInStep δ)} {init : δ} :
+    ForIn.forIn m init f = ForIn.forIn m.toList init f :=
+  Raw₀.forIn_eq_forIn_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+namespace Const
+
+variable {β : Type v} {m : DHashMap α (fun _ => β)}
+
+theorem foldM_eq_foldlM_toList [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β → m' δ} {init : δ} :
+    m.foldM f init = (Const.toList m).foldlM (fun a b => f a b.1 b.2) init :=
+  Raw₀.Const.foldM_eq_foldlM_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem fold_eq_foldl_toList {f : δ → (a : α) → β → δ} {init : δ} :
+    m.fold f init = (Const.toList m).foldl (fun a b => f a b.1 b.2) init :=
+  Raw₀.Const.fold_eq_foldl_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : (a : α) → β → m' PUnit} :
+    m.forM f = (Const.toList m).forM (fun a => f a.1 a.2) :=
+  Raw₀.Const.forM_eq_forM_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn f init = ForIn.forIn (Const.toList m) init (fun a b => f a.1 a.2 b) :=
+  Raw₀.Const.forIn_eq_forIn_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+variable {m : DHashMap α (fun _ => Unit)}
+
+theorem foldM_eq_foldlM_keys [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} :
+    m.foldM (fun d a _ => f d a) init = m.keys.foldlM f init :=
+  Raw₀.Const.foldM_eq_foldlM_keys ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem fold_eq_foldl_keys {f : δ → α → δ} {init : δ} :
+    m.fold (fun d a _ => f d a) init = m.keys.foldl f init :=
+  Raw₀.Const.fold_eq_foldl_keys ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem forM_eq_forM_keys [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
+    m.forM (fun a _ => f a) = m.keys.forM f :=
+  Raw₀.Const.forM_eq_forM_keys ⟨m.1, m.2.size_buckets_pos⟩
+
+theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keys init f :=
+  Raw₀.Const.forIn_eq_forIn_keys ⟨m.1, m.2.size_buckets_pos⟩
+
+end Const
+
+end monadic
+
 @[simp]
 theorem insertMany_nil :
     m.insertMany [] = m :=
diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean
index d4309b6689..99300bbd77 100644
--- a/src/Std/Data/DHashMap/Raw.lean
+++ b/src/Std/Data/DHashMap/Raw.lean
@@ -335,32 +335,6 @@ This function ensures that the value is used linearly.
   else
     ∅
 
-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.
--/
-@[inline] def filterMap {γ : α → Type w} (f : (a : α) → β a → Option (γ a)) (m : Raw α β) :
-    Raw α γ :=
-  if h : 0 < m.buckets.size then
-    Raw₀.filterMap f ⟨m, h⟩
-  else ∅ -- will never happen for well-formed inputs
-
-/-- Updates the values of the hash map by applying the given function to all mappings. -/
-@[inline] def map {γ : α → Type w} (f : (a : α) → β a → γ a) (m : Raw α β) : Raw α γ :=
-  if h : 0 < m.buckets.size then
-    Raw₀.map f ⟨m, h⟩
-  else ∅ -- will never happen for well-formed inputs
-
-/-- Removes all mappings of the hash map for which the given function returns `false`. -/
-@[inline] def filter (f : (a : α) → β a → Bool) (m : Raw α β) : Raw α β :=
-  if h : 0 < m.buckets.size then
-    Raw₀.filter f ⟨m, h⟩
-  else ∅ -- will never happen for well-formed inputs
-
 /--
 Monadically computes a value by folding the given function over the mappings in the hash
 map in some order.
@@ -399,6 +373,32 @@ instance : ForM m (Raw α β) ((a : α) × β a) where
 instance : ForIn m (Raw α β) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
+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.
+-/
+@[inline] def filterMap {γ : α → Type w} (f : (a : α) → β a → Option (γ a)) (m : Raw α β) :
+    Raw α γ :=
+  if h : 0 < m.buckets.size then
+    Raw₀.filterMap f ⟨m, h⟩
+  else ∅ -- will never happen for well-formed inputs
+
+/-- Updates the values of the hash map by applying the given function to all mappings. -/
+@[inline] def map {γ : α → Type w} (f : (a : α) → β a → γ a) (m : Raw α β) : Raw α γ :=
+  if h : 0 < m.buckets.size then
+    Raw₀.map f ⟨m, h⟩
+  else ∅ -- will never happen for well-formed inputs
+
+/-- Removes all mappings of the hash map for which the given function returns `false`. -/
+@[inline] def filter (f : (a : α) → β a → Bool) (m : Raw α β) : Raw α β :=
+  if h : 0 < m.buckets.size then
+    Raw₀.filter f ⟨m, h⟩
+  else ∅ -- will never happen for well-formed inputs
+
 /-- Transforms the hash map into an array of mappings in some order. -/
 @[inline] def toArray (m : Raw α β) : Array ((a : α) × β a) :=
   m.fold (fun acc k v => acc.push ⟨k, v⟩) #[]
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 621e922aa7..eabf420c15 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -20,7 +20,7 @@ open Std.DHashMap.Internal
 set_option linter.missingDocs true
 set_option autoImplicit false
 
-universe u v
+universe u v w
 
 variable {α : Type u} {β : α → Type v}
 
@@ -1158,6 +1158,86 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
 
 end Const
 
+section monadic
+
+variable {m : Raw α β} {δ : Type w} {m' : Type w → Type w}
+
+theorem foldM_eq_foldlM_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : δ → (a : α) → β a → m' δ} {init : δ} :
+    m.foldM f init = m.toList.foldlM (fun a b => f a b.1 b.2) init :=
+  Raw₀.foldM_eq_foldlM_toList ⟨m, h.size_buckets_pos⟩
+
+theorem fold_eq_foldl_toList (h : m.WF) {f : δ → (a : α) → β a → δ} {init : δ} :
+    m.fold f init = m.toList.foldl (fun a b => f a b.1 b.2) init :=
+  Raw₀.fold_eq_foldl_toList ⟨m, h.size_buckets_pos⟩
+
+omit [BEq α] [Hashable α] in
+@[simp]
+theorem forM_eq_forM [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β a → m' PUnit} :
+    Raw.forM f m = ForM.forM m (fun a => f a.1 a.2) := rfl
+
+theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] (h : m.WF) {f : (a : α) × β a → m' PUnit} :
+    ForM.forM m f = m.toList.forM f :=
+  Raw₀.forM_eq_forM_toList ⟨m, h.size_buckets_pos⟩
+
+omit [BEq α] [Hashable α] in
+@[simp]
+theorem forIn_eq_forIn [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} :
+    Raw.forIn f init m = ForIn.forIn m init (fun a b => f a.1 a.2 b) := rfl
+
+theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
+    {f : (a : α) × β a → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
+    ForIn.forIn m init f = ForIn.forIn m.toList init f :=
+  Raw₀.forIn_eq_forIn_toList ⟨m, h.size_buckets_pos⟩
+
+namespace Const
+
+variable {β : Type v} {m : Raw α (fun _ => β)}
+
+theorem foldM_eq_foldlM_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : δ → (a : α) → β → m' δ} {init : δ} :
+    m.foldM f init = (Const.toList m).foldlM (fun a b => f a b.1 b.2) init :=
+  Raw₀.Const.foldM_eq_foldlM_toList ⟨m, h.size_buckets_pos⟩
+
+theorem fold_eq_foldl_toList (h : m.WF) {f : δ → (a : α) → β → δ} {init : δ} :
+    m.fold f init = (Raw.Const.toList m).foldl (fun a b => f a b.1 b.2) init :=
+  Raw₀.Const.fold_eq_foldl_toList ⟨m, h.size_buckets_pos⟩
+
+theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] (h : m.WF) {f : (a : α) → β → m' PUnit} :
+    m.forM f = (Raw.Const.toList m).forM (fun a => f a.1 a.2) :=
+  Raw₀.Const.forM_eq_forM_toList ⟨m, h.size_buckets_pos⟩
+
+theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : (a : α) → β → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn f init = ForIn.forIn (Raw.Const.toList m) init (fun a b => f a.1 a.2 b) :=
+  Raw₀.Const.forIn_eq_forIn_toList ⟨m, h.size_buckets_pos⟩
+
+variable {m : Raw α (fun _ => Unit)}
+
+theorem foldM_eq_foldlM_keys [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : δ → α → m' δ} {init : δ} :
+    m.foldM (fun d a _ => f d a) init = m.keys.foldlM f init :=
+  Raw₀.Const.foldM_eq_foldlM_keys ⟨m, h.size_buckets_pos⟩
+
+theorem fold_eq_foldl_keys (h : m.WF) {f : δ → α → δ} {init : δ} :
+    m.fold (fun d a _ => f d a) init = m.keys.foldl f init :=
+  Raw₀.Const.fold_eq_foldl_keys ⟨m, h.size_buckets_pos⟩
+
+theorem forM_eq_forM_keys [Monad m'] [LawfulMonad m'] (h : m.WF) {f : α → m' PUnit} :
+    m.forM (fun a _ => f a) = m.keys.forM f :=
+  Raw₀.Const.forM_eq_forM_keys ⟨m, h.size_buckets_pos⟩
+
+theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keys init f :=
+  Raw₀.Const.forIn_eq_forIn_keys ⟨m, h.size_buckets_pos⟩
+
+end Const
+
+end monadic
+
 @[simp]
 theorem insertMany_nil [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.insertMany [] = m := by
diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index 52611832fe..e1be4709ae 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -203,19 +203,6 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a 
     List (α × β) :=
   DHashMap.Const.toList m.inner
 
-section Unverified
-
-/-! We currently do not provide lemmas for the functions below. -/
-
-@[inline, inherit_doc DHashMap.filter] def filter (f : α → β → Bool)
-    (m : HashMap α β) : HashMap α β :=
-  ⟨m.inner.filter f⟩
-
-@[inline, inherit_doc DHashMap.partition] def partition (f : α → β → Bool)
-    (m : HashMap α β) : HashMap α β × HashMap α β :=
-  let ⟨l, r⟩ := m.inner.partition f
-  ⟨⟨l⟩, ⟨r⟩⟩
-
 @[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w → Type w}
     [Monad m] {γ : Type w} (f : γ → α → β → m γ) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.foldM f init
@@ -238,6 +225,19 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForM m (HashMap α β)
 instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β) (α × β) where
   forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init
 
+section Unverified
+
+/-! We currently do not provide lemmas for the functions below. -/
+
+@[inline, inherit_doc DHashMap.filter] def filter (f : α → β → Bool)
+    (m : HashMap α β) : HashMap α β :=
+  ⟨m.inner.filter f⟩
+
+@[inline, inherit_doc DHashMap.partition] def partition (f : α → β → Bool)
+    (m : HashMap α β) : HashMap α β × HashMap α β :=
+  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
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 599bd30792..172ea7b730 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -18,7 +18,7 @@ is to provide an instance of `LawfulBEq α`.
 set_option linter.missingDocs true
 set_option autoImplicit false
 
-universe u v
+universe u v w
 
 variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
 
@@ -751,6 +751,59 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
     m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
   DHashMap.Const.distinct_keys_toList
 
+section monadic
+
+variable {m : HashMap α β} {δ : Type w} {m' : Type w → Type w}
+
+theorem foldM_eq_foldlM_toList [Monad m'] [LawfulMonad m']
+    {f : δ → (a : α) → β → m' δ} {init : δ} :
+    m.foldM f init = m.toList.foldlM (fun a b => f a b.1 b.2) init :=
+  DHashMap.Const.foldM_eq_foldlM_toList
+
+theorem fold_eq_foldl_toList {f : δ → (a : α) → β → δ} {init : δ} :
+    m.fold f init = m.toList.foldl (fun a b => f a b.1 b.2) init :=
+  DHashMap.Const.fold_eq_foldl_toList
+
+@[simp]
+theorem forM_eq_forM [Monad m'] [LawfulMonad m'] {f : (a : α) → β → m' PUnit} :
+    m.forM f = ForM.forM m (fun a => f a.1 a.2) := rfl
+
+theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : α × β → m' PUnit} :
+    ForM.forM m f = ForM.forM m.toList f :=
+  DHashMap.Const.forM_eq_forM_toList
+
+@[simp]
+theorem forIn_eq_forIn [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn f init = ForIn.forIn m init (fun a d => f a.1 a.2 d) := rfl
+
+theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
+    {f : α × β → δ → m' (ForInStep δ)} {init : δ} :
+    ForIn.forIn m init f = ForIn.forIn m.toList init f :=
+  DHashMap.Const.forIn_eq_forIn_toList
+
+variable {m : DHashMap α (fun _ => Unit)}
+
+theorem foldM_eq_foldlM_keys [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} :
+    m.foldM (fun d a _ => f d a) init = m.keys.foldlM f init :=
+  DHashMap.Const.foldM_eq_foldlM_keys
+
+theorem fold_eq_foldl_keys {f : δ → α → δ} {init : δ} :
+    m.fold (fun d a _ => f d a) init = m.keys.foldl f init :=
+  DHashMap.Const.fold_eq_foldl_keys
+
+theorem forM_eq_forM_keys [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
+    m.forM (fun a _ => f a) = m.keys.forM f :=
+  DHashMap.Const.forM_eq_forM_keys
+
+theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keys init f :=
+  DHashMap.Const.forIn_eq_forIn_keys
+
+end monadic
+
 @[simp]
 theorem insertMany_nil :
     insertMany m [] = m :=
diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean
index 2b1cb06788..c92a167e85 100644
--- a/src/Std/Data/HashMap/Raw.lean
+++ b/src/Std/Data/HashMap/Raw.lean
@@ -192,21 +192,6 @@ instance [BEq α] [Hashable α] : GetElem? (Raw α β) α β (fun m a => a ∈ m
 @[inline, inherit_doc DHashMap.Raw.Const.toList] def toList (m : Raw α β) : List (α × β) :=
   DHashMap.Raw.Const.toList m.inner
 
-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⟩
-
-@[inline, inherit_doc DHashMap.Raw.map] def map {γ : Type w} (f : α → β → γ) (m : Raw α β) :
-    Raw α γ :=
-  ⟨m.inner.map f⟩
-
-@[inline, inherit_doc DHashMap.Raw.filter] def filter (f : α → β → Bool) (m : Raw α β) : Raw α β :=
-  ⟨m.inner.filter f⟩
-
 @[inline, inherit_doc DHashMap.Raw.foldM] def foldM {m : Type w → Type w} [Monad m] {γ : Type w}
     (f : γ → α → β → m γ) (init : γ) (b : Raw α β) : m γ :=
   b.inner.foldM f init
@@ -229,6 +214,21 @@ instance {m : Type w → Type w} : ForM m (Raw α β) (α × β) where
 instance {m : Type w → Type w} : ForIn m (Raw α β) (α × β) where
   forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init
 
+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⟩
+
+@[inline, inherit_doc DHashMap.Raw.map] def map {γ : Type w} (f : α → β → γ) (m : Raw α β) :
+    Raw α γ :=
+  ⟨m.inner.map f⟩
+
+@[inline, inherit_doc DHashMap.Raw.filter] def filter (f : α → β → Bool) (m : Raw α β) : Raw α β :=
+  ⟨m.inner.filter f⟩
+
 @[inline, inherit_doc DHashMap.Raw.Const.toArray] def toArray (m : Raw α β) : Array (α × β) :=
   DHashMap.Raw.Const.toArray m.inner
 
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index d0d1ad19e0..4084f331da 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -18,7 +18,7 @@ is to provide an instance of `LawfulBEq α`.
 set_option linter.missingDocs true
 set_option autoImplicit false
 
-universe u v
+universe u v w
 
 variable {α : Type u} {β : Type v}
 
@@ -758,6 +758,61 @@ 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
 
+section monadic
+
+variable {m : Raw α β} {δ : Type w} {m' : Type w → Type w}
+
+theorem foldM_eq_foldlM_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : δ → (a : α) → β → m' δ} {init : δ} :
+    m.foldM f init = m.toList.foldlM (fun a b => f a b.1 b.2) init :=
+  DHashMap.Raw.Const.foldM_eq_foldlM_toList h.out
+
+theorem fold_eq_foldl_toList (h : m.WF) {f : δ → (a : α) → β → δ} {init : δ} :
+    m.fold f init = m.toList.foldl (fun a b => f a b.1 b.2) init :=
+  DHashMap.Raw.Const.fold_eq_foldl_toList h.out
+
+omit [BEq α] [Hashable α] in
+@[simp]
+theorem forM_eq_forM [Monad m'] [LawfulMonad m'] {f : (a : α) → β → m' PUnit} :
+    m.forM f = ForM.forM m (fun a => f a.1 a.2) := rfl
+
+theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] (h : m.WF) {f : α × β → m' PUnit} :
+    ForM.forM m f = ForM.forM m.toList f :=
+  DHashMap.Raw.Const.forM_eq_forM_toList h.out
+
+omit [BEq α] [Hashable α] in
+@[simp]
+theorem forIn_eq_forIn [Monad m'] [LawfulMonad m']
+    {f : (a : α) → β → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn f init = ForIn.forIn m init (fun a d => f a.1 a.2 d) := rfl
+
+theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : α × β → δ → m' (ForInStep δ)} {init : δ} :
+    ForIn.forIn m init f = ForIn.forIn m.toList init f :=
+  DHashMap.Raw.Const.forIn_eq_forIn_toList h.out
+
+variable {m : Raw α Unit}
+
+theorem foldM_eq_foldlM_keys [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : δ → α → m' δ} {init : δ} :
+    m.foldM (fun d a _ => f d a) init = m.keys.foldlM f init :=
+  DHashMap.Raw.Const.foldM_eq_foldlM_keys h.out
+
+theorem fold_eq_foldl_keys (h : m.WF) {f : δ → α → δ} {init : δ} :
+    m.fold (fun d a _ => f d a) init = m.keys.foldl f init :=
+  DHashMap.Raw.Const.fold_eq_foldl_keys h.out
+
+theorem forM_eq_forM_keys [Monad m'] [LawfulMonad m'] (h : m.WF) {f : α → m' PUnit} :
+    m.forM (fun a _ => f a) = m.keys.forM f :=
+  DHashMap.Raw.Const.forM_eq_forM_keys h.out
+
+theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keys init f :=
+  DHashMap.Raw.Const.forIn_eq_forIn_keys h.out
+
+end monadic
+
 @[simp]
 theorem insertMany_nil (h : m.WF) :
     insertMany m [] = m :=
diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean
index 2a75fd63fc..ac8820c48d 100644
--- a/src/Std/Data/HashSet/Basic.lean
+++ b/src/Std/Data/HashSet/Basic.lean
@@ -170,19 +170,6 @@ in the collection will be present in the returned hash set.
 @[inline] def ofList [BEq α] [Hashable α] (l : List α) : HashSet α :=
   ⟨HashMap.unitOfList l⟩
 
-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 (f : α → Bool) (m : HashSet α) : HashSet α :=
-  ⟨m.inner.filter fun a _ => f a⟩
-
-/-- Partition a hashset into two hashsets based on a predicate. -/
-@[inline] def partition (f : α → Bool) (m : HashSet α) : HashSet α × HashSet α :=
-  let ⟨l, r⟩ := m.inner.partition fun a _ => f a
-  ⟨⟨l⟩, ⟨r⟩⟩
-
 /--
 Monadically computes a value by folding the given function over the elements in the hash set in some
 order.
@@ -212,6 +199,19 @@ instance [BEq α] [Hashable α] {m : Type v → Type v} : ForM m (HashSet α) α
 instance [BEq α] [Hashable α] {m : Type v → Type v} : ForIn m (HashSet α) α 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 (f : α → Bool) (m : HashSet α) : HashSet α :=
+  ⟨m.inner.filter fun a _ => f a⟩
+
+/-- Partition a hashset into two hashsets based on a predicate. -/
+@[inline] def partition (f : α → Bool) (m : HashSet α) : HashSet α × HashSet α :=
+  let ⟨l, r⟩ := m.inner.partition fun a _ => f a
+  ⟨⟨l⟩, ⟨r⟩⟩
+
 /-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/
 @[inline] def all (m : HashSet α) (p : α → Bool) : Bool := Id.run do
   for a in m do
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index b3c9d8b885..f99363e566 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -374,6 +374,39 @@ theorem distinct_toList [EquivBEq α] [LawfulHashable α]:
     m.toList.Pairwise (fun a b => (a == b) = false) :=
   HashMap.distinct_keys
 
+section monadic
+
+variable {δ : Type v} {m' : Type v → Type v}
+
+theorem foldM_eq_foldlM_toList [Monad m'] [LawfulMonad m']
+    {f : δ → α → m' δ} {init : δ} :
+    m.foldM f init = m.toList.foldlM f init :=
+  HashMap.foldM_eq_foldlM_keys
+
+theorem fold_eq_foldl_toList {f : δ → α → δ} {init : δ} :
+    m.fold f init = m.toList.foldl f init :=
+  HashMap.fold_eq_foldl_keys
+
+@[simp]
+theorem forM_eq_forM [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
+    m.forM f = ForM.forM m f := rfl
+
+theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
+    ForM.forM m f = ForM.forM m.toList f :=
+  HashMap.forM_eq_forM_keys
+
+@[simp]
+theorem forIn_eq_forIn [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn f init = ForIn.forIn m init f := rfl
+
+theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    ForIn.forIn m init f = ForIn.forIn m.toList init f :=
+  HashMap.forIn_eq_forIn_keys
+
+end monadic
+
 @[simp]
 theorem insertMany_nil :
     insertMany m [] = m :=
diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean
index 687317d808..a183b91738 100644
--- a/src/Std/Data/HashSet/Raw.lean
+++ b/src/Std/Data/HashSet/Raw.lean
@@ -173,14 +173,6 @@ in the collection will be present in the returned hash set.
 @[inline] def ofList [BEq α] [Hashable α] (l : List α) : Raw α :=
   ⟨HashMap.Raw.unitOfList l⟩
 
-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⟩
-
 /--
 Monadically computes a value by folding the given function over the elements in the hash set in some
 order.
@@ -208,6 +200,14 @@ 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⟩
+
 /-- 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
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index a32e4d3ef4..d2f3401b75 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -390,6 +390,41 @@ theorem distinct_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.Pairwise (fun a b => (a == b) = false) :=
   HashMap.Raw.distinct_keys h.1
 
+section monadic
+
+variable {m : Raw α} {δ : Type v} {m' : Type v → Type v}
+
+theorem foldM_eq_foldlM_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : δ → α → m' δ} {init : δ} :
+    m.foldM f init = m.toList.foldlM f init :=
+  HashMap.Raw.foldM_eq_foldlM_keys h.out
+
+theorem fold_eq_foldl_toList (h : m.WF) {f : δ → α → δ} {init : δ} :
+    m.fold f init = m.toList.foldl f init :=
+  HashMap.Raw.fold_eq_foldl_keys h.out
+
+omit [BEq α] [Hashable α] in
+@[simp]
+theorem forM_eq_forM [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
+    m.forM f = ForM.forM m f := rfl
+
+theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] (h : m.WF) {f : α → m' PUnit} :
+    ForM.forM m f = ForM.forM m.toList f :=
+  HashMap.Raw.forM_eq_forM_keys h.out
+
+omit [BEq α] [Hashable α] in
+@[simp]
+theorem forIn_eq_forIn [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    m.forIn f init = ForIn.forIn m init f := rfl
+
+theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
+    {f : α → δ → m' (ForInStep δ)} {init : δ} :
+    ForIn.forIn m init f = ForIn.forIn m.toList init f :=
+  HashMap.Raw.forIn_eq_forIn_keys h.out
+
+end monadic
+
 @[simp]
 theorem insertMany_nil (h : m.WF) :
     insertMany m [] = m :=
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index 75b0667374..18231341f4 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -8,6 +8,7 @@ import Init.Data.BEq
 import Init.Data.Nat.Simproc
 import Init.Data.List.Perm
 import Init.Data.List.Find
+import Init.Data.List.Monadic
 import Std.Classes.Ord
 import Std.Data.Internal.List.Defs
 
@@ -2088,6 +2089,107 @@ theorem pairwise_fst_eq_false_map_toProd [BEq α] {β : Type v}
   simp [List.pairwise_map]
   assumption
 
+theorem foldlM_eq_foldlM_toProd {β : Type v} {δ : Type w} {m' : Type w → Type w} [Monad m']
+    [LawfulMonad m'] {l : List ((_ : α) × β)} {f : δ → (a : α) → β → m' δ} {init : δ} :
+    l.foldlM (fun a b => f a b.fst b.snd) init =
+      (l.map fun x => (x.1, x.2)).foldlM (fun a b => f a b.fst b.snd) init := by
+  induction l generalizing init with
+  | nil => simp
+  | cons hd tl ih => simp [ih]
+
+theorem foldl_eq_foldl_toProd {β : Type v} {δ : Type w}
+    {l : List ((_ : α) × β)} {f : δ → (a : α) → β → δ} {init : δ} :
+    l.foldl (fun a b => f a b.fst b.snd) init =
+      (l.map fun x => (x.1, x.2)).foldl (fun a b => f a b.fst b.snd) init := by
+  induction l generalizing init with
+  | nil => simp
+  | cons hd tl ih => simp [ih]
+
+theorem foldrM_eq_foldrM_toProd {β : Type v} {δ : Type w} {m' : Type w → Type w} [Monad m']
+    [LawfulMonad m'] {l : List ((_ : α) × β)} {f : δ → (a : α) → β → m' δ} {init : δ} :
+    l.foldrM (fun a b => f b a.1 a.2) init =
+      (l.map fun x => (x.1, x.2)).foldrM (fun a b => f b a.1 a.2) init := by
+  induction l generalizing init with
+  | nil => simp
+  | cons hd tl ih => simp [ih]
+
+theorem foldr_eq_foldr_toProd {β : Type v} {δ : Type w}
+    {l : List ((_ : α) × β)} {f : δ → (a : α) → β → δ} {init : δ} :
+    l.foldr (fun a b => f b a.1 a.2) init =
+      (l.map fun x => (x.1, x.2)).foldr (fun a b => f b a.1 a.2) init := by
+  induction l generalizing init with
+  | nil => simp
+  | cons hd tl ih => simp [ih]
+
+theorem forM_eq_forM_toProd {β : Type v} {m' : Type w → Type w} [Monad m']
+    [LawfulMonad m'] {l : List ((_ : α) × β)} {f : (a : α) → β → m' PUnit} :
+    forM l (fun a => f a.1 a.2) = forM (l.map (fun x => (x.1, x.2))) fun a => f a.1 a.2 := by
+  cases l with
+  | nil => simp
+  | cons hd tl => simp
+
+theorem forIn_eq_forIn_toProd {β : Type v} {δ : Type w} {m' : Type w → Type w} [Monad m']
+    [LawfulMonad m'] {l : List ((_ : α) × β)} {f : (a : α) → β → δ → m' (ForInStep δ)} {init : δ} :
+    ForIn.forIn l init (fun a d => f a.1 a.2 d) =
+      ForIn.forIn (l.map (fun x => (x.1, x.2))) init fun a d => f a.1 a.2 d := by
+  cases l  with
+  | nil => simp
+  | cons hd tl => simp
+
+theorem foldlM_eq_foldlM_keys {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m']
+    {l : List ((_ : α) × Unit)} {f : δ → α → m' δ} {init : δ} :
+    l.foldlM (fun a b => f a b.1) init = (keys l).foldlM f init := by
+  induction l generalizing init with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.foldlM_cons, keys]
+    congr
+    simp [ih]
+
+theorem foldl_eq_foldl_keys {δ : Type w}
+    {l : List ((_ : α) × Unit)} {f : δ → α → δ} {init : δ} :
+    l.foldl (fun a b => f a b.1) init = (keys l).foldl f init := by
+  induction l generalizing init with
+  | nil => simp
+  | cons hd tl ih => simp [List.foldlM_cons, keys, ih]
+
+theorem foldrM_eq_foldrM_keys {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m']
+    {l : List ((_ : α) × Unit)} {f : δ → α → m' δ} {init : δ} :
+    l.foldrM (fun a b => f b a.1) init = (keys l).foldrM (fun a b => f b a) init := by
+  induction l generalizing init with
+  | nil => simp
+  | cons hd tl ih =>
+    simp [keys, ih]
+
+theorem foldr_eq_foldr_keys {δ : Type w}
+    {l : List ((_ : α) × Unit)} {f : δ → α → δ} {init : δ} :
+    l.foldr (fun a b => f b a.1) init = (keys l).foldr (fun a b => f b a) init := by
+  induction l generalizing init with
+  | nil => simp
+  | cons hd tl ih => simp [keys, ih]
+
+theorem forM_eq_forM_keys {m' : Type w → Type w} [Monad m'] [LawfulMonad m']
+    {l : List ((_ : α) × Unit)} {f : α → m' PUnit} :
+    l.forM (fun a => f a.1) = (keys l).forM f := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.forM_eq_forM, List.forM_cons, keys]
+    congr
+    funext x
+    apply ih
+
+theorem forIn_eq_forIn_keys {δ : Type w} {m' : Type w → Type w} [Monad m'] [LawfulMonad m']
+    {f : α → δ → m' (ForInStep δ)} {init : δ} {l : List ((_ : α) × Unit)} :
+    ForIn.forIn l init (fun a d => f a.fst d) = ForIn.forIn (keys l) init f := by
+  induction l generalizing init with
+  | nil => simp
+  | cons hd tl ih =>
+    simp [keys]
+    congr
+    funext x
+    cases x <;> simp[ih]
+
 /-- Internal implementation detail of the hash map -/
 def insertList [BEq α] (l toInsert : List ((a : α) × β a)) : List ((a : α) × β a) :=
   match toInsert with