diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index cda996a0f9..4cb6b9c87a 100644
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -83,6 +83,17 @@ instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {
 end
 end StateT
 
+/-- Adapter to create a ForIn instance from a ForM instance -/
+@[inline] def ForM.forIn [Monad m] [ForM (StateT β (ExceptT β m)) ρ α]
+    (x : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β := do
+  let g a b := .mk do
+    match ← f a b with
+    | .yield b' => pure (.ok (⟨⟩, b'))
+    | .done b' => pure (.error b')
+  match ← forM (m := StateT β (ExceptT β m)) (α := α) x g |>.run b |>.run with
+  | .ok a => pure a.2
+  | .error a => pure a
+
 section
 variable {σ : Type u} {m : Type u → Type v}
 
diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean
index 3152c279e8..f75100d805 100644
--- a/src/Lean/Data/HashSet.lean
+++ b/src/Lean/Data/HashSet.lean
@@ -47,7 +47,7 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
   foldBuckets m.buckets d f
 
 @[inline] def forBucketsM {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (f : α → m PUnit) : m PUnit :=
-  data.val.forM fun as=> as.forM f
+  data.val.forM fun as => as.forM f
 
 @[inline] def forM {m : Type w → Type w} [Monad m] (f : α → m PUnit) (h : HashSetImp α) : m PUnit :=
   forBucketsM h.buckets f
@@ -162,6 +162,9 @@ variable {α : Type u} {_ : BEq α} {_ : Hashable α}
 instance : ForM m (HashSet α) α where
   forM := HashSet.forM
 
+instance : ForIn m (HashSet α) α where
+  forIn := ForM.forIn
+
 @[inline] def size (m : HashSet α) : Nat :=
   match m with
   | ⟨ {size := sz, ..}, _ ⟩ => sz