以下、公式資料ベースの要点です。なお、公式 Zulip は Web 検索経由では ForIn 自体を解説する有用スレッドを確認できず、実質的な根拠は Functional Programming in Lean と Lean 公式リファレンス です。
結論
ForIn は、Lean の
for x in xs do
...
を動かすための型クラスです。List、Array、Range などの「走査できるもの」に対し、do ブロック内でモナド的に反復する方法を与えます。
公式リファレンス上の本体はこれです。 
class ForIn (m : Type u₁ → Type u₂) (ρ : Type u)
(α : outParam (Type v)) where
forIn :
{β : Type u₁} →
ρ →
β →
(α → β → m (ForInStep β)) →
m β
読み方は次の通りです。
ForIn m ρ α
は、
「モナド m の中で、コレクション型 ρ を、要素型 α として走査できる」
という意味です。
forIn の引数は：
ρ -- 走査対象
β -- ループ内部状態の型
β -- 初期状態
α → β → m (ForInStep β) -- 各要素に対する本体
m β -- 最終状態
ForInStep β は「続けるか、止めるか」を表します。公式リファレンスでは、done は break / return に対応し、yield は通常継続または continue に対応すると説明されています。 
inductive ForInStep (β : Type u) where
| done : β → ForInStep β
| yield : β → ForInStep β
典型例：for は ForIn に脱糖される
Functional Programming in Lean は、for ... in ... do が ForIn に脱糖され、ForIn は ForM より複雑で「状態」と「早期終了」を扱う、と説明しています。 
def sumList (xs : List Nat) : Nat := Id.run do
let mut acc := 0
for x in xs do
acc := acc + x
return acc
#eval sumList [1, 2, 3, 4]
-- 10
これは概念的には次のような状態渡しです。
def sumListExplicit (xs : List Nat) : Id Nat :=
ForIn.forIn xs 0 fun x acc =>
pure <| ForInStep.yield (acc + x)
#eval sumListExplicit [1, 2, 3, 4]
-- 10
break：ForInStep.done
def sumUntilGreaterThan10 (xs : List Nat) : Nat := Id.run do
let mut acc := 0
for x in xs do
if x > 10 then
break
acc := acc + x
return acc
#eval sumUntilGreaterThan10 [1, 2, 20, 3]
-- 3
対応するイメージは：
def sumUntilGreaterThan10Explicit (xs : List Nat) : Id Nat :=
ForIn.forIn xs 0 fun x acc =>
if x > 10 then
pure <| ForInStep.done acc
else
pure <| ForInStep.yield (acc + x)
return：ループだけでなく do ブロック全体から戻る
Functional Programming in Lean では、for ループ内の早期 return を使った List.find? の例が出ています。 
def find? (p : α → Bool) (xs : List α) : Option α := do
for x in xs do
if p x then
return x
failure
例：
#eval find? (fun n => n > 5) [1, 3, 8, 2]
-- some 8
#eval find? (fun n => n > 5) [1, 3, 4]
-- none
continue：今回の反復だけスキップ
同じく公式本では、continue によってループ本体の残りを飛ばせることが説明されています。 
def sumOdds (xs : List Nat) : Nat := Id.run do
let mut acc := 0
for x in xs do
if x % 2 == 0 then
continue
acc := acc + x
return acc
#eval sumOdds [1, 2, 3, 4, 5]
-- 9
ForM から ForIn を作る
Functional Programming in Lean では、ForM インスタンスから ForM.forIn によって ForIn インスタンスを作れると説明されています。ただし、そのアダプタは内部で StateT と ExceptT を使うため、モナドを一般化している ForM に対して使うものです。 
structure AllLessThan where
num : Nat
def AllLessThan.forM [Monad m]
(coll : AllLessThan)
(action : Nat → m PUnit) : m PUnit := do
let rec countdown : Nat → m PUnit
| 0 => pure ⟨⟩
| n + 1 => do
action n
countdown n
countdown coll.num
instance [Monad m] : ForM m AllLessThan Nat where
forM := AllLessThan.forM
instance [Monad m] : ForIn m AllLessThan Nat where
forIn := ForM.forIn
使用例：
def printLessThanFive : IO Unit := do
for i in ({ num := 5 } : AllLessThan) do
IO.println i
#eval printLessThanFive
-- 4
-- 3
-- 2
-- 1
-- 0
ForIn'：要素がコレクションに属する証拠つきループ
ForIn' は、各反復で a ∈ x の証明も本体に渡す強化版です。公式リファレンスでは、for h : x in xs do ... 形式で使うと説明されています。 
class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u)
(α : outParam (Type v))
(d : outParam (Membership α ρ)) where
forIn' :
{β : Type u₁} →
(x : ρ) →
β →
((a : α) → a ∈ x → β → m (ForInStep β)) →
m β
公式本の例では、範囲 [0:xs.size] を証拠つきで回すことで、xs[i] が安全なアクセスだと Lean に分からせています。 
def printArray [ToString α] (xs : Array α) : IO Unit := do
for h : i in [0:xs.size] do
IO.println s!"{i}:\t{xs[i]}"
ここで h は概念的に：
h : i ∈ [0:xs.size]
であり、Lean はそこから i < xs.size を導けます。
複数コレクションの並列ループ
Functional Programming in Lean は、複数の in 節をカンマで並べると並列に反復し、どれかが尽きた時点で停止すると説明しています。 
def parallelLoop : IO Unit := do
for x in ["currant", "gooseberry", "rowan"], y in [4:8] do
IO.println (x, y)
#eval parallelLoop
-- ("currant", 4)
-- ("gooseberry", 5)
-- ("rowan", 6)
注意：Lean 4.27 以降の変更
Lean 4.27.0 のリリースノートでは、ForIn、ForIn'、ForM のインターフェースが変更され、型クラス自体は Monad m パラメータを取らなくなり、下流の instance 側で [Monad m] を仮定する必要がある、と説明されています。 
したがって、古い記事やコードでは：
instance : ForIn m MyCollection α where
...
の周辺で Monad m の置き方が現在の Lean と合わない場合があります。現在は概ね：
instance [Monad m] : ForIn m MyCollection α where
...
の形に寄せるのが安全です。
まとめ
ForIn は「for x in xs do を使えるようにする型クラス」です。ForM が単純な全要素走査を表すのに対し、ForIn は let mut、break、continue、return を支えるために、内部状態 β と ForInStep β を扱います。証明つきの反復が必要なら ForIn' を使います。
以下、公式資料ベースの要点です。なお、公式 Zulip は Web 検索経由では ForIn 自体を解説する有用スレッドを確認できず、実質的な根拠は Functional Programming in Lean と Lean 公式リファレンス です。
結論
ForIn は、Lean の
for x in xs do
...
を動かすための型クラスです。List、Array、Range などの「走査できるもの」に対し、do ブロック内でモナド的に反復する方法を与えます。
公式リファレンス上の本体はこれです。 
class ForIn (m : Type u₁ → Type u₂) (ρ : Type u)
(α : outParam (Type v)) where
forIn :
{β : Type u₁} →
ρ →
β →
(α → β → m (ForInStep β)) →
m β
読み方は次の通りです。
ForIn m ρ α
は、
「モナド m の中で、コレクション型 ρ を、要素型 α として走査できる」
という意味です。
forIn の引数は：
ρ -- 走査対象
β -- ループ内部状態の型
β -- 初期状態
α → β → m (ForInStep β) -- 各要素に対する本体
m β -- 最終状態
ForInStep β は「続けるか、止めるか」を表します。公式リファレンスでは、done は break / return に対応し、yield は通常継続または continue に対応すると説明されています。 
inductive ForInStep (β : Type u) where
| done : β → ForInStep β
| yield : β → ForInStep β
典型例：for は ForIn に脱糖される
Functional Programming in Lean は、for ... in ... do が ForIn に脱糖され、ForIn は ForM より複雑で「状態」と「早期終了」を扱う、と説明しています。 
def sumList (xs : List Nat) : Nat := Id.run do
let mut acc := 0
for x in xs do
acc := acc + x
return acc
#eval sumList [1, 2, 3, 4]
-- 10
これは概念的には次のような状態渡しです。
def sumListExplicit (xs : List Nat) : Id Nat :=
ForIn.forIn xs 0 fun x acc =>
pure <| ForInStep.yield (acc + x)
#eval sumListExplicit [1, 2, 3, 4]
-- 10
break：ForInStep.done
def sumUntilGreaterThan10 (xs : List Nat) : Nat := Id.run do
let mut acc := 0
for x in xs do
if x > 10 then
break
acc := acc + x
return acc
#eval sumUntilGreaterThan10 [1, 2, 20, 3]
-- 3
対応するイメージは：
def sumUntilGreaterThan10Explicit (xs : List Nat) : Id Nat :=
ForIn.forIn xs 0 fun x acc =>
if x > 10 then
pure <| ForInStep.done acc
else
pure <| ForInStep.yield (acc + x)
return：ループだけでなく do ブロック全体から戻る
Functional Programming in Lean では、for ループ内の早期 return を使った List.find? の例が出ています。 
def find? (p : α → Bool) (xs : List α) : Option α := do
for x in xs do
if p x then
return x
failure
例：
#eval find? (fun n => n > 5) [1, 3, 8, 2]
-- some 8
#eval find? (fun n => n > 5) [1, 3, 4]
-- none
continue：今回の反復だけスキップ
同じく公式本では、continue によってループ本体の残りを飛ばせることが説明されています。 
def sumOdds (xs : List Nat) : Nat := Id.run do
let mut acc := 0
for x in xs do
if x % 2 == 0 then
continue
acc := acc + x
return acc
#eval sumOdds [1, 2, 3, 4, 5]
-- 9
ForM から ForIn を作る
Functional Programming in Lean では、ForM インスタンスから ForM.forIn によって ForIn インスタンスを作れると説明されています。ただし、そのアダプタは内部で StateT と ExceptT を使うため、モナドを一般化している ForM に対して使うものです。 
structure AllLessThan where
num : Nat
def AllLessThan.forM [Monad m]
(coll : AllLessThan)
(action : Nat → m PUnit) : m PUnit := do
let rec countdown : Nat → m PUnit
| 0 => pure ⟨⟩
| n + 1 => do
action n
countdown n
countdown coll.num
instance [Monad m] : ForM m AllLessThan Nat where
forM := AllLessThan.forM
instance [Monad m] : ForIn m AllLessThan Nat where
forIn := ForM.forIn
使用例：
def printLessThanFive : IO Unit := do
for i in ({ num := 5 } : AllLessThan) do
IO.println i
#eval printLessThanFive
-- 4
-- 3
-- 2
-- 1
-- 0
ForIn'：要素がコレクションに属する証拠つきループ
ForIn' は、各反復で a ∈ x の証明も本体に渡す強化版です。公式リファレンスでは、for h : x in xs do ... 形式で使うと説明されています。 
class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u)
(α : outParam (Type v))
(d : outParam (Membership α ρ)) where
forIn' :
{β : Type u₁} →
(x : ρ) →
β →
((a : α) → a ∈ x → β → m (ForInStep β)) →
m β
公式本の例では、範囲 [0:xs.size] を証拠つきで回すことで、xs[i] が安全なアクセスだと Lean に分からせています。 
def printArray [ToString α] (xs : Array α) : IO Unit := do
for h : i in [0:xs.size] do
IO.println s!"{i}:\t{xs[i]}"
ここで h は概念的に：
h : i ∈ [0:xs.size]
であり、Lean はそこから i < xs.size を導けます。
複数コレクションの並列ループ
Functional Programming in Lean は、複数の in 節をカンマで並べると並列に反復し、どれかが尽きた時点で停止すると説明しています。 
def parallelLoop : IO Unit := do
for x in ["currant", "gooseberry", "rowan"], y in [4:8] do
IO.println (x, y)
#eval parallelLoop
-- ("currant", 4)
-- ("gooseberry", 5)
-- ("rowan", 6)
注意：Lean 4.27 以降の変更
Lean 4.27.0 のリリースノートでは、ForIn、ForIn'、ForM のインターフェースが変更され、型クラス自体は Monad m パラメータを取らなくなり、下流の instance 側で [Monad m] を仮定する必要がある、と説明されています。 
したがって、古い記事やコードでは：
instance : ForIn m MyCollection α where
...
の周辺で Monad m の置き方が現在の Lean と合わない場合があります。現在は概ね：
instance [Monad m] : ForIn m MyCollection α where
...
の形に寄せるのが安全です。
まとめ
ForIn は「for x in xs do を使えるようにする型クラス」です。ForM が単純な全要素走査を表すのに対し、ForIn は let mut、break、continue、return を支えるために、内部状態 β と ForInStep β を扱います。証明つきの反復が必要なら ForIn' を使います。