diff --git a/src/Init/Data/Iterators/Combinators.lean b/src/Init/Data/Iterators/Combinators.lean
index 3081e2e81e..32823bdadf 100644
--- a/src/Init/Data/Iterators/Combinators.lean
+++ b/src/Init/Data/Iterators/Combinators.lean
@@ -8,4 +8,5 @@ module
 prelude
 public import Init.Data.Iterators.Combinators.Monadic
 public import Init.Data.Iterators.Combinators.FilterMap
+public import Init.Data.Iterators.Combinators.FlatMap
 public import Init.Data.Iterators.Combinators.ULift
diff --git a/src/Init/Data/Iterators/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Combinators/FlatMap.lean
new file mode 100644
index 0000000000..4b64c63c57
--- /dev/null
+++ b/src/Init/Data/Iterators/Combinators/FlatMap.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Combinators.FilterMap
+public import Init.Data.Iterators.Combinators.Monadic.FlatMap
+
+set_option doc.verso true
+
+/-!
+# {lit}`flatMap` combinator
+
+This file provides the {lit}`flatMap` iterator combinator and variants of it.
+
+If {lit}`it` is any iterator, {lit}`it.flatMap f` maps each output of {lit}`it` to an iterator using
+{lit}`f`.
+
+{lit}`it.flatMap f` first emits all outputs of the first obtained iterator, then of the second,
+and so on. In other words, {lit}`it` flattens the iterator of iterators obtained by mapping with
+{lit}`f`.
+-/
+
+namespace Std.Iterators
+
+@[always_inline, inherit_doc IterM.flatMapAfterM]
+public def Iter.flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [Iterator α₂ m γ]
+    (f : β → m (IterM (α := α₂) m γ)) (it₁ : Iter (α := α) β) (it₂ : Option (IterM (α := α₂) m γ)) :=
+  ((it₁.mapM pure).flatMapAfterM f it₂ : IterM m γ)
+
+@[always_inline, expose, inherit_doc IterM.flatMapM]
+public def Iter.flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [Iterator α₂ m γ]
+    (f : β → m (IterM (α := α₂) m γ)) (it : Iter (α := α) β) :=
+  (it.flatMapAfterM f none : IterM m γ)
+
+@[always_inline, inherit_doc IterM.flatMapAfter]
+public def Iter.flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    (f : β → Iter (α := α₂) γ) (it₁ : Iter (α := α) β) (it₂ : Option (Iter (α := α₂) γ)) :=
+  ((it₁.toIterM.flatMapAfter (fun b => (f b).toIterM) (Iter.toIterM <$> it₂)).toIter : Iter γ)
+
+@[always_inline, expose, inherit_doc IterM.flatMap]
+public def Iter.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    (f : β → Iter (α := α₂) γ) (it : Iter (α := α) β) :=
+  (it.flatMapAfter f none : Iter γ)
+
+end Std.Iterators
diff --git a/src/Init/Data/Iterators/Combinators/Monadic.lean b/src/Init/Data/Iterators/Combinators/Monadic.lean
index 0b908ab537..fbad749115 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic.lean
@@ -7,4 +7,5 @@ module
 
 prelude
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
+public import Init.Data.Iterators.Combinators.Monadic.FlatMap
 public import Init.Data.Iterators.Combinators.Monadic.ULift
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean
new file mode 100644
index 0000000000..5f268462ae
--- /dev/null
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean
@@ -0,0 +1,385 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Combinators.Monadic.FilterMap
+public import Init.Data.Option.Lemmas
+
+/-!
+# Monadic `flatMap` combinator
+
+This file provides the `flatMap` iterator combinator and variants of it.
+
+If `it` is any iterator, `it.flatMap f` maps each output of `it` to an iterator using
+`f`.
+
+`it.flatMap f` first emits all outputs of the first obtained iterator, then of the second,
+and so on. In other words, `it` flattens the iterator of iterators obtained by mapping with
+`f`.
+-/
+
+namespace Std.Iterators
+
+/-- Internal implementation detail of the `flatMap` combinator -/
+@[ext, unbox]
+public structure Flatten (α α₂ β : Type w) (m) where
+  it₁ : IterM (α := α) m (IterM (α := α₂) m β)
+  it₂ : Option (IterM (α := α₂) m β)
+
+/--
+Internal iterator combinator that is used to implement all `flatMap` variants
+-/
+@[always_inline]
+def IterM.flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    (it₁ : IterM (α := α) m (IterM (α := α₂) m β)) (it₂ : Option (IterM (α := α₂) m β)) :=
+  (toIterM (α := Flatten α α₂ β m) ⟨it₁, it₂⟩ m β : IterM m β)
+
+/--
+Let `it₁` and `it₂` be iterators and `f` a monadic function mapping `it₁`'s outputs to iterators
+of the same type as `it₂`. Then `it₁.flatMapAfterM f it₂` first goes over `it₂` and then over
+`it₁.flatMap f it₂`, emitting all their values.
+
+The main purpose of this combinator is to represent the intermediate state of a `flatMap` iterator
+that is currently iterating over one of the inner iterators.
+
+**Marble diagram (without monadic effects):**
+
+```text
+it₁                            --b      c    --d -⊥
+it₂                      a1-a2⊥
+f b                               b1-b2⊥
+f c                                      c1-c2⊥
+f d                                             ⊥
+it.flatMapAfterM f it₂   a1-a2----b1-b2--c1-c2----⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it₁`, `it₂` and the inner iterators are finite
+* `Productive` instance: only if `it₁` is finite and `it₂` and the inner iterators are productive
+
+For certain functions `f`, the resulting iterator will be finite (or productive) even though
+no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
+iterator is productive and the inner
+iterators are productive *and provably never empty*, then the resulting iterator is also productive.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it₁`, `it₂` or an internal
+iterator.
+
+For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
+-/
+@[always_inline]
+public def IterM.flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
+    (f : β → m (IterM (α := α₂) m γ)) (it₁ : IterM (α := α) m β) (it₂ : Option (IterM (α := α₂) m γ)) :=
+  ((it₁.mapM f).flattenAfter it₂ : IterM m γ)
+
+/--
+Let `it` be an iterator and `f` a monadic function mapping `it`'s outputs to iterators.
+Then `it.flatMapM f` is an iterator that goes over `it` and for each output, it applies `f` and
+iterates over the resulting iterator. `it.flatMapM f` emits all values obtained from the inner
+iterators -- first, all of the first inner iterator, then all of the second one, and so on.
+
+**Marble diagram (without monadic effects):**
+
+```text
+it                 ---a      --b      c    --d -⊥
+f a                    a1-a2⊥
+f b                             b1-b2⊥
+f c                                    c1-c2⊥
+f d                                           ⊥
+it.flatMapM        ----a1-a2----b1-b2--c1-c2----⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` and the inner iterators are finite
+* `Productive` instance: only if `it` is finite and the inner iterators are productive
+
+For certain functions `f`, the resulting iterator will be finite (or productive) even though
+no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
+iterator is productive and the inner
+iterators are productive *and provably never empty*, then the resulting iterator is also productive.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it` or an internal iterator.
+
+For each value emitted by the outer iterator `it`, this combinator calls `f`.
+-/
+@[always_inline, expose]
+public def IterM.flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
+    (f : β → m (IterM (α := α₂) m γ)) (it : IterM (α := α) m β) :=
+  (it.flatMapAfterM f none : IterM m γ)
+
+/--
+Let `it₁` and `it₂` be iterators and `f` a function mapping `it₁`'s outputs to iterators
+of the same type as `it₂`. Then `it₁.flatMapAfter f it₂` first goes over `it₂` and then over
+`it₁.flatMap f it₂`, emitting all their values.
+
+The main purpose of this combinator is to represent the intermediate state of a `flatMap` iterator
+that is currently iterating over one of the inner iterators.
+
+**Marble diagram:**
+
+```text
+it₁                            --b      c    --d -⊥
+it₂                      a1-a2⊥
+f b                               b1-b2⊥
+f c                                      c1-c2⊥
+f d                                             ⊥
+it.flatMapAfter  f it₂   a1-a2----b1-b2--c1-c2----⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it₁`, `it₂` and the inner iterators are finite
+* `Productive` instance: only if `it₁` is finite and `it₂` and the inner iterators are productive
+
+For certain functions `f`, the resulting iterator will be finite (or productive) even though
+no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
+iterator is productive and the inner
+iterators are productive *and provably never empty*, then the resulting iterator is also productive.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it₁`, `it₂` or an internal
+iterator.
+
+For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
+-/
+@[always_inline]
+public def IterM.flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
+    (f : β → IterM (α := α₂) m γ) (it₁ : IterM (α := α) m β) (it₂ : Option (IterM (α := α₂) m γ)) :=
+  ((it₁.map f).flattenAfter it₂ : IterM m γ)
+
+/--
+Let `it` be an iterator and `f` a function mapping `it`'s outputs to iterators.
+Then `it.flatMap f` is an iterator that goes over `it` and for each output, it applies `f` and
+iterates over the resulting iterator. `it.flatMap f` emits all values obtained from the inner
+iterators -- first, all of the first inner iterator, then all of the second one, and so on.
+
+**Marble diagram:**
+
+```text
+it                 ---a      --b      c    --d -⊥
+f a                    a1-a2⊥
+f b                             b1-b2⊥
+f c                                    c1-c2⊥
+f d                                           ⊥
+it.flatMap         ----a1-a2----b1-b2--c1-c2----⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` and the inner iterators are finite
+* `Productive` instance: only if `it` is finite and the inner iterators are productive
+
+For certain functions `f`, the resulting iterator will be finite (or productive) even though
+no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
+iterator is productive and the inner
+iterators are productive *and provably never empty*, then the resulting iterator is also productive.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it` or an internal iterator.
+
+For each value emitted by the outer iterator `it`, this combinator calls `f`.
+-/
+@[always_inline, expose]
+public def IterM.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
+    (f : β → IterM (α := α₂) m γ) (it : IterM (α := α) m β) :=
+  (it.flatMapAfter f none : IterM m γ)
+
+variable {α α₂ β : Type w} {m : Type w → Type w'}
+
+/-- The plausible-step predicate for `Flatten` iterators -/
+public inductive Flatten.IsPlausibleStep [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] :
+    (it : IterM (α := Flatten α α₂ β m) m β) → (step : IterStep (IterM (α := Flatten α α₂ β m) m β) β) → Prop where
+  | outerYield : ∀ {it₁ it₁' it₂'}, it₁.IsPlausibleStep (.yield it₁' it₂') →
+      IsPlausibleStep (toIterM ⟨it₁, none⟩ m β) (.skip (toIterM ⟨it₁', some it₂'⟩ m β))
+  | outerSkip : ∀ {it₁ it₁'}, it₁.IsPlausibleStep (.skip it₁') →
+      IsPlausibleStep (toIterM ⟨it₁, none⟩ m β) (.skip (toIterM ⟨it₁', none⟩ m β))
+  | outerDone : ∀ {it₁}, it₁.IsPlausibleStep .done →
+      IsPlausibleStep (toIterM ⟨it₁, none⟩ m β) .done
+  | innerYield : ∀ {it₁ it₂ it₂' b}, it₂.IsPlausibleStep (.yield it₂' b) →
+      IsPlausibleStep (toIterM ⟨it₁, some it₂⟩ m β) (.yield (toIterM ⟨it₁, some it₂'⟩ m β) b)
+  | innerSkip : ∀ {it₁ it₂ it₂'}, it₂.IsPlausibleStep (.skip it₂') →
+      IsPlausibleStep (toIterM ⟨it₁, some it₂⟩ m β) (.skip (toIterM ⟨it₁, some it₂'⟩ m β))
+  | innerDone : ∀ {it₁ it₂}, it₂.IsPlausibleStep .done →
+      IsPlausibleStep (toIterM ⟨it₁, some it₂⟩ m β) (.skip (toIterM ⟨it₁, none⟩ m β))
+
+public instance Flatten.instIterator [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] :
+    Iterator (Flatten α α₂ β m) m β where
+  IsPlausibleStep := IsPlausibleStep
+  step it :=
+    match it with
+    | ⟨it₁, none⟩ => do
+      match (← it₁.step).inflate with
+      | .yield it₁' it₂' h =>
+          pure <| .deflate <| .skip ⟨it₁', some it₂'⟩ (.outerYield h)
+      | .skip it₁' h =>
+          pure <| .deflate <| .skip ⟨it₁', none⟩ (.outerSkip h)
+      | .done h =>
+          pure <| .deflate <| .done (.outerDone h)
+    | ⟨it₁, some it₂⟩ => do
+      match (← it₂.step).inflate with
+      | .yield it₂' c h =>
+          pure <| .deflate <| .yield ⟨it₁, some it₂'⟩ c (.innerYield h)
+      | .skip it₂' h =>
+          pure <| .deflate <| .skip ⟨it₁, some it₂'⟩ (.innerSkip h)
+      | .done h =>
+          pure <| .deflate <| .skip ⟨it₁, none⟩ (.innerDone h)
+
+section Finite
+
+variable {α : Type w} {α₂ : Type w} {β : Type w} {m : Type w → Type w'}
+
+variable (α m β) in
+def Rel [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] [Finite α m] [Finite α₂ m] :
+    IterM (α := Flatten α α₂ β m) m β → IterM (α := Flatten α α₂ β m) m β → Prop :=
+  InvImage
+    (Prod.Lex
+      (InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps)
+      (Option.lt (InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps)))
+    (fun it => (it.internalState.it₁, it.internalState.it₂))
+
+theorem Flatten.rel_of_left [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    [Finite α m] [Finite α₂ m] {it it'}
+    (h : it'.internalState.it₁.finitelyManySteps.Rel it.internalState.it₁.finitelyManySteps) :
+    Rel α β m it' it :=
+  Prod.Lex.left _ _ h
+
+theorem Flatten.rel_of_right₁ [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    [Finite α m] [Finite α₂ m] {it₁ it₂ it₂'}
+    (h : (InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps) it₂' it₂) :
+    Rel α β m ⟨it₁, some it₂'⟩ ⟨it₁, some it₂⟩ := by
+  refine Prod.Lex.right _ h
+
+theorem Flatten.rel_of_right₂ [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    [Finite α m] [Finite α₂ m] {it₁ it₂} :
+    Rel α β m ⟨it₁, none⟩ ⟨it₁, some it₂⟩ :=
+  Prod.Lex.right _ True.intro
+
+instance [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    [Finite α m] [Finite α₂ m] :
+    FinitenessRelation (Flatten α α₂ β m) m where
+  rel := Rel α β m
+  wf := by
+    apply InvImage.wf
+    refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
+    · exact InvImage.wf _ WellFoundedRelation.wf
+    · exact Option.wellFounded_lt <| InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, h, h'⟩ := h
+    cases h' <;> cases h
+    case outerYield =>
+      apply Flatten.rel_of_left
+      exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
+    case outerSkip =>
+      apply Flatten.rel_of_left
+      exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
+    case innerYield =>
+      apply Flatten.rel_of_right₁
+      exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
+    case innerSkip =>
+      apply Flatten.rel_of_right₁
+      exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
+    case innerDone =>
+      apply Flatten.rel_of_right₂
+
+@[no_expose]
+public instance [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    [Finite α m] [Finite α₂ m] : Finite (Flatten α α₂ β m) m :=
+  .of_finitenessRelation instFinitenessRelationFlattenOfIterMOfFinite
+
+end Finite
+
+section Productive
+
+variable {α : Type w} {α₂ : Type w} {β : Type w} {m : Type w → Type w'}
+
+variable (α m β) in
+def ProductiveRel [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] [Finite α m]
+    [Productive α₂ m] :
+    IterM (α := Flatten α α₂ β m) m β → IterM (α := Flatten α α₂ β m) m β → Prop :=
+  InvImage
+    (Prod.Lex
+      (InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps)
+      (Option.lt (InvImage IterM.TerminationMeasures.Productive.Rel IterM.finitelyManySkips)))
+    (fun it => (it.internalState.it₁, it.internalState.it₂))
+
+theorem Flatten.productiveRel_of_left [Monad m] [Iterator α m (IterM (α := α₂) m β)]
+    [Iterator α₂ m β] [Finite α m] [Productive α₂ m] {it it'}
+    (h : it'.internalState.it₁.finitelyManySteps.Rel it.internalState.it₁.finitelyManySteps) :
+    ProductiveRel α β m it' it :=
+  Prod.Lex.left _ _ h
+
+theorem Flatten.productiveRel_of_right₁ [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    [Finite α m] [Productive α₂ m] {it₁ it₂ it₂'}
+    (h : (InvImage IterM.TerminationMeasures.Productive.Rel IterM.finitelyManySkips) it₂' it₂) :
+    ProductiveRel α β m ⟨it₁, some it₂'⟩ ⟨it₁, some it₂⟩ := by
+  refine Prod.Lex.right _ h
+
+theorem Flatten.productiveRel_of_right₂ [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    [Finite α m] [Productive α₂ m] {it₁ it₂} :
+    ProductiveRel α β m ⟨it₁, none⟩ ⟨it₁, some it₂⟩ :=
+  Prod.Lex.right _ True.intro
+
+instance [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    [Finite α m] [Productive α₂ m] :
+    ProductivenessRelation (Flatten α α₂ β m) m where
+  rel := ProductiveRel α β m
+  wf := by
+    apply InvImage.wf
+    refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
+    · exact InvImage.wf _ WellFoundedRelation.wf
+    · exact Option.wellFounded_lt <| InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    cases h
+    case outerYield =>
+      apply Flatten.productiveRel_of_left
+      exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
+    case outerSkip =>
+      apply Flatten.productiveRel_of_left
+      exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
+    case innerSkip =>
+      apply Flatten.productiveRel_of_right₁
+      exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›
+    case innerDone =>
+      apply Flatten.productiveRel_of_right₂
+
+@[no_expose]
+public instance [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    [Finite α m] [Productive α₂ m] : Productive (Flatten α α₂ β m) m :=
+  .of_productivenessRelation instProductivenessRelationFlattenOfFiniteIterMOfProductive
+
+end Productive
+
+public instance Flatten.instIteratorCollect [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
+    [Iterator α₂ m β] : IteratorCollect (Flatten α α₂ β m) m n :=
+  .defaultImplementation
+
+public instance Flatten.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
+    [Iterator α₂ m β] : IteratorCollectPartial (Flatten α α₂ β m) m n :=
+  .defaultImplementation
+
+public instance Flatten.instIteratorLoop [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
+    [Iterator α₂ m β] : IteratorLoop (Flatten α α₂ β m) m n :=
+  .defaultImplementation
+
+public instance Flatten.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
+    [Iterator α₂ m β] : IteratorLoopPartial (Flatten α α₂ β m) m n :=
+  .defaultImplementation
+
+end Std.Iterators
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators.lean b/src/Init/Data/Iterators/Lemmas/Combinators.lean
index c7671bc49f..f526200cde 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators.lean
@@ -9,4 +9,5 @@ prelude
 public import Init.Data.Iterators.Lemmas.Combinators.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic
 public import Init.Data.Iterators.Lemmas.Combinators.FilterMap
+public import Init.Data.Iterators.Lemmas.Combinators.FlatMap
 public import Init.Data.Iterators.Lemmas.Combinators.ULift
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
new file mode 100644
index 0000000000..6a57b3d362
--- /dev/null
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
@@ -0,0 +1,266 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Lemmas.Combinators.FilterMap
+public import Init.Data.Iterators.Combinators.FlatMap
+import all Init.Data.Iterators.Combinators.FlatMap
+public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
+
+namespace Std.Iterators
+open Std.Internal
+
+public theorem Flatten.IsPlausibleStep.outerYield_flatMapM_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ it₁' : Iter (α := α) β} {it₂' b}
+    (h : it₁.IsPlausibleStep (.yield it₁' b)) :
+    (it₁.flatMapAfterM f none).IsPlausibleStep (.skip (it₁'.flatMapAfterM f (some it₂'))) := by
+  apply outerYield_flatMapM
+  exact .yieldSome h (out' := b) (by simp [PostconditionT.lift, PostconditionT.bind])
+
+public theorem Flatten.IsPlausibleStep.outerSkip_flatMapM_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ it₁' : Iter (α := α) β}
+    (h : it₁.IsPlausibleStep (.skip it₁')) :
+    (it₁.flatMapAfterM f none).IsPlausibleStep (.skip (it₁'.flatMapAfterM f none)) :=
+  outerSkip_flatMapM (.skip h)
+
+public theorem Flatten.IsPlausibleStep.outerDone_flatMapM_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : Iter (α := α) β}
+    (h : it₁.IsPlausibleStep .done) :
+    (it₁.flatMapAfterM f none).IsPlausibleStep .done :=
+  outerDone_flatMapM (.done h)
+
+public theorem Flatten.IsPlausibleStep.innerYield_flatMapM_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : Iter (α := α) β} {it₂ it₂' b}
+    (h : it₂.IsPlausibleStep (.yield it₂' b)) :
+    (it₁.flatMapAfterM f (some it₂)).IsPlausibleStep (.yield (it₁.flatMapAfterM f (some it₂')) b) :=
+  innerYield_flatMapM h
+
+public theorem Flatten.IsPlausibleStep.innerSkip_flatMapM_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : Iter (α := α) β} {it₂ it₂'}
+    (h : it₂.IsPlausibleStep (.skip it₂')) :
+    (it₁.flatMapAfterM f (some it₂)).IsPlausibleStep (.skip (it₁.flatMapAfterM f (some it₂'))) :=
+  innerSkip_flatMapM h
+
+public theorem Flatten.IsPlausibleStep.innerDone_flatMapM_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : Iter (α := α) β} {it₂}
+    (h : it₂.IsPlausibleStep .done) :
+    (it₁.flatMapAfterM f (some it₂)).IsPlausibleStep (.skip (it₁.flatMapAfterM f none)) :=
+  innerDone_flatMapM h
+
+public theorem Flatten.IsPlausibleStep.outerYield_flatMap_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    {f : β → Iter (α := α₂) γ} {it₁ it₁' : Iter (α := α) β} {b}
+    (h : it₁.IsPlausibleStep (.yield it₁' b)) :
+    (it₁.flatMapAfter f none).IsPlausibleStep (.skip (it₁'.flatMapAfter f (some (f b)))) :=
+  outerYield_flatMap h
+
+public theorem Flatten.IsPlausibleStep.outerSkip_flatMap_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    {f : β → Iter (α := α₂) γ} {it₁ it₁' : Iter (α := α) β}
+    (h : it₁.IsPlausibleStep (.skip it₁')) :
+    (it₁.flatMapAfter f none).IsPlausibleStep (.skip (it₁'.flatMapAfter f none)) :=
+  outerSkip_flatMap h
+
+public theorem Flatten.IsPlausibleStep.outerDone_flatMap_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w}  [Iterator α Id β] [Iterator α₂ Id γ]
+    {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β}
+    (h : it₁.IsPlausibleStep .done) :
+    (it₁.flatMapAfter f none).IsPlausibleStep .done :=
+  outerDone_flatMap h
+
+public theorem Flatten.IsPlausibleStep.innerYield_flatMap_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ it₂' b}
+    (h : it₂.IsPlausibleStep (.yield it₂' b)) :
+    (it₁.flatMapAfter f (some it₂)).IsPlausibleStep (.yield (it₁.flatMapAfter f (some it₂')) b) :=
+  innerYield_flatMap h
+
+public theorem Flatten.IsPlausibleStep.innerSkip_flatMap_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ it₂'}
+    (h : it₂.IsPlausibleStep (.skip it₂')) :
+    (it₁.flatMapAfter f (some it₂)).IsPlausibleStep (.skip (it₁.flatMapAfter f (some it₂'))) :=
+  innerSkip_flatMap h
+
+public theorem Flatten.IsPlausibleStep.innerDone_flatMap_pure {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂}
+    (h : it₂.IsPlausibleStep .done) :
+    (it₁.flatMapAfter f (some it₂)).IsPlausibleStep (.skip (it₁.flatMapAfter f none)) :=
+  innerDone_flatMap h
+
+public theorem Iter.step_flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : Iter (α := α) β} {it₂ : Option (IterM (α := α₂) m γ)} :
+  (it₁.flatMapAfterM f it₂).step = (do
+    match it₂ with
+    | none =>
+      match it₁.step with
+      | .yield it₁' b h =>
+        return .deflate (.skip (it₁'.flatMapAfterM f (some (← f b))) (.outerYield_flatMapM_pure h))
+      | .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfterM f none) (.outerSkip_flatMapM_pure h))
+      | .done h => return .deflate (.done (.outerDone_flatMapM_pure h))
+    | some it₂ =>
+      match (← it₂.step).inflate with
+      | .yield it₂' out h =>
+        return .deflate (.yield (it₁.flatMapAfterM f (some it₂')) out (.innerYield_flatMapM_pure h))
+      | .skip it₂' h =>
+        return .deflate (.skip (it₁.flatMapAfterM f (some it₂')) (.innerSkip_flatMapM_pure h))
+      | .done h =>
+        return .deflate (.skip (it₁.flatMapAfterM f none) (.innerDone_flatMapM_pure h))) := by
+  simp only [flatMapAfterM, IterM.step_flatMapAfterM, Iter.step_mapM]
+  split
+  · split <;> simp [*]
+  · rfl
+
+public theorem Iter.step_flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : Iter (α := α) β} :
+  (it₁.flatMapM f).step = (do
+    match it₁.step with
+    | .yield it₁' b h =>
+      return .deflate (.skip (it₁'.flatMapAfterM f (some (← f b))) (.outerYield_flatMapM_pure h))
+    | .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfterM f none) (.outerSkip_flatMapM_pure h))
+    | .done h => return .deflate (.done (.outerDone_flatMapM_pure h))) := by
+  simp [flatMapM, step_flatMapAfterM]
+
+public theorem Iter.step_flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
+  (it₁.flatMapAfter f it₂).step = (match it₂ with
+    | none =>
+      match it₁.step with
+      | .yield it₁' b h =>
+        .skip (it₁'.flatMapAfter f (some (f b))) (.outerYield_flatMap_pure h)
+      | .skip it₁' h => .skip (it₁'.flatMapAfter f none) (.outerSkip_flatMap_pure h)
+      | .done h => .done (.outerDone_flatMap_pure h)
+    | some it₂ =>
+      match it₂.step with
+      | .yield it₂' out h => .yield (it₁.flatMapAfter f (some it₂')) out (.innerYield_flatMap_pure h)
+      | .skip it₂' h => .skip (it₁.flatMapAfter f (some it₂')) (.innerSkip_flatMap_pure h)
+      | .done h => .skip (it₁.flatMapAfter f none) (.innerDone_flatMap_pure h)) := by
+  simp only [flatMapAfter, step, toIterM_toIter, IterM.step_flatMapAfter]
+  cases it₂
+  · simp only [Option.map_eq_map, Option.map_none, Id.run_bind, Option.map_some]
+    cases it₁.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
+  · rename_i it₂
+    simp only [Option.map_eq_map, Option.map_some, Id.run_bind, Option.map_none]
+    cases it₂.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
+
+public theorem Iter.step_flatMap {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} :
+  (it₁.flatMap f).step = (match it₁.step with
+    | .yield it₁' b h =>
+      .skip (it₁'.flatMapAfter f (some (f b))) (.outerYield_flatMap_pure h)
+    | .skip it₁' h => .skip (it₁'.flatMapAfter f none) (.outerSkip_flatMap_pure h)
+    | .done h => .done (.outerDone_flatMap_pure h)) := by
+  simp [flatMap, step_flatMapAfter]
+
+public theorem Iter.toList_flatMapAfterM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] [Finite α Id] [Finite α₂ m]
+    [IteratorCollect α Id m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α Id m] [LawfulIteratorCollect α₂ m m]
+    {f : β → m (IterM (α := α₂) m γ)}
+    {it₁ : Iter (α := α) β} {it₂ : Option (IterM (α := α₂) m γ)} :
+    (it₁.flatMapAfterM f it₂).toList = do
+      match it₂ with
+      | none => List.flatten <$> (it₁.mapM fun b => do (← f b).toList).toList
+      | some it₂ => return (← it₂.toList) ++
+          (← List.flatten <$> (it₁.mapM fun b => do (← f b).toList).toList) := by
+  simp only [flatMapAfterM, IterM.toList_flatMapAfterM]
+  split
+  · simp only [mapM, IterM.toList_mapM_mapM, monadLift_self]
+    congr <;> simp
+  · apply bind_congr; intro step
+    simp only [mapM, IterM.toList_mapM_mapM, monadLift_self, bind_pure_comp, Functor.map_map]
+    congr <;> simp
+
+public theorem Iter.toArray_flatMapAfterM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] [Finite α Id] [Finite α₂ m]
+    [IteratorCollect α Id m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α Id m] [LawfulIteratorCollect α₂ m m]
+    {f : β → m (IterM (α := α₂) m γ)}
+    {it₁ : Iter (α := α) β} {it₂ : Option (IterM (α := α₂) m γ)} :
+    (it₁.flatMapAfterM f it₂).toArray = do
+      match it₂ with
+      | none => Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray
+      | some it₂ => return (← it₂.toArray) ++
+          (← Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray) := by
+  simp only [flatMapAfterM, IterM.toArray_flatMapAfterM]
+  split
+  · simp only [mapM, IterM.toArray_mapM_mapM, monadLift_self]
+    congr <;> simp
+  · apply bind_congr; intro step
+    simp only [mapM, IterM.toArray_mapM_mapM, monadLift_self, bind_pure_comp, Functor.map_map]
+    congr <;> simp
+
+public theorem Iter.toList_flatMapM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] [Finite α Id] [Finite α₂ m]
+    [IteratorCollect α Id m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α Id m] [LawfulIteratorCollect α₂ m m]
+    {f : β → m (IterM (α := α₂) m γ)}
+    {it₁ : Iter (α := α) β} :
+    (it₁.flatMapM f).toList = List.flatten <$> (it₁.mapM fun b => do (← f b).toList).toList := by
+  simp [flatMapM, toList_flatMapAfterM]
+
+public theorem Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] [Finite α Id] [Finite α₂ m]
+    [IteratorCollect α Id m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α Id m] [LawfulIteratorCollect α₂ m m]
+    {f : β → m (IterM (α := α₂) m γ)}
+    {it₁ : Iter (α := α) β} :
+    (it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by
+  simp [flatMapM, toArray_flatMapAfterM]
+
+public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    [Finite α Id] [Finite α₂ Id] [IteratorCollect α Id Id] [IteratorCollect α₂ Id Id]
+    [LawfulIteratorCollect α Id Id] [LawfulIteratorCollect α₂ Id Id]
+    {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
+    (it₁.flatMapAfter f it₂).toList = match it₂ with
+      | none => (it₁.map fun b => (f b).toList).toList.flatten
+      | some it₂ => it₂.toList ++
+          (it₁.map fun b => (f b).toList).toList.flatten := by
+  simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter]
+  cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM]
+
+public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    [Finite α Id] [Finite α₂ Id] [IteratorCollect α Id Id] [IteratorCollect α₂ Id Id]
+    [LawfulIteratorCollect α Id Id] [LawfulIteratorCollect α₂ Id Id]
+    {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
+    (it₁.flatMapAfter f it₂).toArray = match it₂ with
+      | none => (it₁.map fun b => (f b).toArray).toArray.flatten
+      | some it₂ => it₂.toArray ++
+          (it₁.map fun b => (f b).toArray).toArray.flatten := by
+  simp only [flatMapAfter, Iter.toArray, toIterM_toIter, IterM.toArray_flatMapAfter]
+  cases it₂ <;> simp [map, IterM.toArray_map_eq_toArray_mapM]
+
+public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    [Finite α Id] [Finite α₂ Id]
+    [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id]
+    [IteratorCollect α Id Id] [IteratorCollect α₂ Id Id]
+    [LawfulIteratorCollect α Id Id] [LawfulIteratorCollect α₂ Id Id]
+    {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} :
+    (it₁.flatMap f).toList = (it₁.map fun b => (f b).toList).toList.flatten := by
+  simp [flatMap, toList_flatMapAfter]
+
+public theorem Iter.toArray_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
+    [Finite α Id] [Finite α₂ Id]
+    [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id]
+    [IteratorCollect α Id Id] [IteratorCollect α₂ Id Id]
+    [LawfulIteratorCollect α Id Id] [LawfulIteratorCollect α₂ Id Id]
+    {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} :
+    (it₁.flatMap f).toArray = (it₁.map fun b => (f b).toArray).toArray.flatten := by
+  simp [flatMap, toArray_flatMapAfter]
+
+end Std.Iterators
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean
index 9821eb5856..d3304e480f 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean
@@ -8,4 +8,5 @@ module
 prelude
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
+public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index d0896ebe1e..c6de07a743 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -291,19 +291,164 @@ theorem IterM.InternalConsumers.toList_filterMap {α β γ: Type w} {m : Type w
   intro step
   cases step.inflate using PlausibleIterStep.casesOn
   · simp only [List.filterMap_cons, bind_assoc, pure_bind]
-    split
-    · split
-      · simp only [bind_pure_comp, pure_bind, Shrink.inflate_deflate]
-        exact ihy ‹_›
-      · simp_all
-    · split
-      · simp_all
-      · simp_all [ihy ‹_›]
-  · simp only [bind_pure_comp, pure_bind, Shrink.inflate_deflate]
-    apply ihs
-    assumption
+    split <;> simp (discharger := assumption) [*]
+  · simp [ihs ‹_›]
   · simp
 
+theorem IterM.toList_map_eq_toList_mapM {α β γ : Type w}
+    {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → γ} {it : IterM (α := α) m β} :
+    (it.map f).toList = (it.mapM fun b => pure (f b)).toList := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [toList_eq_match_step, toList_eq_match_step, step_map, step_mapM, bind_assoc, bind_assoc]
+  apply bind_congr; intro step
+  split <;> simp (discharger := assumption) [ihy, ihs]
+
+theorem IterM.toList_mapM_eq_toList_filterMapM {α β γ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n][LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
+    {f : β → n γ} {it : IterM (α := α) m β} :
+    (it.mapM f).toList =
+      (it.filterMapM fun b => some <$> f b).toList := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [toList_eq_match_step, toList_eq_match_step, step_mapM, step_filterMapM, bind_assoc, bind_assoc]
+  apply bind_congr; intro step
+  split <;> simp (discharger := assumption) [ihy, ihs]
+
+theorem IterM.toList_map_eq_toList_filterMapM {α β γ : Type w}
+    {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → γ} {it : IterM (α := α) m β} :
+    (it.map f).toList = (it.filterMapM fun b => pure (some (f b))).toList := by
+  simp [toList_map_eq_toList_mapM, toList_mapM_eq_toList_filterMapM]
+  congr <;> simp
+
+@[simp]
+theorem IterM.toList_filterMapM_filterMapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → n (Option γ)} {g : γ → o (Option δ)}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.filterMapM f).filterMapM g).toList =
+      (it.filterMapM (n := o) (fun b => do
+        match ← f b with
+        | none => return none
+        | some fb => g fb)).toList := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  letI : MonadLift n o := ⟨monadLift⟩
+  haveI : LawfulMonadLift n o := ⟨by simp [this], by simp [this]⟩
+  rw [toList_eq_match_step, toList_eq_match_step, step_filterMapM,
+    bind_assoc, step_filterMapM, step_filterMapM]
+  simp only [bind_assoc, liftM_bind]
+  apply bind_congr; intro step
+  split
+  · simp only [bind_assoc, liftM_bind]
+    apply bind_congr; intro fx
+    split
+    · simp [ihy ‹_›]
+    · simp only [liftM_pure, PlausibleIterStep.skip, pure_bind, bind_assoc, Shrink.inflate_deflate]
+      apply bind_congr; intro gx
+      split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+@[simp]
+theorem IterM.toList_filterMapM_mapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    {f : β → n γ} {g : γ → o (Option δ)}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.mapM f).filterMapM g).toList =
+      (it.filterMapM (n := o) (fun b => do g (← f b))).toList := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  letI : MonadLift n o := ⟨monadLift⟩
+  haveI : LawfulMonadLift n o := ⟨by simp [this], by simp [this]⟩
+  rw [toList_eq_match_step, toList_eq_match_step, step_filterMapM,
+    bind_assoc, step_filterMapM, step_mapM]
+  simp only [bind_assoc, liftM_bind]
+  apply bind_congr; intro step
+  split
+  · simp only [bind_assoc, liftM_bind]
+    apply bind_congr; intro fx
+    simp only [liftM_pure, pure_bind, bind_assoc, Shrink.inflate_deflate]
+    apply bind_congr; intro gx
+    split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+@[simp]
+theorem IterM.toList_filterMapM_map {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m]
+    {f : β → γ} {g : γ → n (Option δ)}
+    {it : IterM (α := α) m β} :
+    ((it.map f).filterMapM g).toList =
+      (it.filterMapM (n := n) (fun b => g (f b))).toList := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [toList_eq_match_step, toList_eq_match_step, step_filterMapM,
+    bind_assoc, step_filterMapM, step_map]
+  simp only [bind_assoc, liftM_bind]
+  apply bind_congr; intro step
+  split
+  · simp only [bind_assoc, liftM_pure, pure_bind, Shrink.inflate_deflate]
+    apply bind_congr; intro fx
+    split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+@[simp]
+theorem IterM.toList_mapM_filterMapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → n (Option γ)} {g : γ → o δ}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.filterMapM f).mapM g).toList =
+      (it.filterMapM (n := o) (fun b => do
+        match ← f b with
+        | none => return none
+        | some fb => some <$> g fb)).toList := by
+  simp [toList_mapM_eq_toList_filterMapM, toList_filterMapM_filterMapM]
+
+@[simp]
+theorem IterM.toList_mapM_mapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m o] [LawfulIteratorCollect α m o]
+    {f : β → n γ} {g : γ → o δ}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.mapM f).mapM g).toList =
+      (it.mapM (n := o) (fun b => do g (← f b))).toList := by
+  simp only [toList_mapM_eq_toList_filterMapM, toList_filterMapM_mapM]
+  congr <;> simp
+
+@[simp]
+theorem IterM.toList_mapM_map {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
+    {f : β → γ} {g : γ → n δ}
+    {it : IterM (α := α) m β} :
+    ((it.map f).mapM g).toList =
+      (it.mapM (n := n) (fun b => g (f b))).toList := by
+  simp [toList_mapM_eq_toList_filterMapM]
+
 theorem IterM.toList_filterMap {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m]
     [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
@@ -371,6 +516,30 @@ end ToList
 
 section ToListRev
 
+theorem IterM.toListRev_map_eq_toListRev_mapM {α β γ : Type w}
+    {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → γ} {it : IterM (α := α) m β} :
+    (it.map f).toListRev = (it.mapM fun b => pure (f b)).toListRev := by
+  simp [toListRev_eq, toList_map_eq_toList_mapM]
+
+theorem IterM.toListRev_mapM_eq_toListRev_filterMapM {α β γ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n][LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
+    {f : β → n γ} {it : IterM (α := α) m β} :
+    (it.mapM f).toListRev =
+      (it.filterMapM fun b => some <$> f b).toListRev := by
+  simp [toListRev_eq, toList_mapM_eq_toList_filterMapM]
+
+theorem IterM.toListRev_map_eq_toListRev_filterMapM {α β γ : Type w}
+    {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → γ} {it : IterM (α := α) m β} :
+    (it.map f).toListRev = (it.filterMapM fun b => pure (some (f b))).toListRev := by
+  simp [toListRev_eq, toList_map_eq_toList_filterMapM]
+
 theorem IterM.toListRev_filterMap {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m]
     [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
@@ -390,10 +559,115 @@ theorem IterM.toListRev_filter {α β : Type w} {m : Type w → Type w'} [Monad
     (it.filter f).toListRev = List.filter f <$> it.toListRev := by
   simp [toListRev_eq, toList_filter]
 
+@[simp]
+theorem IterM.toListRev_filterMapM_filterMapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → n (Option γ)} {g : γ → o (Option δ)}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.filterMapM f).filterMapM g).toListRev =
+      (it.filterMapM (n := o) (fun b => do
+        match ← f b with
+        | none => return none
+        | some fb => g fb)).toListRev := by
+  simp [toListRev_eq]
+
+@[simp]
+theorem IterM.toListRev_filterMapM_mapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → n γ} {g : γ → o (Option δ)}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.mapM f).filterMapM g).toListRev =
+      (it.filterMapM (n := o) (fun b => do g (← f b))).toListRev := by
+  simp [toListRev_eq]
+
+@[simp]
+theorem IterM.toListRev_filterMapM_map {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → γ} {g : γ → n (Option δ)}
+    {it : IterM (α := α) m β} :
+    ((it.map f).filterMapM g).toListRev =
+      (it.filterMapM (n := n) (fun b => g (f b))).toListRev := by
+  simp [toListRev_eq]
+
+@[simp]
+theorem IterM.toListRev_mapM_filterMapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → n (Option γ)} {g : γ → o δ}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.filterMapM f).mapM g).toListRev =
+      (it.filterMapM (n := o) (fun b => do
+        match ← f b with
+        | none => return none
+        | some fb => some <$> g fb)).toListRev := by
+  simp [toListRev_eq]
+
+@[simp]
+theorem IterM.toListRev_mapM_mapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    {f : β → n γ} {g : γ → o δ}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.mapM f).mapM g).toListRev =
+      (it.mapM (n := o) (fun b => do g (← f b))).toListRev := by
+  letI : IteratorCollect α m o := .defaultImplementation
+  simp [toListRev_eq]
+
+@[simp]
+theorem IterM.toListRev_mapM_map {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] {f : β → γ} {g : γ → n δ} {it : IterM (α := α) m β} :
+    ((it.map f).mapM g).toListRev =
+      (it.mapM (n := n) (fun b => g (f b))).toListRev := by
+  letI : IteratorCollect α m n := .defaultImplementation
+  simp [toListRev_eq]
+
 end ToListRev
 
 section ToArray
 
+theorem IterM.toArray_map_eq_toArray_mapM {α β γ : Type w}
+    {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → γ} {it : IterM (α := α) m β} :
+    (it.map f).toArray = (it.mapM fun b => pure (f b)).toArray := by
+  simp [← toArray_toList, toList_map_eq_toList_mapM]
+
+theorem IterM.toArray_mapM_eq_toArray_filterMapM {α β γ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n][LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
+    {f : β → n γ} {it : IterM (α := α) m β} :
+    (it.mapM f).toArray = (it.filterMapM fun b => some <$> f b).toArray := by
+  simp [← toArray_toList, toList_mapM_eq_toList_filterMapM]
+
+theorem IterM.toArray_map_eq_toArray_filterMapM {α β γ : Type w}
+    {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → γ} {it : IterM (α := α) m β} :
+    (it.map f).toArray = (it.filterMapM fun b => pure (some (f b))).toArray := by
+  simp [← toArray_toList, toList_map_eq_toList_filterMapM]
+
 theorem IterM.toArray_filterMap {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m]
     [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
@@ -413,6 +687,88 @@ theorem IterM.toArray_filter {α : Type w} {m : Type w → Type w'} [Monad m] [L
     (it.filter f).toArray = Array.filter f <$> it.toArray := by
   simp [← toArray_toList, toList_filter]
 
+@[simp]
+theorem IterM.toArray_filterMapM_filterMapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → n (Option γ)} {g : γ → o (Option δ)}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.filterMapM f).filterMapM g).toArray =
+      (it.filterMapM (n := o) (fun b => do
+        match ← f b with
+        | none => return none
+        | some fb => g fb)).toArray := by
+  simp [← toArray_toList]
+
+@[simp]
+theorem IterM.toArray_filterMapM_mapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → n γ} {g : γ → o (Option δ)}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.mapM f).filterMapM g).toArray =
+      (it.filterMapM (n := o) (fun b => do g (← f b))).toArray := by
+  simp [← toArray_toList]
+
+@[simp]
+theorem IterM.toArray_filterMapM_map {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → γ} {g : γ → n (Option δ)}
+    {it : IterM (α := α) m β} :
+    ((it.map f).filterMapM g).toArray =
+      (it.filterMapM (n := n) (fun b => g (f b))).toArray := by
+  simp [← toArray_toList]
+
+@[simp]
+theorem IterM.toArray_mapM_filterMapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {f : β → n (Option γ)} {g : γ → o δ}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.filterMapM f).mapM g).toArray =
+      (it.filterMapM (n := o) (fun b => do
+        match ← f b with
+        | none => return none
+        | some fb => some <$> g fb)).toArray := by
+  simp [← toArray_toList]
+
+@[simp]
+theorem IterM.toArray_mapM_mapM {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m o] [LawfulIteratorCollect α m o]
+    {f : β → n γ} {g : γ → o δ}
+    {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    ((it.mapM f).mapM g).toArray =
+      (it.mapM (n := o) (fun b => do g (← f b))).toArray := by
+  simp [← toArray_toList]
+
+@[simp]
+theorem IterM.toArray_mapM_map {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''}
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
+    {f : β → γ} {g : γ → n δ}
+    {it : IterM (α := α) m β} :
+    ((it.map f).mapM g).toArray =
+      (it.mapM (n := n) (fun b => g (f b))).toArray := by
+  simp [← toArray_toList]
+
 end ToArray
 
 section Fold
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean
new file mode 100644
index 0000000000..023bda777e
--- /dev/null
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean
@@ -0,0 +1,344 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
+
+public import Init.Data.Iterators.Combinators.Monadic.FlatMap
+import all Init.Data.Iterators.Combinators.Monadic.FlatMap
+
+namespace Std.Iterators
+open Std.Internal
+
+theorem IterM.step_flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
+    {it₁ : IterM (α := α) m (IterM (α := α₂) m β)} {it₂ : Option (IterM (α := α₂) m β)} :
+  (it₁.flattenAfter it₂).step = (do
+    match it₂ with
+    | none =>
+      match (← it₁.step).inflate with
+      | .yield it₁' it₂' h => return .deflate (.skip (it₁'.flattenAfter (some it₂')) (.outerYield h))
+      | .skip it₁' h => return .deflate (.skip (it₁'.flattenAfter none) (.outerSkip h))
+      | .done h => return .deflate (.done (.outerDone h))
+    | some it₂ =>
+      match (← it₂.step).inflate with
+      | .yield it₂' out h => return .deflate (.yield (it₁.flattenAfter (some it₂')) out (.innerYield h))
+      | .skip it₂' h => return .deflate (.skip (it₁.flattenAfter (some it₂')) (.innerSkip h))
+      | .done h => return .deflate (.skip (it₁.flattenAfter none) (.innerDone h))) := by
+  cases it₂
+  all_goals
+  · apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.flattenAfter, toIterM]
+
+public theorem Flatten.IsPlausibleStep.outerYield_flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ it₁' : IterM (α := α) m β} {it₂' b}
+    (h : it₁.IsPlausibleStep (.yield it₁' b)) :
+    (it₁.flatMapAfterM f none).IsPlausibleStep (.skip (it₁'.flatMapAfterM f (some it₂'))) :=
+  .outerYield (.yieldSome h ⟨⟨_, trivial⟩, rfl⟩)
+
+public theorem Flatten.IsPlausibleStep.outerSkip_flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ it₁' : IterM (α := α) m β}
+    (h : it₁.IsPlausibleStep (.skip it₁')) :
+    (it₁.flatMapAfterM f none).IsPlausibleStep (.skip (it₁'.flatMapAfterM f none)) :=
+  .outerSkip (.skip h)
+
+public theorem Flatten.IsPlausibleStep.outerDone_flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : IterM (α := α) m β}
+    (h : it₁.IsPlausibleStep .done) :
+    (it₁.flatMapAfterM f none).IsPlausibleStep .done :=
+  .outerDone (.done h)
+
+public theorem Flatten.IsPlausibleStep.innerYield_flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : IterM (α := α) m β} {it₂ it₂' b}
+    (h : it₂.IsPlausibleStep (.yield it₂' b)) :
+    (it₁.flatMapAfterM f (some it₂)).IsPlausibleStep (.yield (it₁.flatMapAfterM f (some it₂')) b) :=
+  .innerYield h
+
+public theorem Flatten.IsPlausibleStep.innerSkip_flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : IterM (α := α) m β} {it₂ it₂'}
+    (h : it₂.IsPlausibleStep (.skip it₂')) :
+    (it₁.flatMapAfterM f (some it₂)).IsPlausibleStep (.skip (it₁.flatMapAfterM f (some it₂'))) :=
+  .innerSkip h
+
+public theorem Flatten.IsPlausibleStep.innerDone_flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : IterM (α := α) m β} {it₂}
+    (h : it₂.IsPlausibleStep .done) :
+    (it₁.flatMapAfterM f (some it₂)).IsPlausibleStep (.skip (it₁.flatMapAfterM f none)) :=
+  .innerDone h
+
+public theorem Flatten.IsPlausibleStep.outerYield_flatMap {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → IterM (α := α₂) m γ} {it₁ it₁' : IterM (α := α) m β} {b}
+    (h : it₁.IsPlausibleStep (.yield it₁' b)) :
+    (it₁.flatMapAfter f none).IsPlausibleStep (.skip (it₁'.flatMapAfter f (some (f b)))) :=
+  .outerYield (.yieldSome h ⟨⟨_, rfl⟩, rfl⟩)
+
+public theorem Flatten.IsPlausibleStep.outerSkip_flatMap {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → IterM (α := α₂) m γ} {it₁ it₁' : IterM (α := α) m β}
+    (h : it₁.IsPlausibleStep (.skip it₁')) :
+    (it₁.flatMapAfter f none).IsPlausibleStep (.skip (it₁'.flatMapAfter f none)) :=
+  .outerSkip (.skip h)
+
+public theorem Flatten.IsPlausibleStep.outerDone_flatMap {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β}
+    (h : it₁.IsPlausibleStep .done) :
+    (it₁.flatMapAfter f none).IsPlausibleStep .done :=
+  .outerDone (.done h)
+
+public theorem Flatten.IsPlausibleStep.innerYield_flatMap {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} {it₂ it₂' b}
+    (h : it₂.IsPlausibleStep (.yield it₂' b)) :
+    (it₁.flatMapAfter f (some it₂)).IsPlausibleStep (.yield (it₁.flatMapAfter f (some it₂')) b) :=
+  .innerYield h
+
+public theorem Flatten.IsPlausibleStep.innerSkip_flatMap {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} {it₂ it₂'}
+    (h : it₂.IsPlausibleStep (.skip it₂')) :
+    (it₁.flatMapAfter f (some it₂)).IsPlausibleStep (.skip (it₁.flatMapAfter f (some it₂'))) :=
+  .innerSkip h
+
+public theorem Flatten.IsPlausibleStep.innerDone_flatMap {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} {it₂}
+    (h : it₂.IsPlausibleStep .done) :
+    (it₁.flatMapAfter f (some it₂)).IsPlausibleStep (.skip (it₁.flatMapAfter f none)) :=
+  .innerDone h
+
+public theorem IterM.step_flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
+  (it₁.flatMapAfterM f it₂).step = (do
+    match it₂ with
+    | none =>
+      match (← it₁.step).inflate with
+      | .yield it₁' b h =>
+        return .deflate (.skip (it₁'.flatMapAfterM f (some (← f b))) (.outerYield_flatMapM h))
+      | .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfterM f none) (.outerSkip_flatMapM h))
+      | .done h => return .deflate (.done (.outerDone_flatMapM h))
+    | some it₂ =>
+      match (← it₂.step).inflate with
+      | .yield it₂' out h => return .deflate (.yield (it₁.flatMapAfterM f (some it₂')) out (.innerYield_flatMapM h))
+      | .skip it₂' h => return .deflate (.skip (it₁.flatMapAfterM f (some it₂')) (.innerSkip_flatMapM h))
+      | .done h => return .deflate (.skip (it₁.flatMapAfterM f none) (.innerDone_flatMapM h))) := by
+  simp only [flatMapAfterM, step_flattenAfter, IterM.step_mapM]
+  split
+  · simp only [bind_assoc]
+    apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn <;> simp
+  · rfl
+
+public theorem IterM.step_flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → m (IterM (α := α₂) m γ)} {it₁ : IterM (α := α) m β} :
+  (it₁.flatMapM f).step = (do
+    match (← it₁.step).inflate with
+    | .yield it₁' b h =>
+      return .deflate (.skip (it₁'.flatMapAfterM f (some (← f b)))
+        (.outerYield_flatMapM h))
+    | .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfterM f none) (.outerSkip_flatMapM h))
+    | .done h => return .deflate (.done (.outerDone_flatMapM h))) := by
+  simp [flatMapM, step_flatMapAfterM]
+
+public theorem IterM.step_flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
+  (it₁.flatMapAfter f it₂).step = (do
+    match it₂ with
+    | none =>
+      match (← it₁.step).inflate with
+      | .yield it₁' b h =>
+        return .deflate (.skip (it₁'.flatMapAfter f (some (f b))) (.outerYield_flatMap h))
+      | .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfter f none) (.outerSkip_flatMap h))
+      | .done h => return .deflate (.done (.outerDone_flatMap h))
+    | some it₂ =>
+      match (← it₂.step).inflate with
+      | .yield it₂' out h => return .deflate (.yield (it₁.flatMapAfter f (some it₂')) out (.innerYield_flatMap h))
+      | .skip it₂' h => return .deflate (.skip (it₁.flatMapAfter f (some it₂')) (.innerSkip_flatMap h))
+      | .done h => return .deflate (.skip (it₁.flatMapAfter f none) (.innerDone_flatMap h))) := by
+  simp only [flatMapAfter, step_flattenAfter, IterM.step_map]
+  split
+  · simp only [bind_assoc]
+    apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn <;> simp
+  · rfl
+
+public theorem IterM.step_flatMap {α : Type w} {β : Type w} {α₂ : Type w}
+    {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
+    {f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} :
+  (it₁.flatMap f).step = (do
+    match (← it₁.step).inflate with
+    | .yield it₁' b h =>
+      return .deflate (.skip (it₁'.flatMapAfter f (some (f b))) (.outerYield_flatMap h))
+    | .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfter f none) (.outerSkip_flatMap h))
+    | .done h => return .deflate (.done (.outerDone_flatMap h))) := by
+  simp [flatMap, step_flatMapAfter]
+
+theorem IterM.toList_flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] [Finite α m] [Finite α₂ m]
+    [IteratorCollect α m m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m]
+    {it₁ : IterM (α := α) m (IterM (α := α₂) m β)} {it₂ : Option (IterM (α := α₂) m β)} :
+    (it₁.flattenAfter it₂).toList = do
+      match it₂ with
+      | none => List.flatten <$> (it₁.mapM fun it₂ => it₂.toList).toList
+      | some it₂ => return (← it₂.toList) ++ (← List.flatten <$> (it₁.mapM fun it₂ => it₂.toList).toList) := by
+  induction it₁ using IterM.inductSteps generalizing it₂ with | step it₁ ihy₁ ihs₁ =>
+  have hn : (it₁.flattenAfter none).toList =
+      List.flatten <$> (it₁.mapM fun it₂ => it₂.toList).toList := by
+    rw [toList_eq_match_step, toList_eq_match_step, step_flattenAfter, step_mapM]
+    simp only [bind_assoc, map_eq_pure_bind]
+    apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn
+    · simp [ihy₁ ‹_›]
+    · simp [ihs₁ ‹_›]
+    · simp
+  cases it₂
+  · exact hn
+  · rename_i ih₂
+    induction ih₂ using IterM.inductSteps with | step it₂ ihy₂ ihs₂ =>
+    rw [toList_eq_match_step, step_flattenAfter, bind_assoc]
+    simp only
+    rw [toList_eq_match_step, bind_assoc]
+    apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn
+    · simp [ihy₂ ‹_›]
+    · simp [ihs₂ ‹_›]
+    · simp [hn]
+
+theorem IterM.toArray_flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] [Finite α m] [Finite α₂ m]
+    [IteratorCollect α m m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m]
+    {it₁ : IterM (α := α) m (IterM (α := α₂) m β)} {it₂ : Option (IterM (α := α₂) m β)} :
+    (it₁.flattenAfter it₂).toArray = do
+      match it₂ with
+      | none => Array.flatten <$> (it₁.mapM fun it₂ => it₂.toArray).toArray
+      | some it₂ => return (← it₂.toArray) ++ (← Array.flatten <$> (it₁.mapM fun it₂ => it₂.toArray).toArray) := by
+  induction it₁ using IterM.inductSteps generalizing it₂ with | step it₁ ihy₁ ihs₁ =>
+  have hn : (it₁.flattenAfter none).toArray =
+      Array.flatten <$> (it₁.mapM fun it₂ => it₂.toArray).toArray := by
+    rw [toArray_eq_match_step, toArray_eq_match_step, step_flattenAfter, step_mapM]
+    simp only [bind_assoc, map_eq_pure_bind]
+    apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn
+    · simp [ihy₁ ‹_›]
+    · simp [ihs₁ ‹_›]
+    · simp
+  cases it₂
+  · exact hn
+  · rename_i ih₂
+    induction ih₂ using IterM.inductSteps with | step it₂ ihy₂ ihs₂ =>
+    rw [toArray_eq_match_step, step_flattenAfter, bind_assoc]
+    simp only
+    rw [toArray_eq_match_step, bind_assoc]
+    apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn
+    · simp [ihy₂ ‹_›]
+    · simp [ihs₂ ‹_›]
+    · simp [hn]
+
+public theorem IterM.toList_flatMapAfterM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m]
+    [IteratorCollect α m m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m]
+    {f : β → m (IterM (α := α₂) m γ)}
+    {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
+    (it₁.flatMapAfterM f it₂).toList = do
+      match it₂ with
+      | none => List.flatten <$> (it₁.mapM fun b => do (← f b).toList).toList
+      | some it₂ => return (← it₂.toList) ++
+          (← List.flatten <$> (it₁.mapM fun b => do (← f b).toList).toList) := by
+  simp [flatMapAfterM, toList_flattenAfter]; rfl
+
+public theorem IterM.toArray_flatMapAfterM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m]
+    [IteratorCollect α m m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m]
+    {f : β → m (IterM (α := α₂) m γ)}
+    {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
+    (it₁.flatMapAfterM f it₂).toArray = do
+      match it₂ with
+      | none => Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray
+      | some it₂ => return (← it₂.toArray) ++
+          (← Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray) := by
+  simp [flatMapAfterM, toArray_flattenAfter]; rfl
+
+public theorem IterM.toList_flatMapM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m]
+    [IteratorCollect α m m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m]
+    {f : β → m (IterM (α := α₂) m γ)}
+    {it₁ : IterM (α := α) m β} :
+    (it₁.flatMapM f).toList = List.flatten <$> (it₁.mapM fun b => do (← f b).toList).toList := by
+  simp [flatMapM, toList_flatMapAfterM]
+
+public theorem IterM.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m]
+    [IteratorCollect α m m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m]
+    {f : β → m (IterM (α := α₂) m γ)}
+    {it₁ : IterM (α := α) m β} :
+    (it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by
+  simp [flatMapM, toArray_flatMapAfterM]
+
+public theorem IterM.toList_flatMapAfter {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m]
+    [IteratorCollect α m m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m]
+    {f : β → IterM (α := α₂) m γ}
+    {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
+    (it₁.flatMapAfter f it₂).toList = do
+      match it₂ with
+      | none => List.flatten <$> (it₁.mapM fun b => (f b).toList).toList
+      | some it₂ => return (← it₂.toList) ++
+          (← List.flatten <$> (it₁.mapM fun b => (f b).toList).toList) := by
+  simp [flatMapAfter, toList_flattenAfter]; rfl
+
+public theorem IterM.toArray_flatMapAfter {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m]
+    [IteratorCollect α m m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m]
+    {f : β → IterM (α := α₂) m γ}
+    {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
+    (it₁.flatMapAfter f it₂).toArray = do
+      match it₂ with
+      | none => Array.flatten <$> (it₁.mapM fun b => (f b).toArray).toArray
+      | some it₂ => return (← it₂.toArray) ++
+          (← Array.flatten <$> (it₁.mapM fun b => (f b).toArray).toArray) := by
+  simp [flatMapAfter, toArray_flattenAfter]; rfl
+
+public theorem IterM.toList_flatMap {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m]
+    [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m]
+    [IteratorCollect α m m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m]
+    {f : β → IterM (α := α₂) m γ}
+    {it₁ : IterM (α := α) m β} :
+    (it₁.flatMap f).toList = List.flatten <$> (it₁.mapM fun b => (f b).toList).toList := by
+  simp [flatMap, toList_flatMapAfter]
+
+public theorem IterM.toArray_flatMap {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
+    [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m]
+    [Iterator α m β] [Iterator α₂ m γ] [Finite α m] [Finite α₂ m]
+    [IteratorCollect α m m] [IteratorCollect α₂ m m]
+    [LawfulIteratorCollect α m m] [LawfulIteratorCollect α₂ m m]
+    {f : β → IterM (α := α₂) m γ}
+    {it₁ : IterM (α := α) m β} :
+    (it₁.flatMap f).toArray = Array.flatten <$> (it₁.mapM fun b => (f b).toArray).toArray := by
+  simp [flatMap, toArray_flatMapAfter]
+
+end Std.Iterators
diff --git a/src/Init/Data/Iterators/PostconditionMonad.lean b/src/Init/Data/Iterators/PostconditionMonad.lean
index 9663222164..861b618d80 100644
--- a/src/Init/Data/Iterators/PostconditionMonad.lean
+++ b/src/Init/Data/Iterators/PostconditionMonad.lean
@@ -9,6 +9,7 @@ prelude
 public import Init.Control.Lawful.Basic
 public import Init.Data.Subtype.Basic
 public import Init.PropLemmas
+public import Init.Control.Lawful.MonadLift.Basic
 
 public section
 
@@ -82,7 +83,7 @@ protected def PostconditionT.map {m : Type w → Type w'} [Functor m] {α : Type
 Given a function `α → PostconditionT m β`, returns a a function
 `PostconditionT m α → PostconditionT m β`, turning `PostconditionT m` into a monad.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 protected def PostconditionT.bind {m : Type w → Type w'} [Monad m] {α : Type w} {β : Type w}
     (x : PostconditionT m α) (f : α → PostconditionT m β) : PostconditionT m β :=
   ⟨fun b => ∃ a, x.Property a ∧ (f a).Property b,
@@ -222,6 +223,21 @@ theorem PostconditionT.operation_map {m : Type w → Type w'} [Functor m] {α :
       (fun a => ⟨_, (property_map (m := m)).mpr ⟨a.1, rfl, a.2⟩⟩) <$> x.operation := by
   rfl
 
+@[simp]
+theorem PostconditionT.operation_bind {m : Type w → Type w'} [Monad m] {α : Type w} {β : Type w}
+    {x : PostconditionT m α} {f : α → PostconditionT m β} :
+    (x.bind f).operation = (do
+      let a ← x.operation
+      (fun fa => ⟨fa.1, by exact⟨a.1, a.2, fa.2⟩⟩) <$> (f a.1).operation) := by
+  rfl
+
+theorem PostconditionT.operation_bind' {m : Type w → Type w'} [Monad m] {α : Type w} {β : Type w}
+    {x : PostconditionT m α} {f : α → PostconditionT m β} :
+    (x >>= f).operation = (do
+      let a ← x.operation
+      (fun fa => ⟨fa.1, by exact⟨a.1, a.2, fa.2⟩⟩) <$> (f a.1).operation) := by
+  rfl
+
 @[simp]
 theorem PostconditionT.property_lift {m : Type w → Type w'} [Functor m] {α : Type w}
     {x : m α} : (lift x : PostconditionT m α).Property = (fun _ => True) := by
@@ -233,4 +249,19 @@ theorem PostconditionT.operation_lift {m : Type w → Type w'} [Functor m] {α :
       (⟨·, property_lift (m := m) ▸ True.intro⟩) <$> x := by
   rfl
 
+instance {m : Type w → Type w'} {n : Type w → Type w''} [MonadLift m n] :
+    MonadLift (PostconditionT m) (PostconditionT n) where
+  monadLift x := ⟨_, monadLift x.operation⟩
+
+instance PostconditionT.instLawfulMonadLift {m : Type w → Type w'} {n : Type w → Type w''}
+    [MonadLift m n] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLift m n] :
+    LawfulMonadLift (PostconditionT m) (PostconditionT n) where
+  monadLift_pure a := by
+    simp [MonadLift.monadLift, monadLift, LawfulMonadLift.monadLift_pure, pure,
+      PostconditionT.pure]
+  monadLift_bind x f := by
+    simp only [MonadLift.monadLift, bind, monadLift, LawfulMonadLift.monadLift_bind,
+      PostconditionT.bind, mk.injEq, heq_eq_eq, true_and]
+    simp only [map_eq_pure_bind, LawfulMonadLift.monadLift_bind, LawfulMonadLift.monadLift_pure]
+
 end Std.Iterators