From 32972da7fefa55b8565b49cb3a40eb585ec33966 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 19 May 2025 11:44:52 +0200
Subject: [PATCH 1/5] wip

---
 src/Std/Data/Iterators/Consumers/Loop.lean    |  12 +-
 .../Iterators/Consumers/Monadic/Loop.lean     |  34 +--
 .../Data/Iterators/Lemmas/Consumers/Loop.lean | 174 +++++++++++++++
 .../Lemmas/Consumers/Monadic/Loop.lean        | 210 ++++++++++++++++++
 4 files changed, 409 insertions(+), 21 deletions(-)
 create mode 100644 src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
 create mode 100644 src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean

diff --git a/src/Std/Data/Iterators/Consumers/Loop.lean b/src/Std/Data/Iterators/Consumers/Loop.lean
index c7a0bd292798..4250bbfe2674 100644
--- a/src/Std/Data/Iterators/Consumers/Loop.lean
+++ b/src/Std/Data/Iterators/Consumers/Loop.lean
@@ -47,10 +47,10 @@ number of steps. If the iterator is not finite or such an instance is not availa
 verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
-def Iter.foldM {n : Type w → Type w} [Monad n]
+def Iter.foldM {m : Type w → Type w'} [Monad m]
     {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β] [Finite α Id]
-    [IteratorLoop α Id n] (f : γ → β → n γ)
-    (init : γ) (it : Iter (α := α) β) : n γ :=
+    [IteratorLoop α Id m] (f : γ → β → m γ)
+    (init : γ) (it : Iter (α := α) β) : m γ :=
   ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
 
 /--
@@ -63,10 +63,10 @@ This is a partial, potentially nonterminating, function. It is not possible to f
 its behavior. If the iterator has a `Finite` instance, consider using `IterM.foldM` instead.
 -/
 @[always_inline, inline]
-def Iter.Partial.foldM {n : Type w → Type w} [Monad n]
+def Iter.Partial.foldM {m : Type w → Type w'} [Monad m]
     {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
-    [IteratorLoopPartial α Id n] (f : γ → β → n γ)
-    (init : γ) (it : Iter.Partial (α := α) β) : n γ :=
+    [IteratorLoopPartial α Id m] (f : γ → β → m γ)
+    (init : γ) (it : Iter.Partial (α := α) β) : m γ :=
   ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
 
 /--
diff --git a/src/Std/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Std/Data/Iterators/Consumers/Monadic/Loop.lean
index 4eadc20bc0f2..2b8ce5775939 100644
--- a/src/Std/Data/Iterators/Consumers/Monadic/Loop.lean
+++ b/src/Std/Data/Iterators/Consumers/Monadic/Loop.lean
@@ -170,8 +170,8 @@ It simply iterates through the iterator using `IterM.step`. For certain iterator
 implementations are possible and should be used instead.
 -/
 @[always_inline, inline]
-def IteratorLoopPartial.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type w → Type w'}
-    [Monad m] [Monad n] [Iterator α m β] :
+def IteratorLoopPartial.defaultImplementation {α : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoopPartial α m n where
   forInPartial lift := IterM.DefaultConsumers.forInPartial lift _
 
@@ -182,6 +182,19 @@ instance (α : Type w) (m : Type w → Type w') (n : Type w → Type w')
   letI : IteratorLoop α m n := .defaultImplementation
   ⟨rfl⟩
 
+theorem IteratorLoop.wellFounded_of_finite {m : Type w → Type w'}
+    {α β γ : Type w} [Iterator α m β] [Finite α m] :
+    WellFounded α m (γ := γ) fun _ _ _ => True := by
+  apply Subrelation.wf
+    (r := InvImage IterM.TerminationMeasures.Finite.Rel (fun p => p.1.finitelyManySteps))
+  · intro p' p h
+    apply Relation.TransGen.single
+    obtain ⟨b, h, _⟩ | ⟨h, _⟩ := h
+    · exact ⟨.yield p'.fst b, rfl, h⟩
+    · exact ⟨.skip p'.fst, rfl, h⟩
+  · apply InvImage.wf
+    exact WellFoundedRelation.wf
+
 /--
 This `ForIn`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
 -/
@@ -192,16 +205,7 @@ def IteratorLoop.finiteForIn {m : Type w → Type w'} {n : Type w → Type w''}
     ForIn n (IterM (α := α) m β) β where
   forIn {γ} [Monad n] it init f :=
     IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
-      (by
-        apply Subrelation.wf
-          (r := InvImage IterM.TerminationMeasures.Finite.Rel (fun p => p.1.finitelyManySteps))
-        · intro p' p h
-          apply Relation.TransGen.single
-          obtain ⟨b, h, _⟩ | ⟨h, _⟩ := h
-          · exact ⟨.yield p'.fst b, rfl, h⟩
-          · exact ⟨.skip p'.fst, rfl, h⟩
-        · apply InvImage.wf
-          exact WellFoundedRelation.wf)
+      wellFounded_of_finite
       it init ((⟨·, .intro⟩) <$> f · ·)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
@@ -227,7 +231,7 @@ number of steps. If the iterator is not finite or such an instance is not availa
 verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
-def IterM.foldM {m : Type w → Type w'} {n : Type w → Type w'} [Monad n]
+def IterM.foldM {m : Type w → Type w'} {n : Type w → Type w''} [Monad n]
     {α : Type w} {β : Type w} {γ : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
     [MonadLiftT m n]
     (f : γ → β → n γ) (init : γ) (it : IterM (α := α) m β) : n γ :=
@@ -295,7 +299,7 @@ verify the behavior of the partial variant.
 def IterM.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
     [Iterator α m β] [Finite α m] (it : IterM (α := α) m β) [IteratorLoop α m m] :
     m PUnit :=
-  it.foldM (γ := PUnit) (fun _ _ => pure .unit) .unit
+  it.fold (γ := PUnit) (fun _ _ => .unit) .unit
 
 /--
 Iterates over the whole iterator, applying the monadic effects of each step, discarding all
@@ -308,6 +312,6 @@ its behavior. If the iterator has a `Finite` instance, consider using `IterM.dra
 def IterM.Partial.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
     [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorLoopPartial α m m] :
     m PUnit :=
-  it.foldM (γ := PUnit) (fun _ _ => pure .unit) .unit
+  it.fold (γ := PUnit) (fun _ _ => .unit) .unit
 
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
new file mode 100644
index 000000000000..46d3db1c1e96
--- /dev/null
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Init.Data.List.Control
+import Std.Data.Iterators.Lemmas.Basic
+import Std.Data.Iterators.Lemmas.Consumers.Collect
+import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+import Std.Data.Iterators.Consumers.Collect
+import Std.Data.Iterators.Consumers.Loop
+
+namespace Std.Iterators
+
+theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
+    {m : Type w → Type w''} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
+    {f : β → γ → m (ForInStep γ)} :
+    ForIn.forIn it init f =
+      IterM.DefaultConsumers.forIn (fun _ c => pure c.run) γ (fun _ _ _ => True)
+        IteratorLoop.wellFounded_of_finite it.toIterM init ((⟨·, .intro⟩) <$> f · ·) := by
+  cases hl.lawful; rfl
+
+theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
+    {f : β → γ → m (ForInStep γ)} :
+    ForIn.forIn it init f = letI : MonadLift Id m := ⟨pure⟩; ForIn.forIn it.toIterM init f := by
+  rfl
+
+theorem Iter.forIn_of_step {α β : Type w} [Iterator α Id β]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
+    {f : β → γ → m (ForInStep γ)} :
+    ForIn.forIn it init f = (do
+      match it.step with
+      | .yield it' out _ =>
+        match ← f out init with
+        | .yield c => ForIn.forIn it' c f
+        | .done c => return c
+      | .skip it' _ => ForIn.forIn it' init f
+      | .done _ => return init) := by
+  rw [Iter.forIn_eq_forIn_toIterM, @IterM.forIn_of_step, Iter.step]
+  simp only [liftM, monadLift, pure_bind]
+  generalize it.toIterM.step = step
+  cases step.casesHelper
+  · apply bind_congr
+    intro forInStep
+    rfl
+  · rfl
+  · rfl
+
+-- TODO: nonterminal simps
+theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id] [LawfulIteratorCollect α Id]
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
+    {f : β → γ → m (ForInStep γ)} :
+    ForIn.forIn it.toList init f = ForIn.forIn it init f := by
+  rw [List.forIn_eq_foldlM]
+  revert init
+  induction it using Iter.induct with case step it ihy ihs =>
+  intro init
+  rw [forIn_of_step, Iter.toList_of_step]
+  simp only [map_eq_pure_bind]
+  generalize it.step = step
+  cases step.casesHelper
+  · rename_i it' out h
+    simp only [List.foldlM_cons, bind_pure_comp, map_bind]
+    apply bind_congr
+    intro forInStep
+    cases forInStep
+    · simp
+      induction it'.toList <;> simp [*]
+    · simp
+      simp only [ForIn.forIn, forIn', List.forIn'] at ihy
+      rw [ihy h, forIn_eq_forIn_toIterM]
+  · simp
+    rw [ihs]
+    assumption
+  · simp
+
+theorem Iter.foldM_eq_forIn {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'}
+    [Monad m] [IteratorLoop α Id m] {f : γ → β → m γ}
+    {init : γ} {it : Iter (α := α) β} :
+    it.foldM (init := init) f = ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x) :=
+  rfl
+
+theorem Iter.forIn_yield_eq_foldM {α β γ δ : Type w} [Iterator α Id β]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
+    [LawfulIteratorLoop α Id m] {f : β → γ → m δ} {g : β → γ → δ → γ} {init : γ}
+    {it : Iter (α := α) β} :
+    ForIn.forIn it init (fun c b => (fun d => .yield (g c b d)) <$> f c b) =
+      it.foldM (fun b c => g c b <$> f c b) init := by
+  simp [Iter.foldM_eq_forIn]
+
+theorem Iter.foldM_of_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
+    {m : Type w → Type w'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
+    [LawfulIteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Iter (α := α) β} :
+    it.foldM (init := init) f = (do
+      match it.step with
+      | .yield it' out _ => it'.foldM (init := ← f init out) f
+      | .skip it' _ => it'.foldM (init := init) f
+      | .done _ => return init) := by
+  rw [Iter.foldM_eq_forIn, Iter.forIn_of_step]
+  generalize it.step = step
+  cases step.casesHelper <;> simp [foldM_eq_forIn]
+
+theorem Iter.foldlM_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'}
+    [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id] [LawfulIteratorCollect α Id]
+    {f : γ → β → m γ}
+    {init : γ} {it : Iter (α := α) β} :
+    it.toList.foldlM (init := init) f = it.foldM (init := init) f := by
+  rw [Iter.foldM_eq_forIn, ← Iter.forIn_toList]
+  simp only [List.forIn_yield_eq_foldlM, id_map']
+
+-- TODO: nonterminal simp
+theorem IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id] [LawfulIteratorCollect α Id]
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
+    {f : β → γ → m (ForInStep γ)} :
+    forIn it init f = ForInStep.value <$>
+      it.foldM (fun c b => match c with
+        | .yield c => f b c
+        | .done c => pure (.done c)) (ForInStep.yield init) := by
+  simp [← Iter.forIn_toList, ← Iter.foldlM_toList, List.forIn_eq_foldlM]; rfl
+
+theorem Iter.fold_eq_forIn {α β γ : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
+    it.fold (init := init) f =
+      ForIn.forIn (m := Id) it init (fun x acc => pure (ForInStep.yield (f acc x))) := by
+  rfl
+
+theorem Iter.fold_eq_foldM {α β γ : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ}
+    {it : Iter (α := α) β} :
+    it.fold (init := init) f = it.foldM (m := Id) (init := init) (pure <| f · ·) := by
+  simp [foldM_eq_forIn, fold_eq_forIn]
+
+theorem Iter.forIn_yield_eq_fold {α β γ : Type w} [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id] {f : β → γ → γ} {init : γ}
+    {it : Iter (α := α) β} :
+    ForIn.forIn (m := Id) it init (fun c b => .yield (f c b)) =
+      it.fold (fun b c => f c b) init := by
+  simp [Iter.fold_eq_forIn]
+
+theorem Iter.fold_of_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
+    it.fold (init := init) f = (match it.step with
+      | .yield it' out _ => it'.fold (init := f init out) f
+      | .skip it' _ => it'.fold (init := init) f
+      | .done _ => init) := by
+  rw [fold_eq_foldM, foldM_of_step]
+  simp only [fold_eq_foldM]
+  generalize it.step = step
+  cases step.casesHelper <;> simp
+
+theorem Iter.foldl_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id]
+    [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorCollect α Id] [LawfulIteratorCollect α Id]
+    {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
+    it.toList.foldl (init := init) f = it.fold (init := init) f := by
+  simp [Iter.fold_eq_foldM, ← Iter.foldlM_toList, List.foldl_eq_foldlM]
+
+end Std.Iterators
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
new file mode 100644
index 000000000000..2f537a96f79a
--- /dev/null
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
@@ -0,0 +1,210 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+prelude
+import Init.Control.Lawful.Basic
+import Std.Data.Iterators.Consumers.Monadic.Collect
+import Std.Data.Iterators.Consumers.Monadic.Loop
+import Std.Data.Iterators.Lemmas.Monadic.Basic
+import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+
+namespace Std.Iterators
+
+theorem IterM.DefaultConsumers.forIn_of_step {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β]
+    {n : Type w → Type w''} [Monad n]
+    {lift : ∀ γ, m γ → n γ} {γ : Type w}
+    {plausible_forInStep : β → γ → ForInStep γ → Prop}
+    {wf : IteratorLoop.WellFounded α m plausible_forInStep}
+    {it : IterM (α := α) m β} {init : γ}
+    {f : (b : β) → (c : γ) → n (Subtype (plausible_forInStep b c))} :
+    IterM.DefaultConsumers.forIn lift γ plausible_forInStep wf it init f = (do
+      match ← lift _ it.step with
+      | .yield it' out _ =>
+        match ← f out init with
+        | ⟨.yield c, _⟩ => IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' c f
+        | ⟨.done c, _⟩ => return c
+      | .skip it' _ => IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' init f
+      | .done _ => return init) := by
+  rw [forIn]
+  apply bind_congr
+  intro step
+  cases step.casesHelper <;> rfl
+
+theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+    {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n]
+    [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
+    {f : β → γ → n (ForInStep γ)} :
+    ForIn.forIn it init f = IterM.DefaultConsumers.forIn (fun _ => monadLift) γ (fun _ _ _ => True)
+        IteratorLoop.wellFounded_of_finite it init ((⟨·, .intro⟩) <$> f · ·) := by
+  cases hl.lawful; rfl
+
+theorem IterM.forIn_of_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
+    {f : β → γ → n (ForInStep γ)} :
+    ForIn.forIn it init f = (do
+      match ← it.step with
+      | .yield it' out _ =>
+        match ← f out init with
+        | .yield c => ForIn.forIn it' c f
+        | .done c => return c
+      | .skip it' _ => ForIn.forIn it' init f
+      | .done _ => return init) := by
+  rw [IterM.forIn_eq, DefaultConsumers.forIn_of_step]
+  apply bind_congr
+  intro step
+  cases step.casesHelper
+  · simp only [map_eq_pure_bind, bind_assoc]
+    apply bind_congr
+    intro forInStep
+    cases forInStep <;> simp [IterM.forIn_eq]
+  · simp [IterM.forIn_eq]
+  · simp
+
+theorem IterM.foldM_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+    {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [MonadLiftT m n] {f : γ → β → n γ}
+    {init : γ} {it : IterM (α := α) m β} :
+    it.foldM (init := init) f = ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x) :=
+  rfl
+
+theorem IterM.forIn_yield_eq_foldM {α β γ δ : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n]
+    [LawfulIteratorLoop α m n] [MonadLiftT m n] {f : β → γ → n δ} {g : β → γ → δ → γ} {init : γ}
+    {it : IterM (α := α) m β} :
+    ForIn.forIn it init (fun c b => (fun d => .yield (g c b d)) <$> f c b) =
+      it.foldM (fun b c => g c b <$> f c b) init := by
+  simp [IterM.foldM_eq_forIn]
+
+theorem IterM.foldM_of_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+    {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    [MonadLiftT m n] {f : γ → β → n γ} {init : γ} {it : IterM (α := α) m β} :
+    it.foldM (init := init) f = (do
+      match ← it.step with
+      | .yield it' out _ => it'.foldM (init := ← f init out) f
+      | .skip it' _ => it'.foldM (init := init) f
+      | .done _ => return init) := by
+  rw [IterM.foldM_eq_forIn, IterM.forIn_of_step]
+  apply bind_congr
+  intro step
+  cases step.casesHelper <;> simp [foldM_eq_forIn]
+
+theorem IterM.fold_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m]
+    [IteratorLoop α m m] {f : γ → β → γ} {init : γ} {it : IterM (α := α) m β} :
+    it.fold (init := init) f =
+      ForIn.forIn (m := m) it init (fun x acc => pure (ForInStep.yield (f acc x))) := by
+  rfl
+
+theorem IterM.fold_eq_foldM {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] {f : γ → β → γ} {init : γ}
+    {it : IterM (α := α) m β} :
+    it.fold (init := init) f = it.foldM (init := init) (pure <| f · ·) := by
+  simp [foldM_eq_forIn, fold_eq_forIn]
+
+theorem IterM.forIn_pure_yield_eq_fold {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m]
+    [LawfulIteratorLoop α m m] {f : β → γ → γ} {init : γ}
+    {it : IterM (α := α) m β} :
+    ForIn.forIn it init (fun c b => pure (.yield (f c b))) =
+      it.fold (fun b c => f c b) init := by
+  simp [IterM.fold_eq_forIn]
+
+theorem IterM.fold_of_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {f : γ → β → γ} {init : γ} {it : IterM (α := α) m β} :
+    it.fold (init := init) f = (do
+      match ← it.step with
+      | .yield it' out _ => it'.fold (init := f init out) f
+      | .skip it' _ => it'.fold (init := init) f
+      | .done _ => return init) := by
+  rw [fold_eq_foldM, foldM_of_step]
+  simp only [fold_eq_foldM]
+  apply bind_congr
+  intro step
+  cases step.casesHelper <;> simp
+
+theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    [IteratorCollect α m] [LawfulIteratorCollect α m]
+    {it : IterM (α := α) m β} :
+    it.toList = it.fold (init := []) (fun l out => l ++ [out]) := by
+  suffices h : ∀ l' : List β, (l' ++ ·) <$> it.toList =
+      it.fold (init := l') (fun l out => l ++ [out]) by
+    specialize h []
+    simpa using h
+  induction it using IterM.induct with | step it ihy ihs =>
+  intro l'
+  rw [IterM.toList_of_step, IterM.fold_of_step]
+  simp only [map_eq_pure_bind, bind_assoc]
+  apply bind_congr
+  intro step
+  cases step.casesHelper
+  · rename_i it' out h
+    specialize ihy h (l' ++ [out])
+    simpa using ihy
+  · rename_i it' h
+    simp [ihs h]
+  · simp
+
+theorem IterM.drain_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+    [Monad m] [IteratorLoop α m m] {it : IterM (α := α) m β} :
+    it.drain = it.fold (init := PUnit.unit) (fun _ _ => .unit) :=
+  rfl
+
+theorem IterM.drain_eq_foldM {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m] [IteratorLoop α m m] {it : IterM (α := α) m β} :
+    it.drain = it.foldM (init := PUnit.unit) (fun _ _ => pure .unit) := by
+  simp [IterM.drain_eq_fold, IterM.fold_eq_foldM]
+
+theorem IterM.drain_eq_forIn {α β : Type w} {m : Type w → Type w'}  [Iterator α m β] [Finite α m]
+    [Monad m] [IteratorLoop α m m] {it : IterM (α := α) m β} :
+    it.drain = ForIn.forIn (m := m) it PUnit.unit (fun _ _ => pure (ForInStep.yield .unit)) := by
+  simp [IterM.drain_eq_fold, IterM.fold_eq_forIn]
+
+theorem IterM.drain_of_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+    [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} :
+    it.drain = (do
+      match ← it.step with
+      | .yield it' _ _ => it'.drain
+      | .skip it' _ => it'.drain
+      | .done _ => return .unit) := by
+  rw [IterM.drain_eq_fold, IterM.fold_of_step]
+  simp [IterM.drain_eq_fold]
+
+theorem IterM.drain_eq_map_toList {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    [IteratorCollect α m] [LawfulIteratorCollect α m]
+    {it : IterM (α := α) m β} :
+    it.drain = (fun _ => .unit) <$> it.toList := by
+  induction it using IterM.induct with | step it ihy ihs =>
+  rw [IterM.drain_of_step, IterM.toList_of_step]
+  simp only [map_eq_pure_bind, bind_assoc]
+  apply bind_congr
+  intro step
+  cases step.casesHelper
+  · rename_i it' out h
+    simp [ihy h]
+  · rename_i it' h
+    simp [ihs h]
+  · simp
+
+theorem IterM.drain_eq_map_toListRev {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    [IteratorCollect α m] [LawfulIteratorCollect α m]
+    {it : IterM (α := α) m β} :
+    it.drain = (fun _ => .unit) <$> it.toListRev := by
+  simp [IterM.drain_eq_map_toList, IterM.toListRev_eq]
+
+theorem IterM.drain_eq_map_toArray {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    [IteratorCollect α m] [LawfulIteratorCollect α m]
+    {it : IterM (α := α) m β} :
+    it.drain = (fun _ => .unit) <$> it.toList := by
+  simp [IterM.drain_eq_map_toList]
+
+end Std.Iterators

From 8e991a91a124a2d97d976527595ed1502f51bbd1 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 19 May 2025 14:20:08 +0200
Subject: [PATCH 2/5] cleanups

---
 .../Data/Iterators/Lemmas/Consumers/Loop.lean  | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
index 46d3db1c1e96..105db99ddfb6 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -53,7 +53,6 @@ theorem Iter.forIn_of_step {α β : Type w} [Iterator α Id β]
   · rfl
   · rfl
 
--- TODO: nonterminal simps
 theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
@@ -74,14 +73,12 @@ theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
     apply bind_congr
     intro forInStep
     cases forInStep
-    · simp
-      induction it'.toList <;> simp [*]
-    · simp
-      simp only [ForIn.forIn, forIn', List.forIn'] at ihy
-      rw [ihy h, forIn_eq_forIn_toIterM]
-  · simp
-    rw [ihs]
-    assumption
+    · induction it'.toList <;> simp [*]
+    · simp only [ForIn.forIn, forIn', List.forIn'] at ihy
+      simp [ihy h, forIn_eq_forIn_toIterM]
+  · rename_i it' h
+    simp only [bind_pure_comp]
+    rw [ihs h]
   · simp
 
 theorem Iter.foldM_eq_forIn {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'}
@@ -119,7 +116,6 @@ theorem Iter.foldlM_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id
   rw [Iter.foldM_eq_forIn, ← Iter.forIn_toList]
   simp only [List.forIn_yield_eq_foldlM, id_map']
 
--- TODO: nonterminal simp
 theorem IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
@@ -130,7 +126,7 @@ theorem IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β]
       it.foldM (fun c b => match c with
         | .yield c => f b c
         | .done c => pure (.done c)) (ForInStep.yield init) := by
-  simp [← Iter.forIn_toList, ← Iter.foldlM_toList, List.forIn_eq_foldlM]; rfl
+  simp only [← Iter.forIn_toList, List.forIn_eq_foldlM, ← Iter.foldlM_toList]; rfl
 
 theorem Iter.fold_eq_forIn {α β γ : Type w} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :

From 7745cfc9fe8ed9dd3335330c47e56b091f45a4fd Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 20 May 2025 14:44:53 +0200
Subject: [PATCH 3/5] fix problems caused by earlier PRs' changes

---
 .../Data/Iterators/Lemmas/Consumers/Loop.lean | 26 ++++++-------
 .../Lemmas/Consumers/Monadic/Loop.lean        | 38 +++++++++----------
 2 files changed, 31 insertions(+), 33 deletions(-)

diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
index 105db99ddfb6..8f2e172acc3f 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -30,7 +30,7 @@ theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     ForIn.forIn it init f = letI : MonadLift Id m := ⟨pure⟩; ForIn.forIn it.toIterM init f := by
   rfl
 
-theorem Iter.forIn_of_step {α β : Type w} [Iterator α Id β]
+theorem Iter.forIn_eq_match_step {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
     [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
     {γ : Type w} {it : Iter (α := α) β} {init : γ}
@@ -43,10 +43,10 @@ theorem Iter.forIn_of_step {α β : Type w} [Iterator α Id β]
         | .done c => return c
       | .skip it' _ => ForIn.forIn it' init f
       | .done _ => return init) := by
-  rw [Iter.forIn_eq_forIn_toIterM, @IterM.forIn_of_step, Iter.step]
+  rw [Iter.forIn_eq_forIn_toIterM, @IterM.forIn_eq_match_step, Iter.step]
   simp only [liftM, monadLift, pure_bind]
   generalize it.toIterM.step = step
-  cases step.casesHelper
+  cases step using PlausibleIterStep.casesOn
   · apply bind_congr
     intro forInStep
     rfl
@@ -61,13 +61,11 @@ theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
     {f : β → γ → m (ForInStep γ)} :
     ForIn.forIn it.toList init f = ForIn.forIn it init f := by
   rw [List.forIn_eq_foldlM]
-  revert init
-  induction it using Iter.induct with case step it ihy ihs =>
-  intro init
-  rw [forIn_of_step, Iter.toList_of_step]
+  induction it using Iter.inductSteps generalizing init with case step it ihy ihs =>
+  rw [forIn_eq_match_step, Iter.toList_eq_match_step]
   simp only [map_eq_pure_bind]
   generalize it.step = step
-  cases step.casesHelper
+  cases step using PlausibleIterStep.casesOn
   · rename_i it' out h
     simp only [List.foldlM_cons, bind_pure_comp, map_bind]
     apply bind_congr
@@ -95,7 +93,7 @@ theorem Iter.forIn_yield_eq_foldM {α β γ δ : Type w} [Iterator α Id β]
       it.foldM (fun b c => g c b <$> f c b) init := by
   simp [Iter.foldM_eq_forIn]
 
-theorem Iter.foldM_of_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
+theorem Iter.foldM_eq_match_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
     {m : Type w → Type w'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
     [LawfulIteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Iter (α := α) β} :
     it.foldM (init := init) f = (do
@@ -103,9 +101,9 @@ theorem Iter.foldM_of_step {α β γ : Type w} [Iterator α Id β] [Finite α Id
       | .yield it' out _ => it'.foldM (init := ← f init out) f
       | .skip it' _ => it'.foldM (init := init) f
       | .done _ => return init) := by
-  rw [Iter.foldM_eq_forIn, Iter.forIn_of_step]
+  rw [Iter.foldM_eq_forIn, Iter.forIn_eq_match_step]
   generalize it.step = step
-  cases step.casesHelper <;> simp [foldM_eq_forIn]
+  cases step using PlausibleIterStep.casesOn <;> simp [foldM_eq_forIn]
 
 theorem Iter.foldlM_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'}
     [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
@@ -148,17 +146,17 @@ theorem Iter.forIn_yield_eq_fold {α β γ : Type w} [Iterator α Id β]
       it.fold (fun b c => f c b) init := by
   simp [Iter.fold_eq_forIn]
 
-theorem Iter.fold_of_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
+theorem Iter.fold_eq_match_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
     it.fold (init := init) f = (match it.step with
       | .yield it' out _ => it'.fold (init := f init out) f
       | .skip it' _ => it'.fold (init := init) f
       | .done _ => init) := by
-  rw [fold_eq_foldM, foldM_of_step]
+  rw [fold_eq_foldM, foldM_eq_match_step]
   simp only [fold_eq_foldM]
   generalize it.step = step
-  cases step.casesHelper <;> simp
+  cases step using PlausibleIterStep.casesOn <;> simp
 
 theorem Iter.foldl_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
index 2f537a96f79a..350c77284ff1 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
@@ -12,7 +12,7 @@ import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 
 namespace Std.Iterators
 
-theorem IterM.DefaultConsumers.forIn_of_step {α β : Type w} {m : Type w → Type w'}
+theorem IterM.DefaultConsumers.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'}
     [Iterator α m β]
     {n : Type w → Type w''} [Monad n]
     {lift : ∀ γ, m γ → n γ} {γ : Type w}
@@ -31,7 +31,7 @@ theorem IterM.DefaultConsumers.forIn_of_step {α β : Type w} {m : Type w → Ty
   rw [forIn]
   apply bind_congr
   intro step
-  cases step.casesHelper <;> rfl
+  cases step using PlausibleIterStep.casesOn <;> rfl
 
 theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n]
@@ -41,7 +41,7 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
         IteratorLoop.wellFounded_of_finite it init ((⟨·, .intro⟩) <$> f · ·) := by
   cases hl.lawful; rfl
 
-theorem IterM.forIn_of_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n]
     [IteratorLoop α m n] [LawfulIteratorLoop α m n]
     [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
@@ -54,10 +54,10 @@ theorem IterM.forIn_of_step {α β : Type w} {m : Type w → Type w'} [Iterator
         | .done c => return c
       | .skip it' _ => ForIn.forIn it' init f
       | .done _ => return init) := by
-  rw [IterM.forIn_eq, DefaultConsumers.forIn_of_step]
+  rw [IterM.forIn_eq, DefaultConsumers.forIn_eq_match_step]
   apply bind_congr
   intro step
-  cases step.casesHelper
+  cases step using PlausibleIterStep.casesOn
   · simp only [map_eq_pure_bind, bind_assoc]
     apply bind_congr
     intro forInStep
@@ -79,7 +79,7 @@ theorem IterM.forIn_yield_eq_foldM {α β γ δ : Type w} {m : Type w → Type w
       it.foldM (fun b c => g c b <$> f c b) init := by
   simp [IterM.foldM_eq_forIn]
 
-theorem IterM.foldM_of_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+theorem IterM.foldM_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n]
     [MonadLiftT m n] {f : γ → β → n γ} {init : γ} {it : IterM (α := α) m β} :
     it.foldM (init := init) f = (do
@@ -87,10 +87,10 @@ theorem IterM.foldM_of_step {α β γ : Type w} {m : Type w → Type w'} [Iterat
       | .yield it' out _ => it'.foldM (init := ← f init out) f
       | .skip it' _ => it'.foldM (init := init) f
       | .done _ => return init) := by
-  rw [IterM.foldM_eq_forIn, IterM.forIn_of_step]
+  rw [IterM.foldM_eq_forIn, IterM.forIn_eq_match_step]
   apply bind_congr
   intro step
-  cases step.casesHelper <;> simp [foldM_eq_forIn]
+  cases step using PlausibleIterStep.casesOn <;> simp [foldM_eq_forIn]
 
 theorem IterM.fold_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m]
@@ -113,7 +113,7 @@ theorem IterM.forIn_pure_yield_eq_fold {α β γ : Type w} {m : Type w → Type
       it.fold (fun b c => f c b) init := by
   simp [IterM.fold_eq_forIn]
 
-theorem IterM.fold_of_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+theorem IterM.fold_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {f : γ → β → γ} {init : γ} {it : IterM (α := α) m β} :
     it.fold (init := init) f = (do
@@ -121,11 +121,11 @@ theorem IterM.fold_of_step {α β γ : Type w} {m : Type w → Type w'} [Iterato
       | .yield it' out _ => it'.fold (init := f init out) f
       | .skip it' _ => it'.fold (init := init) f
       | .done _ => return init) := by
-  rw [fold_eq_foldM, foldM_of_step]
+  rw [fold_eq_foldM, foldM_eq_match_step]
   simp only [fold_eq_foldM]
   apply bind_congr
   intro step
-  cases step.casesHelper <;> simp
+  cases step using PlausibleIterStep.casesOn <;> simp
 
 theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
@@ -136,13 +136,13 @@ theorem IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator
       it.fold (init := l') (fun l out => l ++ [out]) by
     specialize h []
     simpa using h
-  induction it using IterM.induct with | step it ihy ihs =>
+  induction it using IterM.inductSteps with | step it ihy ihs =>
   intro l'
-  rw [IterM.toList_of_step, IterM.fold_of_step]
+  rw [IterM.toList_eq_match_step, IterM.fold_eq_match_step]
   simp only [map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
-  cases step.casesHelper
+  cases step using PlausibleIterStep.casesOn
   · rename_i it' out h
     specialize ihy h (l' ++ [out])
     simpa using ihy
@@ -165,7 +165,7 @@ theorem IterM.drain_eq_forIn {α β : Type w} {m : Type w → Type w'}  [Iterato
     it.drain = ForIn.forIn (m := m) it PUnit.unit (fun _ _ => pure (ForInStep.yield .unit)) := by
   simp [IterM.drain_eq_fold, IterM.fold_eq_forIn]
 
-theorem IterM.drain_of_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+theorem IterM.drain_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} :
     it.drain = (do
@@ -173,7 +173,7 @@ theorem IterM.drain_of_step {α β : Type w} {m : Type w → Type w'} [Iterator
       | .yield it' _ _ => it'.drain
       | .skip it' _ => it'.drain
       | .done _ => return .unit) := by
-  rw [IterM.drain_eq_fold, IterM.fold_of_step]
+  rw [IterM.drain_eq_fold, IterM.fold_eq_match_step]
   simp [IterM.drain_eq_fold]
 
 theorem IterM.drain_eq_map_toList {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
@@ -181,12 +181,12 @@ theorem IterM.drain_eq_map_toList {α β : Type w} {m : Type w → Type w'} [Ite
     [IteratorCollect α m] [LawfulIteratorCollect α m]
     {it : IterM (α := α) m β} :
     it.drain = (fun _ => .unit) <$> it.toList := by
-  induction it using IterM.induct with | step it ihy ihs =>
-  rw [IterM.drain_of_step, IterM.toList_of_step]
+  induction it using IterM.inductSteps with | step it ihy ihs =>
+  rw [IterM.drain_eq_match_step, IterM.toList_eq_match_step]
   simp only [map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
-  cases step.casesHelper
+  cases step using PlausibleIterStep.casesOn
   · rename_i it' out h
     simp [ihy h]
   · rename_i it' h

From 219dc1984cf83e9d3159a5dfd4a5c00c72b8b2b1 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Tue, 20 May 2025 18:15:34 +0200
Subject: [PATCH 4/5] fix pipeline?

---
 src/Std/Data/Iterators/Lemmas/Consumers.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Std/Data/Iterators/Lemmas/Consumers.lean b/src/Std/Data/Iterators/Lemmas/Consumers.lean
index fff07bb39e00..7afe1cd75acf 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers.lean
+++ b/src/Std/Data/Iterators/Lemmas/Consumers.lean
@@ -6,3 +6,4 @@ Authors: Paul Reichert
 prelude
 import Std.Data.Iterators.Lemmas.Consumers.Monadic
 import Std.Data.Iterators.Lemmas.Consumers.Collect
+import Std.Data.Iterators.Lemmas.Consumers.Loop

From 096bf7816107e57a337d1e0f448034a1a9a69a02 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 23 May 2025 16:01:52 +0200
Subject: [PATCH 5/5] fix breakage after rebase

---
 src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
index 8f2e172acc3f..aee100bc88fe 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -129,13 +129,13 @@ theorem IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β]
 theorem Iter.fold_eq_forIn {α β γ : Type w} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
     it.fold (init := init) f =
-      ForIn.forIn (m := Id) it init (fun x acc => pure (ForInStep.yield (f acc x))) := by
+      (ForIn.forIn (m := Id) it init (fun x acc => pure (ForInStep.yield (f acc x)))).run := by
   rfl
 
 theorem Iter.fold_eq_foldM {α β γ : Type w} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ}
     {it : Iter (α := α) β} :
-    it.fold (init := init) f = it.foldM (m := Id) (init := init) (pure <| f · ·) := by
+    it.fold (init := init) f = (it.foldM (m := Id) (init := init) (pure <| f · ·)).run := by
   simp [foldM_eq_forIn, fold_eq_forIn]
 
 theorem Iter.forIn_yield_eq_fold {α β γ : Type w} [Iterator α Id β]
@@ -144,7 +144,8 @@ theorem Iter.forIn_yield_eq_fold {α β γ : Type w} [Iterator α Id β]
     {it : Iter (α := α) β} :
     ForIn.forIn (m := Id) it init (fun c b => .yield (f c b)) =
       it.fold (fun b c => f c b) init := by
-  simp [Iter.fold_eq_forIn]
+  simp only [fold_eq_forIn]
+  rfl
 
 theorem Iter.fold_eq_match_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
@@ -163,6 +164,6 @@ theorem Iter.foldl_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id]
     [IteratorCollect α Id] [LawfulIteratorCollect α Id]
     {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
     it.toList.foldl (init := init) f = it.fold (init := init) f := by
-  simp [Iter.fold_eq_foldM, ← Iter.foldlM_toList, List.foldl_eq_foldlM]
+  rw [fold_eq_foldM, List.foldl_eq_foldlM, ← Iter.foldlM_toList]
 
 end Std.Iterators