From a3be74a90d7e180aae3b53fe8ca9798deb33eb33 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 13 Feb 2026 20:53:58 +0100
Subject: [PATCH 01/18] wip: lemmas about step size iterator

---
 src/Init/Data/Iterators/Basic.lean            |  12 ++
 src/Init/Data/Iterators/Consumers/Access.lean |  38 ++++
 .../Iterators/Consumers/Monadic/Access.lean   |  26 +++
 .../Combinators/Monadic/StepSize.lean         |   6 +
 .../Data/Iterators/Combinators/StepSize.lean  |   6 +
 .../Lemmas/Combinators/Monadic/StepSize.lean  |  31 ++++
 .../Lemmas/Combinators/StepSize.lean          | 175 ++++++++++++++++++
 .../Iterators/Producers/Monadic/Array.lean    |  36 ++++
 8 files changed, 330 insertions(+)
 create mode 100644 src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean
 create mode 100644 src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean

diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean
index 2ade57faa3a8..687c8305d343 100644
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -214,6 +214,12 @@ theorem Iter.toIterM_comp_toIter {α : Type w} {β : Type w} :
     Iter.toIterM ∘ IterM.toIter (α := α) (β := β) = id :=
   rfl
 
+theorem Iter.toIterM_inj :
+    Iter.toIterM it = Iter.toIterM it' ↔ it = it' := by
+  apply Iff.intro
+  · cases it; cases it'; simp [Iter.toIterM]
+  · simp +contextual
+
 section IterStep
 
 variable {α : Type u} {β : Type w}
@@ -297,6 +303,12 @@ theorem IterStep.mapIterator_comp {α' : Type u'} {α'' : Type u''}
   apply funext
   exact fun _ => mapIterator_mapIterator.symm
 
+theorem IterStep.mapIterator_inj {α' : Type u'} {f : α → α'} {s s'} (hf : ∀ a b, f a = f b → a = b) :
+    IterStep.mapIterator (β := β) f s = IterStep.mapIterator (β := β) f s' ↔ s = s' := by
+  replace hf (a b : α) : f a = f b ↔ a = b := ⟨hf a b, by simp +contextual⟩
+  simp only [mapIterator]
+  split <;> split <;> simp [hf]
+
 @[simp]
 theorem IterStep.mapIterator_id {step : IterStep α β} :
     step.mapIterator id = step := by
diff --git a/src/Init/Data/Iterators/Consumers/Access.lean b/src/Init/Data/Iterators/Consumers/Access.lean
index 205861a4d249..e233dd65099d 100644
--- a/src/Init/Data/Iterators/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Access.lean
@@ -19,6 +19,44 @@ set_option linter.missingDocs true
 namespace Std
 open Std.Iterators
 
+def Iter.IsPlausibleNthOutputStep {α β : Type w} [Iterator α Id β]
+    (n : Nat) (it : Iter (α := α) β) (step : IterStep (Iter (α := α) β) β) : Prop :=
+  it.toIterM.IsPlausibleNthOutputStep n (step.mapIterator Iter.toIterM)
+
+/--
+Returns the step in which `it` yields its `n`-th element, or `.done` if it terminates earlier.
+In contrast to `step`, this function will always return either `.yield` or `.done` but never a
+`.skip` step.
+
+For monadic iterators, the monadic effects of this operation may differ from manually iterating
+to the `n`-th value because `nextAtIdx?` can take shortcuts. By the signature, the return value
+is guaranteed to plausible in the sense of `IterM.IsPlausibleNthOutputStep`.
+
+This function is only available for iterators that explicitly support it by implementing
+the `IteratorAccess` typeclass.
+-/
+@[inline]
+def Iter.nextAtIdx? [Iterator α Id β] [IteratorAccess α Id] (it : Iter (α := α) β)
+    (n : Nat) : PlausibleIterStep (it.IsPlausibleNthOutputStep n) :=
+  let step := it.toIterM.nextAtIdx? n |>.run
+  ⟨step.val.mapIterator IterM.toIter, by simp [IsPlausibleNthOutputStep, step.property]⟩
+
+/--
+Slow version of `IterM.nextAtIdx?` that does not require an `IteratorAccess α m` instance.
+
+Returns the step in which `it` yields its `n`-th element, or `.done` if it terminates earlier.
+In contrast to `step`, this function will always return either `.yield` or `.done` but never a
+`.skip` step.
+
+This function terminates after finitely many steps.
+-/
+@[inline]
+def Iter.nextAtIdxSlow? [Iterator α Id β] [Productive α Id]
+    (it : Iter (α := α) β)
+    (n : Nat) : PlausibleIterStep (it.IsPlausibleNthOutputStep n) :=
+  let step := it.toIterM.nextAtIdxSlow? n |>.run
+  ⟨step.val.mapIterator IterM.toIter, by simp [IsPlausibleNthOutputStep, step.property]⟩
+
 /--
 If possible, takes `n` steps with the iterator `it` and
 returns the `n`-th emitted value, or `none` if `it` finished
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
index da556b180dab..190a3e762943 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Iterators.Basic
+public import Init.WFExtrinsicFix
 
 set_option linter.missingDocs true
 
@@ -95,6 +96,31 @@ def IterM.nextAtIdx? [Iterator α m β] [IteratorAccess α m] (it : IterM (α :=
     (n : Nat) : m (PlausibleIterStep (it.IsPlausibleNthOutputStep n)) :=
   IteratorAccess.nextAtIdx? it n
 
+/--
+Slow version of `IterM.nextAtIdx?` that does not require an `IteratorAccess α m` instance.
+
+Returns the step in which `it` yields its `n`-th element, or `.done` if it terminates earlier.
+In contrast to `step`, this function will always return either `.yield` or `.done` but never a
+`.skip` step.
+
+This function terminates after finitely many steps.
+-/
+@[inline]
+def IterM.nextAtIdxSlow? [Monad m] [Iterator α m β] [Productive α m]
+    (it : IterM (α := α) m β)
+    (n : Nat) : m (PlausibleIterStep (it.IsPlausibleNthOutputStep n)) :=
+  go it n (fun s => id)
+where
+  go [Productive α m] it' n' (h : ∀ s, it'.IsPlausibleNthOutputStep n' s → it.IsPlausibleNthOutputStep n s) := do
+    match (← it'.step).inflate with
+    | .yield it'' out hp =>
+      match n' with
+      | 0 => return .yield it'' out (h _ (.zero_yield hp))
+      | k + 1 => go it'' k (fun s hp' => h s (.yield hp hp'))
+    | .skip it'' hp => go it'' n' (fun s hp' => h s (.skip hp hp'))
+    | .done hp => return .done (h _ (.done hp))
+  termination_by (n', it'.finitelyManySkips)
+
 /--
 Returns the `n`-th value emitted by `it`, or `none` if `it` terminates earlier.
 
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
index 440d1cbd8399..ef5987fec3d7 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
@@ -55,6 +55,12 @@ def IterM.stepSize [Iterator α m β] [IteratorAccess α m] [Monad m]
     IterM (α := Types.StepSizeIterator α m β) m β :=
   ⟨⟨0, n - 1, it⟩⟩
 
+@[inline]
+def IterM.Intermediate.stepSize [Iterator α m β] [IteratorAccess α m] [Monad m]
+    (it : IterM (α := α) m β) (nextIdx : Nat) (n : Nat) :
+    IterM (α := Types.StepSizeIterator α m β) m β :=
+  ⟨⟨0, nextIdx, it⟩⟩
+
 namespace Iterators.Types
 
 instance StepSizeIterator.instIterator [Iterator α m β] [IteratorAccess α m] [Monad m] :
diff --git a/src/Std/Data/Iterators/Combinators/StepSize.lean b/src/Std/Data/Iterators/Combinators/StepSize.lean
index 61fe8330c763..32e546d4c731 100644
--- a/src/Std/Data/Iterators/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Combinators/StepSize.lean
@@ -23,4 +23,10 @@ def Iter.stepSize [Iterator α Id β] [IteratorAccess α Id]
     Iter (α := Types.StepSizeIterator α Id β) β :=
   (it.toIterM.stepSize n).toIter
 
+@[inline]
+def Iter.Intermediate.stepSize [Iterator α Id β] [IteratorAccess α Id]
+    (it : Iter (α := α) β) (nextIdx n : Nat) :
+    Iter (α := Types.StepSizeIterator α Id β) β :=
+  (IterM.Intermediate.stepSize it.toIterM nextIdx n).toIter
+
 end Std
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean
new file mode 100644
index 000000000000..281abf497292
--- /dev/null
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean
@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 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 Std.Data.Iterators.Combinators.Monadic.StepSize
+
+public section
+open Std Std.Iterators Std.Iterators.Types
+
+namespace Std.IterM
+
+-- example [Iterator α Id β] [IteratorAccess α Id] [LawfulDeterministicIterator α Id] :
+--     Productive α Id where
+--   wf := by
+--     constructor
+--     intro it
+--     have :=
+
+-- instance [Iterator α m β] [LawfulDeterministicIterator α m] [IteratorAccess α m] [Monad m] :
+--     LawfulDeterministicIterator (StepSizeIterator α m β) m where
+--   isPlausibleStep_eq_eq it := by
+--     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, funext_iff]
+--     obtain ⟨⟨
+
+-- theorem step_stepSize
+
+end Std.IterM
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
new file mode 100644
index 000000000000..0409e1fae8d5
--- /dev/null
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -0,0 +1,175 @@
+/-
+Copyright (c) 2026 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.Consumers.Access
+public import Init.Data.Iterators.Consumers.Collect
+public import Init.Data.Iterators.Combinators.Take
+public import Std.Data.Iterators.Combinators.StepSize
+import Init.Data.Iterators.Lemmas.Consumers.Access
+
+public section
+open Std Std.Iterators Std.Iterators.Types
+
+namespace Std.Iter
+
+-- example [Iterator α Id β] [IteratorAccess α Id] [LawfulDeterministicIterator α Id] :
+--     Productive α Id where
+--   wf := by
+--     constructor
+--     intro it
+--     have :=
+
+-- instance [Iterator α m β] [LawfulDeterministicIterator α m] [IteratorAccess α m] [Monad m] :
+--     LawfulDeterministicIterator (StepSizeIterator α m β) m where
+--   isPlausibleStep_eq_eq it := by
+--     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, funext_iff]
+--     obtain ⟨⟨
+
+-- theorem step_stepSize
+
+instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α := α) Id β} :
+    Subsingleton it.Step where
+  allEq s s' := by
+    obtain ⟨s'', hs''⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq it
+    obtain ⟨s, hs⟩ := s
+    obtain ⟨s', hs'⟩ := s'
+    simp only [hs''] at hs hs'
+    have := hs.trans hs'.symm
+    rwa [Subtype.mk.injEq]
+
+instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : Iter (α := α) β} :
+    Subsingleton it.Step where
+  allEq s s' := by
+    obtain ⟨s'', hs''⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq it.toIterM
+    obtain ⟨s, hs⟩ := s
+    obtain ⟨s', hs'⟩ := s'
+    simp only [Iter.IsPlausibleStep, hs''] at hs hs'
+    have := hs.trans hs'.symm
+    rw [IterStep.mapIterator_inj (fun _ _ => toIterM_inj.mp) ] at this
+    rwa [Subtype.mk.injEq]
+
+theorem eq_step_of_isPlausibleStep [Iterator α Id β] [LawfulDeterministicIterator α Id]
+    {it : Iter (α := α) β} {step} (h : it.IsPlausibleStep step) :
+    step = it.step.val := by
+  have : ⟨step, h⟩ = it.step := Subsingleton.allEq _ _
+  simp [← this]
+
+theorem _root_.Std.IterM.eq_step_of_isPlausibleStep [Iterator α Id β] [LawfulDeterministicIterator α Id]
+    {it : IterM (α := α) Id β} {step} (h : it.IsPlausibleStep step) :
+    step = it.step.run.inflate.val := by
+  have : ⟨step, h⟩ = it.step.run.inflate := Subsingleton.allEq _ _
+  simp [← this]
+
+theorem _root_.Std.IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep [Iterator α Id β]
+    [LawfulDeterministicIterator α Id]
+    {it : IterM (α := α) Id β} {s s'}
+    (hs : it.IsPlausibleNthOutputStep n s)
+    (hs' : it.IsPlausibleNthOutputStep n s') :
+    s = s' := by
+  induction hs
+  case zero_yield h =>
+    match hs' with
+    | .zero_yield h' ..
+    | .skip h' ..
+    | .done h' =>
+      replace h := IterM.eq_step_of_isPlausibleStep h
+      replace h' := IterM.eq_step_of_isPlausibleStep h'
+      rw [← h] at h'
+      cases h'
+      all_goals rfl
+  case done h =>
+    match hs' with
+    | .zero_yield h' ..
+    | .yield h' ..
+    | .skip h' ..
+    | .done h' =>
+      replace h := IterM.eq_step_of_isPlausibleStep h
+      replace h' := IterM.eq_step_of_isPlausibleStep h'
+      rw [← h] at h'
+      all_goals cases h'
+      all_goals rfl
+  case yield h _ ih =>
+    match hs' with
+    | .yield h' ..
+    | .skip h' ..
+    | .done h' =>
+      replace h := IterM.eq_step_of_isPlausibleStep h
+      replace h' := IterM.eq_step_of_isPlausibleStep h'
+      rw [← h] at h'
+      cases h'
+      all_goals
+        apply ih ‹_›
+  case skip h _ ih =>
+    match hs' with
+    | .zero_yield h' ..
+    | .yield h' ..
+    | .skip h' ..
+    | .done h' =>
+      replace h := IterM.eq_step_of_isPlausibleStep h
+      replace h' := IterM.eq_step_of_isPlausibleStep h'
+      rw [← h] at h'
+      cases h'
+      all_goals
+        apply ih ‹_›
+
+instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α := α) Id β} :
+    Subsingleton (PlausibleIterStep (it.IsPlausibleNthOutputStep n)) where
+  allEq s s' := by
+    obtain ⟨s, hs⟩ := s
+    obtain ⟨s', hs'⟩ := s'
+    have := IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep hs hs'
+    rwa [Subtype.mk.injEq]
+
+theorem _root_.Std.IterM.step_stepSize [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
+    it.nextAtIdx? n = it.nextAtIdxSlow? n := by
+  ext
+  apply Subsingleton.allEq
+
+theorem step_stepSize [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
+    it.nextAtIdx? n = it.nextAtIdxSlow? n := by
+  simp [Iter.nextAtIdx?, Iter.nextAtIdxSlow?, IterM.step_stepSize]
+
+theorem atIdxSlow?_stepSize_aux [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
+    (Iter.Intermediate.stepSize it i n).atIdxSlow? k = it.atIdxSlow? (i + (n - 1 + 1) * k) := by
+  induction k
+  · simp
+    induction i, it using Iter.atIdxSlow?.induct_unfolding
+    case yield_zero it it' _ h _ =>
+      rw [atIdxSlow?_eq_match]
+      simp [Intermediate.stepSize, IterM.Intermediate.stepSize, Iter.step_eq]
+      cases (it.toIterM.nextAtIdx? 0).run using PlausibleIterStep.casesOn
+      · rename_i h'
+        simp [Iter.IsPlausibleStep] at h
+        replace h := IterM.IsPlausibleNthOutputStep.zero_yield h
+        cases IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h h'
+        simp
+      · rename_i h'
+        simp [Iter.IsPlausibleStep] at h
+        replace h := IterM.IsPlausibleNthOutputStep.zero_yield h
+        cases IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h h'
+      · rename_i h'
+        simp [Iter.IsPlausibleStep] at h
+        replace h := IterM.IsPlausibleNthOutputStep.zero_yield h
+        cases IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h h'
+    case yield_succ it it' _ h _ =>
+      rw [atIdxSlow?_eq_match, atIdxSlow?_eq_match]
+  generalize h : Iter.Intermediate.stepSize it i n = sit
+  induction k, sit using Iter.atIdxSlow?.induct_unfolding
+  case yield_zero =>
+    simp
+    simp [Intermediate.stepSize, IterM.Intermediate.stepSize] at h
+
+theorem atIdxSlow?_stepSize [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
+    (it.stepSize n).atIdxSlow? k = it.atIdxSlow? ((n - 1 + 1) * k) := by
+
+
+end Std.Iter
diff --git a/src/Std/Data/Iterators/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
index 0a3ad4c7f97a..f293c322743b 100644
--- a/src/Std/Data/Iterators/Producers/Monadic/Array.lean
+++ b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Iterators.Consumers
 import Init.Omega
+meta import Init.ByCases
 
 @[expose] public section
 
@@ -116,4 +117,39 @@ instance ArrayIterator.instIteratorLoop {α : Type w} [Monad m] {n : Type x →
     IteratorLoop (ArrayIterator α) m n :=
   .defaultImplementation
 
+instance : IteratorAccess (ArrayIterator α) Id where
+  nextAtIdx? it n :=
+    let step : IterStep (IterM (α := ArrayIterator α) Id α) α :=
+      if h : it.internalState.pos + n < it.internalState.array.size then
+        .yield
+          ⟨⟨it.internalState.array, it.internalState.pos + n + 1⟩⟩
+          it.internalState.array[it.internalState.pos + n]
+      else
+        .done
+    haveI : IterM.IsPlausibleNthOutputStep n it step := by
+      simp only [step]; clear step
+      induction n generalizing it
+      · split
+        · refine .zero_yield ?_
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, *]
+        · refine .done ?_
+          simp_all [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+      · rename_i n ih
+        by_cases h : it.internalState.pos < it.internalState.array.size
+        · refine .yield (it' := ?it') (out := ?_) ?_ ?_
+          · exact ⟨⟨it.internalState.array, it.internalState.pos + 1⟩⟩
+          · exact it.internalState.array[it.internalState.pos]
+          · simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          · specialize ih ?it'
+            simp only [Nat.add_comm 1, Nat.add_assoc] at ih ⊢
+            split
+            · rw [dif_pos (by omega)] at ih
+              apply ih
+            · rw [dif_neg (by omega)] at ih
+              apply ih
+        · rw [dif_neg (by omega)]
+          refine .done (α := ArrayIterator α) (m := Id) ?_
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep] using h
+    pure ⟨step, this⟩
+
 end Std.Iterators.Types

From 40571b00b65c53fbd45befbae06b6edd582870b4 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sat, 14 Feb 2026 21:20:22 +0100
Subject: [PATCH 02/18] wip

---
 .../Iterators/Consumers/Monadic/Access.lean   |  64 +++++++-
 src/Init/Data/Iterators/Consumers/Stream.lean |   2 +-
 .../Iterators/Lemmas/Consumers/Access.lean    |  25 +++
 .../Lemmas/Consumers/Monadic/Access.lean      | 139 ++++++++++++++++
 .../Combinators/Monadic/StepSize.lean         |   2 +-
 .../Lemmas/Combinators/StepSize.lean          | 154 +++++++++++++++++-
 6 files changed, 380 insertions(+), 6 deletions(-)
 create mode 100644 src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean

diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
index 190a3e762943..424e131c8d2a 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Iterators.Basic
 public import Init.WFExtrinsicFix
+import Init.RCases
 
 set_option linter.missingDocs true
 
@@ -47,7 +48,7 @@ inductive IterM.IsPlausibleNthOutputStep {α β : Type w} {m : Type w → Type w
   | skip {it it' : IterM (α := α) m β} {step} : it.IsPlausibleStep (.skip it') →
       it'.IsPlausibleNthOutputStep n step → it.IsPlausibleNthOutputStep n step
 
-theorem IterM.not_isPlausibleNthOutputStep_yield {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+theorem IterM.not_isPlausibleNthOutputStep_skip {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     {n : Nat} {it it' : IterM (α := α) m β} :
     ¬ it.IsPlausibleNthOutputStep n (.skip it') := by
   intro h
@@ -58,6 +59,45 @@ theorem IterM.not_isPlausibleNthOutputStep_yield {α β : Type w} {m : Type w 
   · simp_all
   · simp_all
 
+theorem IterM.isPlausibleNthOutputStep_trans_of_yield {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β] {k n} {it it' : IterM (α := α) m β} {out step}
+    (h : it.IsPlausibleNthOutputStep k (.yield it' out))
+    (h' : it'.IsPlausibleNthOutputStep n step) :
+    it.IsPlausibleNthOutputStep (n + k + 1) step := by
+  generalize hs : (IterStep.yield it' out) = s at h
+  induction h generalizing h' it' out
+  case zero_yield =>
+    cases hs
+    exact .yield ‹_› h'
+  case done => cases hs
+  case yield ih =>
+    cases hs
+    refine .yield ‹_› ?_
+    simp only [Nat.add_assoc] at ih
+    exact ih h' rfl
+  case skip ih =>
+    cases hs
+    refine .skip ‹_› ?_
+    apply ih h' rfl
+
+theorem IterM.isPlausibleNthOutputStep_trans_of_done {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β] {k n} {it : IterM (α := α) m β}
+    (h : it.IsPlausibleNthOutputStep k .done) (hle : k ≤ n) :
+    it.IsPlausibleNthOutputStep n .done := by
+  generalize hs : IterStep.done = s at h
+  induction h generalizing n
+  case zero_yield => cases hs
+  case yield ih =>
+    cases hs
+    obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero (n := n) (Nat.ne_zero_of_lt (Nat.lt_of_add_one_le hle))
+    exact .yield ‹_› (ih (Nat.le_of_add_le_add_right hle) rfl)
+  case skip ih =>
+    cases hs
+    exact .skip ‹_› (ih hle rfl)
+  case done =>
+    cases hs
+    exact .done ‹_›
+
 /--
 `IteratorAccess α m` provides efficient implementations for random access or iterators that support
 it. `it.nextAtIdx? n` either returns the step in which the `n`th value of `it` is emitted
@@ -103,6 +143,28 @@ Returns the step in which `it` yields its `n`-th element, or `.done` if it termi
 In contrast to `step`, this function will always return either `.yield` or `.done` but never a
 `.skip` step.
 
+This function terminates after finitely many steps.
+-/
+@[inline]
+def IterM.atIdxSlow? [Monad m] [Iterator α m β] [Productive α m]
+    (it' : IterM (α := α) m β)
+    (n' : Nat) : m (Option β) := do
+    match (← it'.step).inflate with
+    | .yield it'' out _ =>
+      match n' with
+      | 0 => return some out
+      | k + 1 => atIdxSlow? it'' k
+    | .skip it'' _ => atIdxSlow? it'' n'
+    | .done _ => return none
+  termination_by (n', it'.finitelyManySkips)
+
+/--
+Slow version of `IterM.nextAtIdx?` that does not require an `IteratorAccess α m` instance.
+
+Returns the step in which `it` yields its `n`-th element, or `.done` if it terminates earlier.
+In contrast to `step`, this function will always return either `.yield` or `.done` but never a
+`.skip` step.
+
 This function terminates after finitely many steps.
 -/
 @[inline]
diff --git a/src/Init/Data/Iterators/Consumers/Stream.lean b/src/Init/Data/Iterators/Consumers/Stream.lean
index 9e477f0663f6..1267459875dc 100644
--- a/src/Init/Data/Iterators/Consumers/Stream.lean
+++ b/src/Init/Data/Iterators/Consumers/Stream.lean
@@ -25,6 +25,6 @@ instance {α β} [Iterator α Id β] [Productive α Id] [IteratorAccess α Id] :
   where finally
     case noskip =>
       revert h
-      exact IterM.not_isPlausibleNthOutputStep_yield
+      exact IterM.not_isPlausibleNthOutputStep_skip
 
 end Std
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
index 43bd0f8c9ddc..bb3763c508c5 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
@@ -7,10 +7,35 @@ module
 
 prelude
 public import Init.Data.Iterators.Consumers.Access
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Access
 
 namespace Std.Iter
 open Std.Iterators
 
+public theorem nextAtIdxSlow?_eq_match [Iterator α Id β] [Productive α Id]
+    {n : Nat} {it : Iter (α := α) β} :
+    it.nextAtIdxSlow? n =
+      (match it.step with
+      | .yield it' out hp =>
+        match n with
+        | 0 => .yield it' out (.zero_yield hp)
+        | n + 1 =>
+          let s := it'.nextAtIdxSlow? n
+          ⟨s.val, .yield hp s.property⟩
+      | .skip it' hp =>
+        let s := it'.nextAtIdxSlow? n
+        ⟨s.val, .skip hp s.property⟩
+      | .done hp => .done (.done hp)) := by
+  simp [Iter.nextAtIdxSlow?]
+  apply Subtype.ext
+  simp only
+  rw [IterM.nextAtIdxSlow?_eq_match]
+  simp only [bind_pure_comp, Id.run_bind, step]
+  split
+  · cases n <;> simp [*]
+  · simp [*]
+  · simp [*]
+
 public theorem atIdxSlow?_eq_match [Iterator α Id β] [Productive α Id]
     {n : Nat} {it : Iter (α := α) β} :
     it.atIdxSlow? n =
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
new file mode 100644
index 000000000000..9f8f1553736a
--- /dev/null
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2026 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.Consumers.Monadic.Access
+import all Init.Data.Iterators.Consumers.Monadic.Access
+public import Init.Control.Lawful.Basic
+import Init.Control.Lawful.Lemmas
+
+namespace Std.IterM
+open Std.Iterators
+
+
+public theorem atIdxSlow?_eq_match [Monad m] [LawfulMonad m] [Iterator α m β] [Productive α m]
+    {n : Nat} {it : IterM (α := α) m β} :
+    it.atIdxSlow? n = (do
+      match (← it.step).inflate.val with
+      | .yield it' out =>
+        match n with
+        | 0 => return some out
+        | n + 1 => it'.atIdxSlow? n
+      | .skip it' => it'.atIdxSlow? n
+      | .done => return none) := by
+  sorry
+
+private theorem val_nextAtIdxSlow?Go [Monad m] [LawfulMonad m] [Iterator α m β] [Productive α m]
+    {n : Nat} {it : IterM (α := α) m β} {n' it' h} :
+    Subtype.val <$> IterM.nextAtIdxSlow?.go it n it' n' h =
+      Subtype.val <$> IterM.nextAtIdxSlow? it' n' := by
+  induction it', n' using IterM.atIdxSlow?.induct generalizing it n
+  rw [IterM.nextAtIdxSlow?, IterM.nextAtIdxSlow?.go, IterM.nextAtIdxSlow?.go]
+  simp only [map_eq_pure_bind, bind_assoc]
+  apply bind_congr; intro step
+  rename_i it' n' ih₁ ih₂
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp
+    cases n'
+    · simp
+    · simp only at ih₁
+      simp [ih₁]
+  · simp only at ih₂
+    simp (discharger := assumption) [ih₂]
+  · simp
+
+public theorem val_nextAtIdxSlow?_eq_match [Monad m] [LawfulMonad m] [Iterator α m β] [Productive α m]
+    {n : Nat} {it : IterM (α := α) m β} :
+    Subtype.val <$> it.nextAtIdxSlow? n = (do
+      match (← it.step).inflate.val with
+      | .yield it' out =>
+        match n with
+        | 0 => return .yield it' out
+        | n + 1 => return (← it'.nextAtIdxSlow? n).val
+      | .skip it' => return (← it'.nextAtIdxSlow? n).val
+      | .done =>
+        return .done) := by
+  rw [IterM.nextAtIdxSlow?, IterM.nextAtIdxSlow?.go]
+  simp only [map_eq_pure_bind, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · cases n
+    · simp
+    · simp [val_nextAtIdxSlow?Go]
+  · simp [val_nextAtIdxSlow?Go]
+  · simp
+
+public theorem nextAtIdxSlow?_eq_match [Monad m] [LawfulMonad m] [Iterator α m β] [Productive α m]
+    {n : Nat} {it : IterM (α := α) m β} :
+    it.nextAtIdxSlow? n = (do
+      match (← it.step).inflate with
+      | .yield it' out hp =>
+        match n with
+        | 0 => return .yield it' out (.zero_yield hp)
+        | n + 1 =>
+          let s ← it'.nextAtIdxSlow? n
+          return ⟨s.val, .yield hp s.property⟩
+      | .skip it' hp =>
+          let s ← it'.nextAtIdxSlow? n
+          return ⟨s.val, .skip hp s.property⟩
+      | .done hp =>
+        return .done (.done hp)) := by
+  apply (map_inj_right Subtype.ext).mp
+  rw [val_nextAtIdxSlow?_eq_match]
+  simp only [map_eq_pure_bind, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · cases n <;> simp
+  · simp
+  · simp
+
+public theorem nextAtIdxSlow?_eq_match_nextAtIdxSlow? [Monad m] [LawfulMonad m] [Iterator α m β] [Productive α m]
+    {n : Nat} {it : IterM (α := α) m β} :
+    it.nextAtIdxSlow? n = (do
+      let step ← it.nextAtIdxSlow? 0
+      match n with
+      | 0 => return step
+      | n + 1 =>
+        match step with
+        | .yield it' out hp =>
+          let s ← it'.nextAtIdxSlow? n
+          return ⟨s.val, isPlausibleNthOutputStep_trans_of_yield hp s.property⟩
+        | .skip it' hp => not_isPlausibleNthOutputStep_skip.elim hp
+        | .done hp => return ⟨.done, isPlausibleNthOutputStep_trans_of_done (k := 0) hp (Nat.zero_le _)⟩) := by
+  fun_induction it.atIdxSlow? n
+  rename_i ih₁ ih₂
+  rw [nextAtIdxSlow?_eq_match, nextAtIdxSlow?_eq_match]
+  simp only [bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp
+  · simp
+    simp at ih₁ ih₂
+    rw [ih₂]
+    · simp
+      apply bind_congr; intro step'
+      split
+      · simp
+      · simp
+        split
+        · simp
+        · exact not_isPlausibleNthOutputStep_skip.elim ‹_›
+        · simp
+    · assumption
+  · simp
+    split <;> simp
+
+public theorem nextAtIdxSlow?_add_one [Monad m] [LawfulMonad m] [Iterator α m β] [Productive α m]
+    {n : Nat} {it : IterM (α := α) m β} :
+    it.nextAtIdxSlow? (n + 1) = (do
+      match ← it.nextAtIdxSlow? 0 with
+      | .yield it' _ hp =>
+        let s ← it'.nextAtIdxSlow? n
+        return ⟨s.val, isPlausibleNthOutputStep_trans_of_yield hp s.property⟩
+      | .skip _ hp => not_isPlausibleNthOutputStep_skip.elim hp
+      | .done hp => return ⟨.done, isPlausibleNthOutputStep_trans_of_done (k := 0) hp (Nat.zero_le _)⟩) := by
+  rw [nextAtIdxSlow?_eq_match_nextAtIdxSlow?]
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
index ef5987fec3d7..9ccc460c028e 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
@@ -59,7 +59,7 @@ def IterM.stepSize [Iterator α m β] [IteratorAccess α m] [Monad m]
 def IterM.Intermediate.stepSize [Iterator α m β] [IteratorAccess α m] [Monad m]
     (it : IterM (α := α) m β) (nextIdx : Nat) (n : Nat) :
     IterM (α := Types.StepSizeIterator α m β) m β :=
-  ⟨⟨0, nextIdx, it⟩⟩
+  ⟨⟨nextIdx, n - 1, it⟩⟩
 
 namespace Iterators.Types
 
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
index 0409e1fae8d5..94814c5a4267 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -8,9 +8,15 @@ module
 prelude
 public import Init.Data.Iterators.Consumers.Access
 public import Init.Data.Iterators.Consumers.Collect
+public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Combinators.Take
 public import Std.Data.Iterators.Combinators.StepSize
 import Init.Data.Iterators.Lemmas.Consumers.Access
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Access
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+import Init.Data.Iterators.Lemmas.Monadic.Basic
+import all Init.Data.Iterators.Consumers.Monadic.Access
+import all Std.Data.Iterators.Combinators.StepSize
 
 public section
 open Std Std.Iterators Std.Iterators.Types
@@ -125,16 +131,157 @@ instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α
     have := IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep hs hs'
     rwa [Subtype.mk.injEq]
 
-theorem _root_.Std.IterM.step_stepSize [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
+theorem _root_.Std.IterM.nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
     it.nextAtIdx? n = it.nextAtIdxSlow? n := by
   ext
   apply Subsingleton.allEq
 
-theorem step_stepSize [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
+theorem nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
     it.nextAtIdx? n = it.nextAtIdxSlow? n := by
-  simp [Iter.nextAtIdx?, Iter.nextAtIdxSlow?, IterM.step_stepSize]
+  simp [Iter.nextAtIdx?, Iter.nextAtIdxSlow?, IterM.nextAtIdx?_eq_nextAtIdxSlow?]
+
+theorem _root_.Std.IterM.nextAtIdxSlow?_stepSize_aux [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
+    (IterM.Intermediate.stepSize it i n).nextAtIdxSlow? 0 = (do
+      match (← it.nextAtIdxSlow? i) with
+      | .yield it' out h =>
+        return .yield (IterM.Intermediate.stepSize it' (n - 1) n) out (by
+          refine .zero_yield ?_
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+            IterM.Intermediate.stepSize, IterM.Intermediate.stepSize])
+      | .skip it' h => return IterM.not_isPlausibleNthOutputStep_skip.elim h
+      | .done h =>
+        return .done (by
+          refine .done ?_
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+            Intermediate.stepSize, IterM.Intermediate.stepSize])) := by
+  induction it, i using IterM.atIdxSlow?.induct_unfolding
+  simp [IterM.Intermediate.stepSize]
+  rw [IterM.nextAtIdxSlow?_eq_match]
+  simp [IterM.step_eq, IterM.nextAtIdx?_eq_nextAtIdxSlow?]
+  apply bind_congr; intro step
+  cases step using PlausibleIterStep.casesOn
+  · simp
+  · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
+  · simp
+
+theorem _root_.Std.IterM.length_nextAtIdxSlow? [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} :
+    (do match ← it.nextAtIdxSlow? n with
+      | .yield it' out _ => it'.length
+      | .skip it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
+      | .done h => return .up 0) = (fun len => .up (len.down - n - 1)) <$> it.length := by
+  induction it using IterM.inductSteps generalizing n with | step it ihy ihs
+  rw [it.nextAtIdxSlow?_eq_match, it.length_eq_match_step]
+  simp only [map_eq_pure_bind, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp
+    split
+    · simp
+    · rename_i it' out h n n'
+      simp
+      refine Eq.trans ?_ ((ihy h (n := n')).trans ?_)
+      · apply bind_congr; intro step
+        cases step using PlausibleIterStep.casesOn
+        · simp
+        · rfl
+        · simp
+      · simp [Nat.add_sub_add_right]
+  · rename_i it' h n _ h
+    simp
+    refine Eq.trans ?_ ((ihs h (n := n)).trans ?_)
+    · apply bind_congr; intro step
+      cases step using PlausibleIterStep.casesOn
+      · simp
+      · rfl
+      · simp
+    · simp
+  · simp
+
+theorem length_nextAtIdxSlow? [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} :
+    (match it.nextAtIdxSlow? n with
+      | .yield it' out _ => it'.length
+      | .skip it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
+      | .done h => 0) = it.length - n - 1 := by
+  have := IterM.length_nextAtIdxSlow? (it := it.toIterM) (n := n)
+  replace this := congrArg Id.run this
+  replace this := congrArg ULift.down this
+  simp at this
+  simp [Iter.length, ← this, Iter.nextAtIdxSlow?]
+  split at this
+  · simp [*]
+  · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
+  · simp [*]
+
+theorem _root_.Std.IterM.length_stepSize [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    [IteratorAccess α Id] {it : IterM (α := α) Id β} :
+    (IterM.Intermediate.stepSize it i n).length.run.down = (it.length.run.down + (n - 1) - i) / (n - 1 + 1) := by
+  induction n generalizing it i
+  · rw [IterM.length_eq_match_step, IterM.length_eq_match_step, IterM.step_eq]
+    simp [IterM.Intermediate.stepSize]
+    cases (it.nextAtIdx? i).run using PlausibleIterStep.casesOn
+    · simp
+      rw [IterM.length_eq_match_step]
+      simp
+
+theorem _root_.Std.IterM.step_stepSize [Iterator α Id β] [Finite α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : IterM (α := α) Id β} :
+    (IterM.Intermediate.stepSize it i n).step.run.inflate.val =
+      match it.step.run.inflate.val with
+      | .yield it' out =>
+        match i with
+        | 0 => .yield (IterM.Intermediate.stepSize it' (n - 1) n) out
+        | i + 1 => .skip (IterM.Intermediate.stepSize it' i n)
+      | .skip it' => .skip (IterM.Intermediate.stepSize it' i n)
+      | .done => .done := by
+  rw [IterM.step_eq]
+  simp [IterM.Intermediate.stepSize, IterM.nextAtIdx?_eq_nextAtIdxSlow?]
+  rw [IterM.nextAtIdxSlow?_eq_match]
+  simp
+  cases it.step.run.inflate using PlausibleIterStep.casesOn
+  · simp
+    split
+    · simp
+    · simp
+
+
+theorem _root_.Std.IterM.length_stepSize [Iterator α Id β] [Finite α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : IterM (α := α) Id β} {i n : Nat} :
+    (IterM.Intermediate.stepSize it i n).length.run.down = (it.length.run.down + (n - 1) - i) / (n - 1 + 1) := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [IterM.length_eq_match_step, IterM.length_eq_match_step, step_stepSize]
+
+theorem atIdxSlow?_stepSize_aux [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
+    (Intermediate.stepSize it i n).nextAtIdxSlow? 0 =
+      match it.nextAtIdxSlow? i with
+      | .yield it' out h =>
+        .yield (Intermediate.stepSize it' (n - 1) n) out (by
+          refine .zero_yield ?_
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+            Intermediate.stepSize, IterM.Intermediate.stepSize])
+      | .skip it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
+      | .done h =>
+        .done (by
+          refine .done ?_
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+            Intermediate.stepSize, IterM.Intermediate.stepSize]) := by
+  simp only [Iter.nextAtIdxSlow?]
+  simp only [Intermediate.stepSize, toIterM_toIter, IterM.nextAtIdxSlow?_stepSize_aux]
+  simp
+  apply Subtype.ext
+  simp
+  let step := (it.toIterM.nextAtIdxSlow? i).run
+  cases hs : step using PlausibleIterStep.casesOn
+  · simp [show (it.toIterM.nextAtIdxSlow? i).run = step from rfl]
+    simp [hs]
+  · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
+  · simp [show (it.toIterM.nextAtIdxSlow? i).run = step from rfl]
+    simp [hs]
 
 theorem atIdxSlow?_stepSize_aux [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
@@ -161,6 +308,7 @@ theorem atIdxSlow?_stepSize_aux [Iterator α Id β] [Productive α Id] [LawfulDe
         cases IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h h'
     case yield_succ it it' _ h _ =>
       rw [atIdxSlow?_eq_match, atIdxSlow?_eq_match]
+
   generalize h : Iter.Intermediate.stepSize it i n = sit
   induction k, sit using Iter.atIdxSlow?.induct_unfolding
   case yield_zero =>

From 448b1381746907f036cf6038aa2824a40a47e8d1 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sat, 28 Feb 2026 23:04:39 +0000
Subject: [PATCH 03/18] feat: add stepSize iterator verification lemmas and fix
 sorry

This PR adds comprehensive verification lemmas for the stepSize iterator
combinator, including atIdxSlow?_stepSize, atIdxSlow?_intermediate_stepSize,
and getElem?_toList_stepSize. It also proves the sorry in
IterM.atIdxSlow?_eq_match, adds a missing docstring for
Iter.IsPlausibleNthOutputStep, and fixes unused variable warnings.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/Init/Data/Iterators/Consumers/Access.lean |   1 +
 .../Lemmas/Consumers/Monadic/Access.lean      |   9 +-
 .../Lemmas/Combinators/StepSize.lean          | 219 +++++++++++-------
 3 files changed, 148 insertions(+), 81 deletions(-)

diff --git a/src/Init/Data/Iterators/Consumers/Access.lean b/src/Init/Data/Iterators/Consumers/Access.lean
index e233dd65099d..cccb1da23263 100644
--- a/src/Init/Data/Iterators/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Access.lean
@@ -19,6 +19,7 @@ set_option linter.missingDocs true
 namespace Std
 open Std.Iterators
 
+/-- Characterizes the plausible step when advancing to the `n`-th output of a pure iterator. -/
 def Iter.IsPlausibleNthOutputStep {α β : Type w} [Iterator α Id β]
     (n : Nat) (it : Iter (α := α) β) (step : IterStep (Iter (α := α) β) β) : Prop :=
   it.toIterM.IsPlausibleNthOutputStep n (step.mapIterator Iter.toIterM)
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
index 9f8f1553736a..676ce39abc13 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
@@ -25,7 +25,10 @@ public theorem atIdxSlow?_eq_match [Monad m] [LawfulMonad m] [Iterator α m β]
         | n + 1 => it'.atIdxSlow? n
       | .skip it' => it'.atIdxSlow? n
       | .done => return none) := by
-  sorry
+  rw [IterM.atIdxSlow?]
+  apply bind_congr; intro step
+  obtain ⟨val, prop⟩ := step.inflate
+  cases val <;> rfl
 
 private theorem val_nextAtIdxSlow?Go [Monad m] [LawfulMonad m] [Iterator α m β] [Productive α m]
     {n : Nat} {it : IterM (α := α) m β} {n' it' h} :
@@ -99,10 +102,10 @@ public theorem nextAtIdxSlow?_eq_match_nextAtIdxSlow? [Monad m] [LawfulMonad m]
       | 0 => return step
       | n + 1 =>
         match step with
-        | .yield it' out hp =>
+        | .yield it' _out hp =>
           let s ← it'.nextAtIdxSlow? n
           return ⟨s.val, isPlausibleNthOutputStep_trans_of_yield hp s.property⟩
-        | .skip it' hp => not_isPlausibleNthOutputStep_skip.elim hp
+        | .skip _it' hp => not_isPlausibleNthOutputStep_skip.elim hp
         | .done hp => return ⟨.done, isPlausibleNthOutputStep_trans_of_done (k := 0) hp (Nat.zero_le _)⟩) := by
   fun_induction it.atIdxSlow? n
   rename_i ih₁ ih₂
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
index 94814c5a4267..3b32ff2e765b 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -11,7 +11,10 @@ public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Combinators.Take
 public import Std.Data.Iterators.Combinators.StepSize
+import Init.Data.Iterators.Lemmas.Basic
+import Init.Omega
 import Init.Data.Iterators.Lemmas.Consumers.Access
+import Init.Data.Iterators.Lemmas.Consumers.Collect
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Access
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 import Init.Data.Iterators.Lemmas.Monadic.Basic
@@ -170,9 +173,9 @@ theorem _root_.Std.IterM.nextAtIdxSlow?_stepSize_aux [Iterator α Id β] [Produc
 theorem _root_.Std.IterM.length_nextAtIdxSlow? [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} :
     (do match ← it.nextAtIdxSlow? n with
-      | .yield it' out _ => it'.length
-      | .skip it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
-      | .done h => return .up 0) = (fun len => .up (len.down - n - 1)) <$> it.length := by
+      | .yield it' _out _ => it'.length
+      | .skip _it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
+      | .done _h => return .up 0) = (fun len => .up (len.down - n - 1)) <$> it.length := by
   induction it using IterM.inductSteps generalizing n with | step it ihy ihs
   rw [it.nextAtIdxSlow?_eq_match, it.length_eq_match_step]
   simp only [map_eq_pure_bind, bind_assoc]
@@ -204,9 +207,9 @@ theorem _root_.Std.IterM.length_nextAtIdxSlow? [Monad m] [LawfulMonad m] [Iterat
 theorem length_nextAtIdxSlow? [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β} :
     (match it.nextAtIdxSlow? n with
-      | .yield it' out _ => it'.length
-      | .skip it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
-      | .done h => 0) = it.length - n - 1 := by
+      | .yield it' _out _ => it'.length
+      | .skip _it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
+      | .done _h => 0) = it.length - n - 1 := by
   have := IterM.length_nextAtIdxSlow? (it := it.toIterM) (n := n)
   replace this := congrArg Id.run this
   replace this := congrArg ULift.down this
@@ -217,46 +220,9 @@ theorem length_nextAtIdxSlow? [Iterator α Id β] [Finite α Id] [IteratorLoop 
   · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
   · simp [*]
 
-theorem _root_.Std.IterM.length_stepSize [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
-    [IteratorAccess α Id] {it : IterM (α := α) Id β} :
-    (IterM.Intermediate.stepSize it i n).length.run.down = (it.length.run.down + (n - 1) - i) / (n - 1 + 1) := by
-  induction n generalizing it i
-  · rw [IterM.length_eq_match_step, IterM.length_eq_match_step, IterM.step_eq]
-    simp [IterM.Intermediate.stepSize]
-    cases (it.nextAtIdx? i).run using PlausibleIterStep.casesOn
-    · simp
-      rw [IterM.length_eq_match_step]
-      simp
-
-theorem _root_.Std.IterM.step_stepSize [Iterator α Id β] [Finite α Id] [LawfulDeterministicIterator α Id]
-    [IteratorAccess α Id] {it : IterM (α := α) Id β} :
-    (IterM.Intermediate.stepSize it i n).step.run.inflate.val =
-      match it.step.run.inflate.val with
-      | .yield it' out =>
-        match i with
-        | 0 => .yield (IterM.Intermediate.stepSize it' (n - 1) n) out
-        | i + 1 => .skip (IterM.Intermediate.stepSize it' i n)
-      | .skip it' => .skip (IterM.Intermediate.stepSize it' i n)
-      | .done => .done := by
-  rw [IterM.step_eq]
-  simp [IterM.Intermediate.stepSize, IterM.nextAtIdx?_eq_nextAtIdxSlow?]
-  rw [IterM.nextAtIdxSlow?_eq_match]
-  simp
-  cases it.step.run.inflate using PlausibleIterStep.casesOn
-  · simp
-    split
-    · simp
-    · simp
-
-
-theorem _root_.Std.IterM.length_stepSize [Iterator α Id β] [Finite α Id] [LawfulDeterministicIterator α Id]
-    [IteratorAccess α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : IterM (α := α) Id β} {i n : Nat} :
-    (IterM.Intermediate.stepSize it i n).length.run.down = (it.length.run.down + (n - 1) - i) / (n - 1 + 1) := by
-  induction it using IterM.inductSteps with | step it ihy ihs
-  rw [IterM.length_eq_match_step, IterM.length_eq_match_step, step_stepSize]
-
-theorem atIdxSlow?_stepSize_aux [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
-    [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
+theorem nextAtIdxSlow?_zero_intermediate_stepSize [Iterator α Id β] [Productive α Id]
+    [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {i n : Nat} :
     (Intermediate.stepSize it i n).nextAtIdxSlow? 0 =
       match it.nextAtIdxSlow? i with
       | .yield it' out h =>
@@ -283,41 +249,138 @@ theorem atIdxSlow?_stepSize_aux [Iterator α Id β] [Productive α Id] [LawfulDe
   · simp [show (it.toIterM.nextAtIdxSlow? i).run = step from rfl]
     simp [hs]
 
-theorem atIdxSlow?_stepSize_aux [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
-    [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
-    (Iter.Intermediate.stepSize it i n).atIdxSlow? k = it.atIdxSlow? (i + (n - 1 + 1) * k) := by
-  induction k
-  · simp
-    induction i, it using Iter.atIdxSlow?.induct_unfolding
-    case yield_zero it it' _ h _ =>
-      rw [atIdxSlow?_eq_match]
-      simp [Intermediate.stepSize, IterM.Intermediate.stepSize, Iter.step_eq]
-      cases (it.toIterM.nextAtIdx? 0).run using PlausibleIterStep.casesOn
-      · rename_i h'
-        simp [Iter.IsPlausibleStep] at h
-        replace h := IterM.IsPlausibleNthOutputStep.zero_yield h
-        cases IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h h'
-        simp
-      · rename_i h'
-        simp [Iter.IsPlausibleStep] at h
-        replace h := IterM.IsPlausibleNthOutputStep.zero_yield h
-        cases IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h h'
-      · rename_i h'
-        simp [Iter.IsPlausibleStep] at h
-        replace h := IterM.IsPlausibleNthOutputStep.zero_yield h
-        cases IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h h'
-    case yield_succ it it' _ h _ =>
-      rw [atIdxSlow?_eq_match, atIdxSlow?_eq_match]
+private theorem atIdxSlow?_eq_of_nextAtIdxSlow? [Iterator α Id β] [Productive α Id]
+    {it : Iter (α := α) β} {i : Nat} :
+    it.atIdxSlow? i = match (it.nextAtIdxSlow? i).val with
+    | .yield _ out => some out
+    | .skip _ => none
+    | .done => none := by
+  induction i, it using Iter.atIdxSlow?.induct_unfolding with
+  | yield_zero it it' out hp hs =>
+    rw [nextAtIdxSlow?_eq_match]; simp [hs]
+  | yield_succ it it' out hp hs k ih =>
+    rw [nextAtIdxSlow?_eq_match]; simp [hs, ih]
+  | skip_case n it it' hp hs ih =>
+    rw [nextAtIdxSlow?_eq_match]; simp [hs, ih]
+  | done_case n it hp hs =>
+    rw [nextAtIdxSlow?_eq_match]; simp [hs]
 
-  generalize h : Iter.Intermediate.stepSize it i n = sit
-  induction k, sit using Iter.atIdxSlow?.induct_unfolding
-  case yield_zero =>
-    simp
-    simp [Intermediate.stepSize, IterM.Intermediate.stepSize] at h
+private theorem atIdxSlow?_none_of_nextAtIdxSlow?_done [Iterator α Id β] [Productive α Id]
+    {it : Iter (α := α) β} {i j : Nat}
+    (h : (it.nextAtIdxSlow? i).val = .done) (hij : i ≤ j) :
+    it.atIdxSlow? j = none := by
+  induction j generalizing it i with
+  | zero =>
+    have : i = 0 := Nat.le_antisymm hij (Nat.zero_le _)
+    subst this; rw [atIdxSlow?_eq_of_nextAtIdxSlow?, h]
+  | succ j ih =>
+    suffices ∀ (it : Iter (α := α) β), (it.nextAtIdxSlow? i).val = .done →
+        it.atIdxSlow? (j + 1) = none from this it h
+    intro it h
+    induction it using Iter.inductSkips with | step it ih_skip
+    rw [atIdxSlow?_eq_match]
+    cases hstep : it.step using PlausibleIterStep.casesOn with
+    | yield it' out hp =>
+      rw [nextAtIdxSlow?_eq_match] at h; simp [hstep] at h
+      cases i with
+      | zero => cases h
+      | succ i => exact ih h (Nat.le_of_succ_le_succ hij)
+    | skip it' hp =>
+      rw [nextAtIdxSlow?_eq_match] at h; simp [hstep] at h
+      exact ih_skip hp h
+    | done hp => simp
 
-theorem atIdxSlow?_stepSize [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
-    [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
+private theorem atIdxSlow?_succ_of_nextAtIdxSlow?_yield [Iterator α Id β] [Productive α Id]
+    {it it' : Iter (α := α) β} {i j : Nat} {out : β}
+    (h : (it.nextAtIdxSlow? i).val = .yield it' out) :
+    it.atIdxSlow? (i + 1 + j) = it'.atIdxSlow? j := by
+  induction i, it using Iter.atIdxSlow?.induct_unfolding generalizing j with
+  | yield_zero it it'' out' hp hs =>
+    rw [nextAtIdxSlow?_eq_match] at h; simp [hs] at h
+    obtain ⟨rfl, rfl⟩ := h
+    show atIdxSlow? (0 + 1 + j) it = atIdxSlow? j it''
+    rw [show (0 : Nat) + 1 + j = Nat.succ j from by omega, atIdxSlow?_eq_match]
+    simp [hs]
+  | yield_succ it it'' out' hp hs k ih =>
+    rw [nextAtIdxSlow?_eq_match] at h; simp [hs] at h
+    show atIdxSlow? (k + 1 + 1 + j) it = atIdxSlow? j it'
+    rw [show k + 1 + 1 + j = Nat.succ (k + 1 + j) from by omega, atIdxSlow?_eq_match]
+    simp [hs]
+    exact ih h
+  | skip_case n it it'' hp hs ih =>
+    rw [nextAtIdxSlow?_eq_match] at h; simp [hs] at h
+    rw [atIdxSlow?_eq_match]; simp [hs]
+    exact ih h
+  | done_case n it hp hs =>
+    rw [nextAtIdxSlow?_eq_match] at h; simp [hs] at h
+
+private theorem nextAtIdxSlow?_zero_intermediate_stepSize_val [Iterator α Id β] [Productive α Id]
+    [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {i n : Nat} :
+    ((Intermediate.stepSize it i n).nextAtIdxSlow? 0).val =
+      (it.nextAtIdxSlow? i).val.mapIterator (fun it' => Intermediate.stepSize it' (n - 1) n) := by
+  have h := congrArg Subtype.val (nextAtIdxSlow?_zero_intermediate_stepSize (it := it) (i := i) (n := n))
+  simp only at h
+  rw [h]
+  cases (it.nextAtIdxSlow? i) using PlausibleIterStep.casesOn with
+  | yield => simp [IterStep.mapIterator]
+  | skip _ h => exact IterM.not_isPlausibleNthOutputStep_skip.elim h
+  | done => simp [IterStep.mapIterator]
+
+theorem atIdxSlow?_intermediate_stepSize [Iterator α Id β] [Productive α Id]
+    [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {i k n : Nat} :
+    (Intermediate.stepSize it i n).atIdxSlow? k = it.atIdxSlow? (i + (n - 1 + 1) * k) := by
+  induction k generalizing it i with
+  | zero =>
+    simp only [Nat.mul_zero, Nat.add_zero]
+    rw [atIdxSlow?_eq_of_nextAtIdxSlow?, nextAtIdxSlow?_zero_intermediate_stepSize_val]
+    rw [atIdxSlow?_eq_of_nextAtIdxSlow?]
+    cases (it.nextAtIdxSlow? i).val with
+    | yield => simp [IterStep.mapIterator]
+    | skip => simp [IterStep.mapIterator]
+    | done => simp [IterStep.mapIterator]
+  | succ k ih =>
+    cases hstep : (it.nextAtIdxSlow? i).val with
+    | yield it' out =>
+      have hss : ((Intermediate.stepSize it i n).nextAtIdxSlow? 0).val =
+          .yield (Intermediate.stepSize it' (n - 1) n) out := by
+        rw [nextAtIdxSlow?_zero_intermediate_stepSize_val, hstep]; rfl
+      have h1 : (Intermediate.stepSize it i n).atIdxSlow? (0 + 1 + k) =
+          (Intermediate.stepSize it' (n - 1) n).atIdxSlow? k :=
+        atIdxSlow?_succ_of_nextAtIdxSlow?_yield hss
+      have h2 : (Intermediate.stepSize it i n).atIdxSlow? (k + 1) =
+          (Intermediate.stepSize it i n).atIdxSlow? (0 + 1 + k) := by
+        congr 1; omega
+      have h3 : it.atIdxSlow? (i + 1 + ((n - 1) + (n - 1 + 1) * k)) =
+          it'.atIdxSlow? ((n - 1) + (n - 1 + 1) * k) :=
+        atIdxSlow?_succ_of_nextAtIdxSlow?_yield hstep
+      have h4 : i + (n - 1 + 1) * (k + 1) = i + 1 + ((n - 1) + (n - 1 + 1) * k) := by
+        rw [Nat.mul_succ]; omega
+      rw [h2, h1, ih, ← h3, h4]
+    | skip it' =>
+      exfalso
+      have := (it.nextAtIdxSlow? i).property
+      rw [hstep] at this
+      exact IterM.not_isPlausibleNthOutputStep_skip this
+    | done =>
+      have hss : ((Intermediate.stepSize it i n).nextAtIdxSlow? 0).val = .done := by
+        rw [nextAtIdxSlow?_zero_intermediate_stepSize_val, hstep]; rfl
+      rw [atIdxSlow?_none_of_nextAtIdxSlow?_done hss (by omega)]
+      exact (atIdxSlow?_none_of_nextAtIdxSlow?_done hstep (by omega)).symm
+
+theorem atIdxSlow?_stepSize [Iterator α Id β] [Productive α Id]
+    [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {k n : Nat} :
     (it.stepSize n).atIdxSlow? k = it.atIdxSlow? ((n - 1 + 1) * k) := by
+  show (Intermediate.stepSize it 0 n).atIdxSlow? k = _
+  rw [atIdxSlow?_intermediate_stepSize]; simp
 
+theorem getElem?_toList_stepSize [Iterator α Id β] [Productive α Id]
+    [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] [Finite α Id]
+    {it : Iter (α := α) β} {k n : Nat} :
+    (it.stepSize n).toList[k]? = it.toList[(n - 1 + 1) * k]? := by
+  simp only [getElem?_toList_eq_atIdxSlow?, atIdxSlow?_stepSize]
 
 end Std.Iter

From 2d31b9edcfd10d353256dc80b8ddf272f748c91e Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sat, 28 Feb 2026 23:56:18 +0000
Subject: [PATCH 04/18] feat: add length_stepSize theorem for stepSize iterator

This PR adds a theorem proving that the length of a stepSize iterator
relates to the original iterator's length via ceiling division:
`(it.stepSize n).length = (it.length + (n - 1)) / (n - 1 + 1)`.

Also adds the generalized intermediate version `length_intermediate_stepSize`
and supporting helper lemmas connecting `nextAtIdxSlow?` results to length
bounds.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .../Lemmas/Combinators/StepSize.lean          | 135 ++++++++++++++++++
 1 file changed, 135 insertions(+)

diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
index 3b32ff2e765b..1ff7f2b76573 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -15,6 +15,7 @@ import Init.Data.Iterators.Lemmas.Basic
 import Init.Omega
 import Init.Data.Iterators.Lemmas.Consumers.Access
 import Init.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Loop
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Access
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 import Init.Data.Iterators.Lemmas.Monadic.Basic
@@ -383,4 +384,138 @@ theorem getElem?_toList_stepSize [Iterator α Id β] [Productive α Id]
     (it.stepSize n).toList[k]? = it.toList[(n - 1 + 1) * k]? := by
   simp only [getElem?_toList_eq_atIdxSlow?, atIdxSlow?_stepSize]
 
+private theorem step_eq_nextAtIdxSlow?_zero_val [Iterator α Id β] [Productive α Id]
+    {it : Iter (α := α) β} :
+    (∀ (it' : Iter (α := α) β), ¬ it.IsPlausibleStep (.skip it')) →
+    it.step.val = (it.nextAtIdxSlow? 0).val := by
+  intro hno_skip
+  rw [nextAtIdxSlow?_eq_match]
+  cases it.step using PlausibleIterStep.casesOn with
+  | yield => simp
+  | skip _ hp => exact absurd hp (hno_skip _)
+  | done => simp
+
+private theorem not_isPlausibleStep_skip_intermediate_stepSize [Iterator α Id β]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {i n : Nat}
+    {it' : Iter (α := Types.StepSizeIterator α Id β) β} :
+    ¬ (Intermediate.stepSize it i n).IsPlausibleStep (.skip it') := by
+  simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+    IterStep.mapIterator, Intermediate.stepSize, IterM.Intermediate.stepSize]
+  intro ⟨h, _⟩
+  exact IterM.not_isPlausibleNthOutputStep_skip h
+
+private theorem step_intermediate_stepSize_val [Iterator α Id β] [Productive α Id]
+    [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {i n : Nat} :
+    (Intermediate.stepSize it i n).step.val =
+      (it.nextAtIdxSlow? i).val.mapIterator (fun it' => Intermediate.stepSize it' (n - 1) n) := by
+  rw [step_eq_nextAtIdxSlow?_zero_val (fun _ => not_isPlausibleStep_skip_intermediate_stepSize),
+    nextAtIdxSlow?_zero_intermediate_stepSize_val]
+
+private theorem lt_length_of_nextAtIdxSlow?_yield [Iterator α Id β] [Finite α Id]
+    [Productive α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it it' : Iter (α := α) β} {i : Nat} {out : β}
+    (h : (it.nextAtIdxSlow? i).val = .yield it' out) :
+    i < it.length := by
+  induction it using Iter.inductSteps generalizing i it' out with
+  | step it ihy ihs =>
+    rw [Std.Iter.length_eq_match_step]
+    rw [nextAtIdxSlow?_eq_match] at h
+    cases hstep : it.step using PlausibleIterStep.casesOn with
+    | yield it'' out'' hp =>
+      simp only [hstep] at h
+      simp only
+      cases i with
+      | zero => omega
+      | succ k =>
+        simp only at h
+        exact Nat.succ_lt_succ (ihy hp h)
+    | skip it'' hp =>
+      simp only [hstep] at h
+      simp only
+      exact ihs hp h
+    | done hp =>
+      simp [hstep] at h
+
+private theorem length_le_of_nextAtIdxSlow?_done [Iterator α Id β] [Finite α Id]
+    [Productive α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {i : Nat}
+    (h : (it.nextAtIdxSlow? i).val = .done) :
+    it.length ≤ i := by
+  induction it using Iter.inductSteps generalizing i with
+  | step it ihy ihs =>
+    rw [Std.Iter.length_eq_match_step]
+    rw [nextAtIdxSlow?_eq_match] at h
+    cases hstep : it.step using PlausibleIterStep.casesOn with
+    | yield it'' out'' hp =>
+      simp only [hstep] at h
+      simp only
+      cases i with
+      | zero => simp at h
+      | succ k =>
+        simp only at h
+        have := ihy hp h
+        omega
+    | skip it'' hp =>
+      simp only [hstep] at h
+      simp only
+      have := ihs hp h
+      omega
+    | done hp =>
+      simp only
+      omega
+
+theorem length_intermediate_stepSize [Iterator α Id β] [Finite α Id]
+    [Productive α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {i n : Nat} :
+    (Intermediate.stepSize it i n).length = (it.length + (n - 1) - i) / (n - 1 + 1) := by
+  suffices ∀ (oit : Iter (α := Types.StepSizeIterator α Id β) β)
+      (it : Iter (α := α) β) (i : Nat),
+      oit = Intermediate.stepSize it i n →
+      oit.length = (it.length + (n - 1) - i) / (n - 1 + 1) from
+    this _ _ _ rfl
+  intro oit
+  induction oit using Iter.inductSteps with
+  | step oit ih_yield ih_skip =>
+    intro it i hoit
+    rw [Std.Iter.length_eq_match_step]
+    subst hoit
+    rw [step_intermediate_stepSize_val]
+    cases h : (it.nextAtIdxSlow? i) using PlausibleIterStep.casesOn with
+    | yield it' out hp =>
+      simp only [IterStep.mapIterator]
+      have hstep : (Intermediate.stepSize it i n).step.val =
+          .yield (Intermediate.stepSize it' (n - 1) n) out := by
+        rw [step_intermediate_stepSize_val, h]; rfl
+      have hps : (Intermediate.stepSize it i n).IsPlausibleStep
+          (.yield (Intermediate.stepSize it' (n - 1) n) out) := by
+        rw [← hstep]; exact (Intermediate.stepSize it i n).step.property
+      rw [ih_yield hps it' (n - 1) rfl]
+      have hlength := length_nextAtIdxSlow? (it := it) (n := i)
+      rw [h] at hlength
+      simp only at hlength
+      rw [hlength]
+      have hi := lt_length_of_nextAtIdxSlow?_yield (by rw [h])
+      have h1 : it.length - i - 1 + (n - 1) - (n - 1) = it.length - i - 1 := by omega
+      rw [h1, ← Nat.add_div_right (it.length - i - 1) (by omega : 0 < n - 1 + 1)]
+      congr 1
+      omega
+    | skip _ hp => exact IterM.not_isPlausibleNthOutputStep_skip.elim hp
+    | done hp =>
+      simp only [IterStep.mapIterator]
+      have hi := length_le_of_nextAtIdxSlow?_done (by rw [h])
+      symm
+      apply Nat.div_eq_of_lt
+      omega
+
+theorem length_stepSize [Iterator α Id β] [Finite α Id]
+    [Productive α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {n : Nat} :
+    (it.stepSize n).length = (it.length + (n - 1)) / (n - 1 + 1) := by
+  show (Intermediate.stepSize it 0 n).length = _
+  rw [length_intermediate_stepSize]
+  simp
+
 end Std.Iter

From b877dd6cbf4d83c0a29d55826305e653f02e8184 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 00:22:21 +0000
Subject: [PATCH 05/18] feat: add LawfulDeterministicIterator instance for
 stepSize iterator

This PR provides a LawfulDeterministicIterator instance for
StepSizeIterator, proving that the stepSize combinator preserves
determinism when the base iterator is deterministic. Also removes
commented-out code from previous incomplete attempts.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .../Lemmas/Combinators/Monadic/StepSize.lean  | 14 -----
 .../Lemmas/Combinators/StepSize.lean          | 52 ++++++++++++++-----
 2 files changed, 38 insertions(+), 28 deletions(-)

diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean
index 281abf497292..9eddfd7bd5a9 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean
@@ -13,19 +13,5 @@ open Std Std.Iterators Std.Iterators.Types
 
 namespace Std.IterM
 
--- example [Iterator α Id β] [IteratorAccess α Id] [LawfulDeterministicIterator α Id] :
---     Productive α Id where
---   wf := by
---     constructor
---     intro it
---     have :=
-
--- instance [Iterator α m β] [LawfulDeterministicIterator α m] [IteratorAccess α m] [Monad m] :
---     LawfulDeterministicIterator (StepSizeIterator α m β) m where
---   isPlausibleStep_eq_eq it := by
---     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, funext_iff]
---     obtain ⟨⟨
-
--- theorem step_stepSize
 
 end Std.IterM
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
index 1ff7f2b76573..11c83a2b7614 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -27,20 +27,6 @@ open Std Std.Iterators Std.Iterators.Types
 
 namespace Std.Iter
 
--- example [Iterator α Id β] [IteratorAccess α Id] [LawfulDeterministicIterator α Id] :
---     Productive α Id where
---   wf := by
---     constructor
---     intro it
---     have :=
-
--- instance [Iterator α m β] [LawfulDeterministicIterator α m] [IteratorAccess α m] [Monad m] :
---     LawfulDeterministicIterator (StepSizeIterator α m β) m where
---   isPlausibleStep_eq_eq it := by
---     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, funext_iff]
---     obtain ⟨⟨
-
--- theorem step_stepSize
 
 instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α := α) Id β} :
     Subsingleton it.Step where
@@ -135,6 +121,44 @@ instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α
     have := IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep hs hs'
     rwa [Subtype.mk.injEq]
 
+instance instLawfulDeterministicIteratorStepSizeIterator
+    [Iterator α Id β] [LawfulDeterministicIterator α Id] [IteratorAccess α Id] :
+    LawfulDeterministicIterator (Types.StepSizeIterator α Id β) Id where
+  isPlausibleStep_eq_eq it := by
+    refine ⟨it.step.run.inflate.val, ?_⟩
+    have hp := it.step.run.inflate.property
+    ext step
+    constructor
+    · intro ⟨h1, h2⟩
+      obtain ⟨hp1, hp2⟩ := hp
+      have heq := IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h1 hp1
+      generalize it.step.run.inflate.val = cstep at heq hp1 hp2 ⊢
+      cases step with
+      | skip _ =>
+        exfalso; simp only [IterStep.mapIterator] at h1
+        exact IterM.not_isPlausibleNthOutputStep_skip h1
+      | done =>
+        cases cstep with
+        | done => rfl
+        | yield _ _ => simp [IterStep.mapIterator] at heq
+        | skip _ =>
+          exfalso; simp only [IterStep.mapIterator] at hp1
+          exact IterM.not_isPlausibleNthOutputStep_skip hp1
+      | yield it₁ out₁ =>
+        cases cstep with
+        | done => simp [IterStep.mapIterator] at heq
+        | skip _ =>
+          exfalso; simp only [IterStep.mapIterator] at hp1
+          exact IterM.not_isPlausibleNthOutputStep_skip hp1
+        | yield it₂ out₂ =>
+          simp only [IterStep.mapIterator, IterStep.yield.injEq, Function.comp_apply] at heq
+          obtain ⟨hinner, rfl⟩ := heq
+          congr 1
+          obtain ⟨hn₁, hi₁⟩ := h2 _ _ rfl
+          obtain ⟨hn₂, hi₂⟩ := hp2 _ _ rfl
+          rcases it₁ with ⟨⟨_, _, _⟩⟩; rcases it₂ with ⟨⟨_, _, _⟩⟩; simp_all
+    · rintro rfl; exact hp
+
 theorem _root_.Std.IterM.nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
     it.nextAtIdx? n = it.nextAtIdxSlow? n := by

From 25e12fa62fe0a118c5bd6864dd65bf033f2019f3 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 13:58:25 +0100
Subject: [PATCH 06/18] wip

---
 .../Lemmas/Combinators/StepSize.lean          | 246 +++++++-----------
 1 file changed, 101 insertions(+), 145 deletions(-)

diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
index 11c83a2b7614..1a2f5adebc52 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -49,13 +49,13 @@ instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : Iter (α
     rw [IterStep.mapIterator_inj (fun _ _ => toIterM_inj.mp) ] at this
     rwa [Subtype.mk.injEq]
 
-theorem eq_step_of_isPlausibleStep [Iterator α Id β] [LawfulDeterministicIterator α Id]
+theorem IsPlausibleStep.eq_step [Iterator α Id β] [LawfulDeterministicIterator α Id]
     {it : Iter (α := α) β} {step} (h : it.IsPlausibleStep step) :
     step = it.step.val := by
   have : ⟨step, h⟩ = it.step := Subsingleton.allEq _ _
   simp [← this]
 
-theorem _root_.Std.IterM.eq_step_of_isPlausibleStep [Iterator α Id β] [LawfulDeterministicIterator α Id]
+theorem _root_.Std.IterM.IsPlausibleStep.eq_step [Iterator α Id β] [LawfulDeterministicIterator α Id]
     {it : IterM (α := α) Id β} {step} (h : it.IsPlausibleStep step) :
     step = it.step.run.inflate.val := by
   have : ⟨step, h⟩ = it.step.run.inflate := Subsingleton.allEq _ _
@@ -73,45 +73,39 @@ theorem _root_.Std.IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputS
     | .zero_yield h' ..
     | .skip h' ..
     | .done h' =>
-      replace h := IterM.eq_step_of_isPlausibleStep h
-      replace h' := IterM.eq_step_of_isPlausibleStep h'
-      rw [← h] at h'
+      replace h' := h'.eq_step
+      rw [← h.eq_step] at h'
       cases h'
-      all_goals rfl
+      all_goals simp
   case done h =>
     match hs' with
     | .zero_yield h' ..
     | .yield h' ..
-    | .skip h' ..
-    | .done h' =>
-      replace h := IterM.eq_step_of_isPlausibleStep h
-      replace h' := IterM.eq_step_of_isPlausibleStep h'
+    | .skip h' .. =>
+      replace h := h.eq_step
+      replace h' := h'.eq_step
       rw [← h] at h'
-      all_goals cases h'
-      all_goals rfl
+      cases h'
+    | .done h' => simp
   case yield h _ ih =>
     match hs' with
     | .yield h' ..
     | .skip h' ..
     | .done h' =>
-      replace h := IterM.eq_step_of_isPlausibleStep h
-      replace h' := IterM.eq_step_of_isPlausibleStep h'
-      rw [← h] at h'
+      replace h' := h'.eq_step
+      rw [← h.eq_step] at h'
       cases h'
-      all_goals
-        apply ih ‹_›
+      all_goals apply ih ‹_›
   case skip h _ ih =>
     match hs' with
     | .zero_yield h' ..
     | .yield h' ..
     | .skip h' ..
     | .done h' =>
-      replace h := IterM.eq_step_of_isPlausibleStep h
-      replace h' := IterM.eq_step_of_isPlausibleStep h'
-      rw [← h] at h'
+      replace h' := h'.eq_step
+      rw [← h.eq_step] at h'
       cases h'
-      all_goals
-        apply ih ‹_›
+      all_goals apply ih ‹_›
 
 instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α := α) Id β} :
     Subsingleton (PlausibleIterStep (it.IsPlausibleNthOutputStep n)) where
@@ -129,38 +123,30 @@ instance instLawfulDeterministicIteratorStepSizeIterator
     have hp := it.step.run.inflate.property
     ext step
     constructor
-    · intro ⟨h1, h2⟩
-      obtain ⟨hp1, hp2⟩ := hp
-      have heq := IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h1 hp1
-      generalize it.step.run.inflate.val = cstep at heq hp1 hp2 ⊢
+    · intro ⟨h₁, h₂⟩
+      obtain ⟨hp₁, hp₂⟩ := hp
+      simp only [IterStep.mapIterator] at h₁ hp₁
+      have heq := IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h₁ hp₁
+      generalize it.step.run.inflate.val = cstep at heq hp₁ hp₂ ⊢
       cases step with
-      | skip _ =>
-        exfalso; simp only [IterStep.mapIterator] at h1
-        exact IterM.not_isPlausibleNthOutputStep_skip h1
+      | skip _ => exact IterM.not_isPlausibleNthOutputStep_skip.elim (by simpa using h₁)
       | done =>
         cases cstep with
-        | done => rfl
-        | yield _ _ => simp [IterStep.mapIterator] at heq
-        | skip _ =>
-          exfalso; simp only [IterStep.mapIterator] at hp1
-          exact IterM.not_isPlausibleNthOutputStep_skip hp1
+        | done => simp
+        | yield _ _ => simp at heq
+        | skip _ => exact IterM.not_isPlausibleNthOutputStep_skip.elim (by simpa using hp₁)
       | yield it₁ out₁ =>
         cases cstep with
-        | done => simp [IterStep.mapIterator] at heq
-        | skip _ =>
-          exfalso; simp only [IterStep.mapIterator] at hp1
-          exact IterM.not_isPlausibleNthOutputStep_skip hp1
+        | done => simp at heq
+        | skip _ => exact IterM.not_isPlausibleNthOutputStep_skip.elim (by simpa using hp₁)
         | yield it₂ out₂ =>
-          simp only [IterStep.mapIterator, IterStep.yield.injEq, Function.comp_apply] at heq
-          obtain ⟨hinner, rfl⟩ := heq
-          congr 1
-          obtain ⟨hn₁, hi₁⟩ := h2 _ _ rfl
-          obtain ⟨hn₂, hi₂⟩ := hp2 _ _ rfl
-          rcases it₁ with ⟨⟨_, _, _⟩⟩; rcases it₂ with ⟨⟨_, _, _⟩⟩; simp_all
-    · rintro rfl; exact hp
-
-theorem _root_.Std.IterM.nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
-    [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
+          rcases it₁ with ⟨⟨_, _, _⟩⟩
+          rcases it₂ with ⟨⟨_, _, _⟩⟩
+          simp_all
+    · simp +contextual [hp]
+
+theorem _root_.Std.IterM.nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id]
+    [LawfulDeterministicIterator α Id] [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
     it.nextAtIdx? n = it.nextAtIdxSlow? n := by
   ext
   apply Subsingleton.allEq
@@ -177,24 +163,29 @@ theorem _root_.Std.IterM.nextAtIdxSlow?_stepSize_aux [Iterator α Id β] [Produc
       | .yield it' out h =>
         return .yield (IterM.Intermediate.stepSize it' (n - 1) n) out (by
           refine .zero_yield ?_
-          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-            IterM.Intermediate.stepSize, IterM.Intermediate.stepSize])
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, IterM.Intermediate.stepSize,
+            IterM.Intermediate.stepSize])
       | .skip it' h => return IterM.not_isPlausibleNthOutputStep_skip.elim h
       | .done h =>
         return .done (by
           refine .done ?_
-          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-            Intermediate.stepSize, IterM.Intermediate.stepSize])) := by
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Intermediate.stepSize,
+            IterM.Intermediate.stepSize])) := by
   induction it, i using IterM.atIdxSlow?.induct_unfolding
-  simp [IterM.Intermediate.stepSize]
   rw [IterM.nextAtIdxSlow?_eq_match]
-  simp [IterM.step_eq, IterM.nextAtIdx?_eq_nextAtIdxSlow?]
+  simp only [IterM.Intermediate.stepSize, IterM.step_eq, IterM.internalState_mk,
+    IterM.nextAtIdx?_eq_nextAtIdxSlow?, bind_pure_comp, bind_map_left, Shrink.inflate_deflate]
   apply bind_congr; intro step
   cases step using PlausibleIterStep.casesOn
   · simp
   · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
   · simp
 
+@[simp]
+theorem Not.elim_eq {hP : P} {hnP : ¬ P} :
+    hnP.elim hP = x ↔ True :=
+  hnP.elim hP
+
 theorem _root_.Std.IterM.length_nextAtIdxSlow? [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} :
     (do match ← it.nextAtIdxSlow? n with
@@ -206,29 +197,20 @@ theorem _root_.Std.IterM.length_nextAtIdxSlow? [Monad m] [LawfulMonad m] [Iterat
   simp only [map_eq_pure_bind, bind_assoc]
   apply bind_congr; intro step
   cases step.inflate using PlausibleIterStep.casesOn
-  · simp
+  · simp only [bind_pure_comp, Functor.map_map]
     split
-    · simp
-    · rename_i it' out h n n'
-      simp
-      refine Eq.trans ?_ ((ihy h (n := n')).trans ?_)
-      · apply bind_congr; intro step
-        cases step using PlausibleIterStep.casesOn
-        · simp
-        · rfl
-        · simp
-      · simp [Nat.add_sub_add_right]
-  · rename_i it' h n _ h
-    simp
-    refine Eq.trans ?_ ((ihs h (n := n)).trans ?_)
-    · apply bind_congr; intro step
-      cases step using PlausibleIterStep.casesOn
-      · simp
-      · rfl
-      · simp
-    · simp
+    · simp only [pure_bind, Nat.sub_zero, Nat.add_one_sub_one, id_map']
+    · simp only [Nat.succ_eq_add_one, Nat.add_sub_add_right, bind_map_left]
+      rw [← ihy ‹_›]
+      apply bind_congr; intro step
+      cases step using PlausibleIterStep.casesOn <;> simp
+  · simp only [bind_pure_comp, bind_map_left, id_map']
+    rw [← ihs ‹_›]
+    apply bind_congr; intro step
+    cases step using PlausibleIterStep.casesOn <;> simp
   · simp
 
+-- TODO: rename
 theorem length_nextAtIdxSlow? [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β} :
     (match it.nextAtIdxSlow? n with
@@ -236,10 +218,9 @@ theorem length_nextAtIdxSlow? [Iterator α Id β] [Finite α Id] [IteratorLoop 
       | .skip _it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
       | .done _h => 0) = it.length - n - 1 := by
   have := IterM.length_nextAtIdxSlow? (it := it.toIterM) (n := n)
-  replace this := congrArg Id.run this
-  replace this := congrArg ULift.down this
-  simp at this
-  simp [Iter.length, ← this, Iter.nextAtIdxSlow?]
+  replace this := congrArg (fun x => ULift.down (Id.run x)) this
+  simp only [Id.run_bind, Id.run_map] at this
+  simp only [nextAtIdxSlow?, length, ← this]
   split at this
   · simp [*]
   · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
@@ -261,18 +242,14 @@ theorem nextAtIdxSlow?_zero_intermediate_stepSize [Iterator α Id β] [Productiv
           refine .done ?_
           simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
             Intermediate.stepSize, IterM.Intermediate.stepSize]) := by
-  simp only [Iter.nextAtIdxSlow?]
-  simp only [Intermediate.stepSize, toIterM_toIter, IterM.nextAtIdxSlow?_stepSize_aux]
-  simp
+  simp only [Iter.nextAtIdxSlow?, Intermediate.stepSize, toIterM_toIter,
+    IterM.nextAtIdxSlow?_stepSize_aux, Id.run_bind]
   apply Subtype.ext
-  simp
   let step := (it.toIterM.nextAtIdxSlow? i).run
   cases hs : step using PlausibleIterStep.casesOn
-  · simp [show (it.toIterM.nextAtIdxSlow? i).run = step from rfl]
-    simp [hs]
+  · simp [hs, step]
   · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
-  · simp [show (it.toIterM.nextAtIdxSlow? i).run = step from rfl]
-    simp [hs]
+  · simp [hs, step]
 
 private theorem atIdxSlow?_eq_of_nextAtIdxSlow? [Iterator α Id β] [Productive α Id]
     {it : Iter (α := α) β} {i : Nat} :
@@ -280,15 +257,8 @@ private theorem atIdxSlow?_eq_of_nextAtIdxSlow? [Iterator α Id β] [Productive
     | .yield _ out => some out
     | .skip _ => none
     | .done => none := by
-  induction i, it using Iter.atIdxSlow?.induct_unfolding with
-  | yield_zero it it' out hp hs =>
-    rw [nextAtIdxSlow?_eq_match]; simp [hs]
-  | yield_succ it it' out hp hs k ih =>
-    rw [nextAtIdxSlow?_eq_match]; simp [hs, ih]
-  | skip_case n it it' hp hs ih =>
-    rw [nextAtIdxSlow?_eq_match]; simp [hs, ih]
-  | done_case n it hp hs =>
-    rw [nextAtIdxSlow?_eq_match]; simp [hs]
+  induction i, it using Iter.atIdxSlow?.induct_unfolding <;>
+    (rw [nextAtIdxSlow?_eq_match]; simp [*])
 
 private theorem atIdxSlow?_none_of_nextAtIdxSlow?_done [Iterator α Id β] [Productive α Id]
     {it : Iter (α := α) β} {i j : Nat}
@@ -296,22 +266,21 @@ private theorem atIdxSlow?_none_of_nextAtIdxSlow?_done [Iterator α Id β] [Prod
     it.atIdxSlow? j = none := by
   induction j generalizing it i with
   | zero =>
-    have : i = 0 := Nat.le_antisymm hij (Nat.zero_le _)
-    subst this; rw [atIdxSlow?_eq_of_nextAtIdxSlow?, h]
+    cases show i = 0 from Nat.le_antisymm hij (Nat.zero_le _)
+    rw [atIdxSlow?_eq_of_nextAtIdxSlow?, h]
   | succ j ih =>
-    suffices ∀ (it : Iter (α := α) β), (it.nextAtIdxSlow? i).val = .done →
-        it.atIdxSlow? (j + 1) = none from this it h
-    intro it h
     induction it using Iter.inductSkips with | step it ih_skip
     rw [atIdxSlow?_eq_match]
     cases hstep : it.step using PlausibleIterStep.casesOn with
     | yield it' out hp =>
-      rw [nextAtIdxSlow?_eq_match] at h; simp [hstep] at h
+      rw [nextAtIdxSlow?_eq_match] at h
+      simp only [hstep, PlausibleIterStep.yield] at h
       cases i with
       | zero => cases h
       | succ i => exact ih h (Nat.le_of_succ_le_succ hij)
     | skip it' hp =>
-      rw [nextAtIdxSlow?_eq_match] at h; simp [hstep] at h
+      rw [nextAtIdxSlow?_eq_match] at h
+      simp only [hstep] at h
       exact ih_skip hp h
     | done hp => simp
 
@@ -321,21 +290,20 @@ private theorem atIdxSlow?_succ_of_nextAtIdxSlow?_yield [Iterator α Id β] [Pro
     it.atIdxSlow? (i + 1 + j) = it'.atIdxSlow? j := by
   induction i, it using Iter.atIdxSlow?.induct_unfolding generalizing j with
   | yield_zero it it'' out' hp hs =>
-    rw [nextAtIdxSlow?_eq_match] at h; simp [hs] at h
+    rw [nextAtIdxSlow?_eq_match] at h
+    simp only [hs, PlausibleIterStep.yield, IterStep.yield.injEq] at h
     obtain ⟨rfl, rfl⟩ := h
     show atIdxSlow? (0 + 1 + j) it = atIdxSlow? j it''
-    rw [show (0 : Nat) + 1 + j = Nat.succ j from by omega, atIdxSlow?_eq_match]
+    rw [show (0 : Nat) + 1 + j = j + 1 from by omega, atIdxSlow?_eq_match]
     simp [hs]
   | yield_succ it it'' out' hp hs k ih =>
-    rw [nextAtIdxSlow?_eq_match] at h; simp [hs] at h
-    show atIdxSlow? (k + 1 + 1 + j) it = atIdxSlow? j it'
-    rw [show k + 1 + 1 + j = Nat.succ (k + 1 + j) from by omega, atIdxSlow?_eq_match]
-    simp [hs]
-    exact ih h
+    rw [nextAtIdxSlow?_eq_match, Nat.succ_eq_add_one, hs] at h
+    rw [show k + 1 + 1 + j = (k + 1 + j) + 1 from by omega, atIdxSlow?_eq_match]
+    simpa [hs] using ih h
   | skip_case n it it'' hp hs ih =>
-    rw [nextAtIdxSlow?_eq_match] at h; simp [hs] at h
-    rw [atIdxSlow?_eq_match]; simp [hs]
-    exact ih h
+    rw [nextAtIdxSlow?_eq_match, hs] at h
+    rw [atIdxSlow?_eq_match, hs]
+    simpa using ih h
   | done_case n it hp hs =>
     rw [nextAtIdxSlow?_eq_match] at h; simp [hs] at h
 
@@ -489,57 +457,45 @@ private theorem length_le_of_nextAtIdxSlow?_done [Iterator α Id β] [Finite α
       simp only
       omega
 
-theorem length_intermediate_stepSize [Iterator α Id β] [Finite α Id]
+theorem Intermediate.length_stepSize [Iterator α Id β] [Finite α Id]
     [Productive α Id] [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β} {i n : Nat} :
     (Intermediate.stepSize it i n).length = (it.length + (n - 1) - i) / (n - 1 + 1) := by
-  suffices ∀ (oit : Iter (α := Types.StepSizeIterator α Id β) β)
-      (it : Iter (α := α) β) (i : Nat),
-      oit = Intermediate.stepSize it i n →
-      oit.length = (it.length + (n - 1) - i) / (n - 1 + 1) from
-    this _ _ _ rfl
-  intro oit
-  induction oit using Iter.inductSteps with
+  generalize hsit : Intermediate.stepSize it i n = sit
+  replace hsit := hsit.symm
+  induction sit using Iter.inductSteps generalizing it i with
   | step oit ih_yield ih_skip =>
-    intro it i hoit
     rw [Std.Iter.length_eq_match_step]
-    subst hoit
+    subst hsit
     rw [step_intermediate_stepSize_val]
     cases h : (it.nextAtIdxSlow? i) using PlausibleIterStep.casesOn with
     | yield it' out hp =>
       simp only [IterStep.mapIterator]
-      have hstep : (Intermediate.stepSize it i n).step.val =
-          .yield (Intermediate.stepSize it' (n - 1) n) out := by
-        rw [step_intermediate_stepSize_val, h]; rfl
-      have hps : (Intermediate.stepSize it i n).IsPlausibleStep
-          (.yield (Intermediate.stepSize it' (n - 1) n) out) := by
-        rw [← hstep]; exact (Intermediate.stepSize it i n).step.property
-      rw [ih_yield hps it' (n - 1) rfl]
-      have hlength := length_nextAtIdxSlow? (it := it) (n := i)
-      rw [h] at hlength
-      simp only at hlength
-      rw [hlength]
-      have hi := lt_length_of_nextAtIdxSlow?_yield (by rw [h])
-      have h1 : it.length - i - 1 + (n - 1) - (n - 1) = it.length - i - 1 := by omega
-      rw [h1, ← Nat.add_div_right (it.length - i - 1) (by omega : 0 < n - 1 + 1)]
-      congr 1
-      omega
+      rw [ih_yield (it := it') (i := n - 1) (out := out) _ rfl]
+      · have hlength := length_nextAtIdxSlow? (it := it) (n := i)
+        simp only [h] at hlength
+        simp only [hlength, Nat.add_sub_cancel, Nat.zero_lt_succ, ← Nat.add_div_right]
+        have hi := lt_length_of_nextAtIdxSlow?_yield (by rw [h])
+        congr 1; omega
+      · have := (Intermediate.stepSize it i n).step.property
+        simpa [step_intermediate_stepSize_val, h, IterStep.mapIterator]
     | skip _ hp => exact IterM.not_isPlausibleNthOutputStep_skip.elim hp
     | done hp =>
       simp only [IterStep.mapIterator]
+      apply Nat.div_eq_of_lt _ |>.symm
       have hi := length_le_of_nextAtIdxSlow?_done (by rw [h])
-      symm
-      apply Nat.div_eq_of_lt
       omega
 
-theorem length_stepSize [Iterator α Id β] [Finite α Id]
-    [Productive α Id] [LawfulDeterministicIterator α Id]
+theorem stepSize_eq_intermediateStepSize [Iterator α Id β] [IteratorAccess α Id]
+    {it : Iter (α := α) β} {n : Nat} :
+    it.stepSize n = Intermediate.stepSize it 0 n :=
+  rfl
+
+theorem length_stepSize [Iterator α Id β] [Finite α Id] [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β} {n : Nat} :
     (it.stepSize n).length = (it.length + (n - 1)) / (n - 1 + 1) := by
-  show (Intermediate.stepSize it 0 n).length = _
-  rw [length_intermediate_stepSize]
-  simp
+  simp [stepSize_eq_intermediateStepSize, Intermediate.length_stepSize]
 
 end Std.Iter

From 713b8c4bb37c20b6be8334fedb7a54c7036fcebb Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 16:39:31 +0100
Subject: [PATCH 07/18] cleanups

---
 src/Init/Data/Iterators/Lemmas/Basic.lean     |  27 +-
 .../Iterators/Lemmas/Consumers/Access.lean    |  51 ++++
 .../Lemmas/Consumers/Monadic/Access.lean      |   2 +-
 .../Data/Iterators/Lemmas/Monadic/Basic.lean  |  26 +-
 .../Lemmas/Combinators/StepSize.lean          | 243 +++++-------------
 .../Iterators/Producers/Monadic/Array.lean    |   6 +-
 6 files changed, 169 insertions(+), 186 deletions(-)

diff --git a/src/Init/Data/Iterators/Lemmas/Basic.lean b/src/Init/Data/Iterators/Lemmas/Basic.lean
index 1e19f181e11e..ab94647ed3b5 100644
--- a/src/Init/Data/Iterators/Lemmas/Basic.lean
+++ b/src/Init/Data/Iterators/Lemmas/Basic.lean
@@ -7,10 +7,11 @@ module
 
 prelude
 public import Init.Data.Iterators.Basic
+public import Init.RCases
 
 public section
 
-namespace Std
+namespace Std.Iter
 open Std.Iterators
 
 /--
@@ -19,7 +20,7 @@ iterator `it` to an element of `motive it` by defining `f it` in terms of the va
 the plausible successors of `it'.
 -/
 @[specialize]
-def Iter.inductSteps {α β} [Iterator α Id β] [Finite α Id]
+def inductSteps {α β} [Iterator α Id β] [Finite α Id]
   (motive : Iter (α := α) β → Sort x)
   (step : (it : Iter (α := α) β) →
     (ih_yield : ∀ {it' : Iter (α := α) β} {out : β},
@@ -38,7 +39,7 @@ iterator `it` to an element of `motive it` by defining `f it` in terms of the va
 the plausible skip successors of `it'.
 -/
 @[specialize]
-def Iter.inductSkips {α β} [Iterator α Id β] [Productive α Id]
+def inductSkips {α β} [Iterator α Id β] [Productive α Id]
   (motive : Iter (α := α) β → Sort x)
   (step : (it : Iter (α := α) β) →
     (ih_skip : ∀ {it' : Iter (α := α) β}, it.IsPlausibleStep (.skip it') → motive it') →
@@ -47,4 +48,22 @@ def Iter.inductSkips {α β} [Iterator α Id β] [Productive α Id]
   step it (fun {it'} _ => inductSkips motive step it')
 termination_by it.finitelyManySkips
 
-end Std
+-- Not a real instance because the discrimination key would be to indiscriminate.
+local instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : Iter (α := α) β} :
+    Subsingleton it.Step where
+  allEq s s' := by
+    obtain ⟨s'', hs''⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq it.toIterM
+    obtain ⟨s, hs⟩ := s
+    obtain ⟨s', hs'⟩ := s'
+    simp only [Iter.IsPlausibleStep, hs''] at hs hs'
+    have := hs.trans hs'.symm
+    rw [IterStep.mapIterator_inj (fun _ _ => toIterM_inj.mp) ] at this
+    rwa [Subtype.mk.injEq]
+
+theorem IsPlausibleStep.eq_step [Iterator α Id β] [LawfulDeterministicIterator α Id]
+    {it : Iter (α := α) β} {step} (h : it.IsPlausibleStep step) :
+    step = it.step.val := by
+  have : ⟨step, h⟩ = it.step := Subsingleton.allEq _ _
+  simp [← this]
+
+end Std.Iter
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
index bb3763c508c5..1150800e5917 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
@@ -7,7 +7,10 @@ module
 
 prelude
 public import Init.Data.Iterators.Consumers.Access
+public import Init.Data.Iterators.Lemmas.Consumers.Loop
+import Init.Data.Iterators.Lemmas.Basic
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Access
+import Init.Omega
 
 namespace Std.Iter
 open Std.Iterators
@@ -48,4 +51,52 @@ public theorem atIdxSlow?_eq_match [Iterator α Id β] [Productive α Id]
       | .done => none) := by
   induction n, it using Iter.atIdxSlow?.induct_unfolding <;> simp_all
 
+public theorem lt_length_of_nextAtIdxSlow?_eq_yield [Iterator α Id β] [Finite α Id]
+    [Productive α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it it' : Iter (α := α) β} {i : Nat} {out : β}
+    (h : (it.nextAtIdxSlow? i).val = .yield it' out) :
+    i < it.length := by
+  induction it using Iter.inductSteps generalizing i it' out with
+  | step it ihy ihs =>
+    rw [Std.Iter.length_eq_match_step]
+    rw [nextAtIdxSlow?_eq_match] at h
+    cases hstep : it.step using PlausibleIterStep.casesOn with
+    | yield it'' out'' hp =>
+      simp only [hstep] at h
+      simp only
+      cases i with
+      | zero => omega
+      | succ k =>
+        simp only at h
+        exact Nat.succ_lt_succ (ihy hp h)
+    | skip it'' hp => exact ihs hp (by simpa [hstep] using h)
+    | done hp => simp [hstep] at h
+
+public theorem length_le_of_nextAtIdxSlow?_eq_done [Iterator α Id β] [Finite α Id]
+    [Productive α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {i : Nat}
+    (h : (it.nextAtIdxSlow? i).val = .done) :
+    it.length ≤ i := by
+  induction it using Iter.inductSteps generalizing i with
+  | step it ihy ihs =>
+    rw [Std.Iter.length_eq_match_step]
+    rw [nextAtIdxSlow?_eq_match] at h
+    cases hstep : it.step using PlausibleIterStep.casesOn with
+    | yield it'' out'' hp =>
+      simp only [hstep] at h
+      simp only
+      cases i with
+      | zero => simp at h
+      | succ k =>
+        have := ihy hp (by simpa using h)
+        omega
+    | skip it'' hp =>
+      simp only [hstep] at h
+      simp only
+      have := ihs hp h
+      omega
+    | done hp =>
+      simp only
+      omega
+
 end Std.Iter
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
index 676ce39abc13..d28251be41f1 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
@@ -8,13 +8,13 @@ module
 prelude
 public import Init.Data.Iterators.Consumers.Monadic.Access
 import all Init.Data.Iterators.Consumers.Monadic.Access
+public import Init.Data.Iterators.Consumers.Monadic.Loop
 public import Init.Control.Lawful.Basic
 import Init.Control.Lawful.Lemmas
 
 namespace Std.IterM
 open Std.Iterators
 
-
 public theorem atIdxSlow?_eq_match [Monad m] [LawfulMonad m] [Iterator α m β] [Productive α m]
     {n : Nat} {it : IterM (α := α) m β} :
     it.atIdxSlow? n = (do
diff --git a/src/Init/Data/Iterators/Lemmas/Monadic/Basic.lean b/src/Init/Data/Iterators/Lemmas/Monadic/Basic.lean
index 289875005f4c..95df1a701177 100644
--- a/src/Init/Data/Iterators/Lemmas/Monadic/Basic.lean
+++ b/src/Init/Data/Iterators/Lemmas/Monadic/Basic.lean
@@ -7,10 +7,11 @@ module
 
 prelude
 public import Init.Data.Iterators.Basic
+import Init.RCases
 
 public section
 
-namespace Std
+namespace Std.IterM
 open Std.Iterators
 
 /--
@@ -19,7 +20,7 @@ iterator `it` to an element of `motive it` by defining `f it` in terms of the va
 the plausible successors of `it'.
 -/
 @[specialize]
-def IterM.inductSteps {α m β} [Iterator α m β] [Finite α m]
+def inductSteps {α m β} [Iterator α m β] [Finite α m]
   (motive : IterM (α := α) m β → Sort x)
   (step : (it : IterM (α := α) m β) →
     (ih_yield : ∀ {it' : IterM (α := α) m β} {out : β},
@@ -38,7 +39,7 @@ iterator `it` to an element of `motive it` by defining `f it` in terms of the va
 the plausible skip successors of `it'.
 -/
 @[specialize]
-def IterM.inductSkips {α m β} [Iterator α m β] [Productive α m]
+def inductSkips {α m β} [Iterator α m β] [Productive α m]
   (motive : IterM (α := α) m β → Sort x)
   (step : (it : IterM (α := α) m β) →
     (ih_skip : ∀ {it' : IterM (α := α) m β}, it.IsPlausibleStep (.skip it') → motive it') →
@@ -47,4 +48,21 @@ def IterM.inductSkips {α m β} [Iterator α m β] [Productive α m]
   step it (fun {it'} _ => inductSkips motive step it')
 termination_by it.finitelyManySkips
 
-end Std
+-- Not a real instance because the discrimination key would be to indiscriminate.
+local instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α := α) Id β} :
+    Subsingleton it.Step where
+  allEq s s' := by
+    obtain ⟨s'', hs''⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq it
+    obtain ⟨s, hs⟩ := s
+    obtain ⟨s', hs'⟩ := s'
+    simp only [hs''] at hs hs'
+    have := hs.trans hs'.symm
+    rwa [Subtype.mk.injEq]
+
+theorem IsPlausibleStep.eq_step [Iterator α Id β] [LawfulDeterministicIterator α Id]
+    {it : IterM (α := α) Id β} {step} (h : it.IsPlausibleStep step) :
+    step = it.step.run.inflate.val := by
+  have : ⟨step, h⟩ = it.step.run.inflate := Subsingleton.allEq _ _
+  simp [← this]
+
+end Std.IterM
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
index 1a2f5adebc52..bc8a73765c8c 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -11,57 +11,27 @@ public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Combinators.Take
 public import Std.Data.Iterators.Combinators.StepSize
-import Init.Data.Iterators.Lemmas.Basic
-import Init.Omega
+import all Std.Data.Iterators.Combinators.StepSize
 import Init.Data.Iterators.Lemmas.Consumers.Access
 import Init.Data.Iterators.Lemmas.Consumers.Collect
-import Init.Data.Iterators.Lemmas.Consumers.Loop
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Access
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
-import Init.Data.Iterators.Lemmas.Monadic.Basic
 import all Init.Data.Iterators.Consumers.Monadic.Access
-import all Std.Data.Iterators.Combinators.StepSize
+import Init.Data.Iterators.Lemmas.Basic
+import Init.Data.Iterators.Lemmas.Monadic.Basic
+import Init.Omega
 
 public section
 open Std Std.Iterators Std.Iterators.Types
 
 namespace Std.Iter
 
+theorem stepSize_eq_intermediateStepSize [Iterator α Id β] [IteratorAccess α Id]
+    {it : Iter (α := α) β} {n : Nat} :
+    it.stepSize n = Intermediate.stepSize it 0 n :=
+  rfl
 
-instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α := α) Id β} :
-    Subsingleton it.Step where
-  allEq s s' := by
-    obtain ⟨s'', hs''⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq it
-    obtain ⟨s, hs⟩ := s
-    obtain ⟨s', hs'⟩ := s'
-    simp only [hs''] at hs hs'
-    have := hs.trans hs'.symm
-    rwa [Subtype.mk.injEq]
-
-instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : Iter (α := α) β} :
-    Subsingleton it.Step where
-  allEq s s' := by
-    obtain ⟨s'', hs''⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq it.toIterM
-    obtain ⟨s, hs⟩ := s
-    obtain ⟨s', hs'⟩ := s'
-    simp only [Iter.IsPlausibleStep, hs''] at hs hs'
-    have := hs.trans hs'.symm
-    rw [IterStep.mapIterator_inj (fun _ _ => toIterM_inj.mp) ] at this
-    rwa [Subtype.mk.injEq]
-
-theorem IsPlausibleStep.eq_step [Iterator α Id β] [LawfulDeterministicIterator α Id]
-    {it : Iter (α := α) β} {step} (h : it.IsPlausibleStep step) :
-    step = it.step.val := by
-  have : ⟨step, h⟩ = it.step := Subsingleton.allEq _ _
-  simp [← this]
-
-theorem _root_.Std.IterM.IsPlausibleStep.eq_step [Iterator α Id β] [LawfulDeterministicIterator α Id]
-    {it : IterM (α := α) Id β} {step} (h : it.IsPlausibleStep step) :
-    step = it.step.run.inflate.val := by
-  have : ⟨step, h⟩ = it.step.run.inflate := Subsingleton.allEq _ _
-  simp [← this]
-
-theorem _root_.Std.IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep [Iterator α Id β]
+theorem _root_.Std.IterM.IsPlausibleNthOutputStep.unique [Iterator α Id β]
     [LawfulDeterministicIterator α Id]
     {it : IterM (α := α) Id β} {s s'}
     (hs : it.IsPlausibleNthOutputStep n s)
@@ -112,7 +82,7 @@ instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α
   allEq s s' := by
     obtain ⟨s, hs⟩ := s
     obtain ⟨s', hs'⟩ := s'
-    have := IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep hs hs'
+    have := hs.unique hs'
     rwa [Subtype.mk.injEq]
 
 instance instLawfulDeterministicIteratorStepSizeIterator
@@ -126,7 +96,7 @@ instance instLawfulDeterministicIteratorStepSizeIterator
     · intro ⟨h₁, h₂⟩
       obtain ⟨hp₁, hp₂⟩ := hp
       simp only [IterStep.mapIterator] at h₁ hp₁
-      have heq := IterM.eq_of_isPlausibleNthOutputStep_of_isPlausibleNthOutputStep h₁ hp₁
+      have heq := h₁.unique hp₁
       generalize it.step.run.inflate.val = cstep at heq hp₁ hp₂ ⊢
       cases step with
       | skip _ => exact IterM.not_isPlausibleNthOutputStep_skip.elim (by simpa using h₁)
@@ -143,12 +113,12 @@ instance instLawfulDeterministicIteratorStepSizeIterator
           rcases it₁ with ⟨⟨_, _, _⟩⟩
           rcases it₂ with ⟨⟨_, _, _⟩⟩
           simp_all
-    · simp +contextual [hp]
+    · simpa +contextual using fun _ => hp
 
 theorem _root_.Std.IterM.nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id]
     [LawfulDeterministicIterator α Id] [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
     it.nextAtIdx? n = it.nextAtIdxSlow? n := by
-  ext
+  apply Id.ext
   apply Subsingleton.allEq
 
 theorem nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
@@ -164,13 +134,13 @@ theorem _root_.Std.IterM.nextAtIdxSlow?_stepSize_aux [Iterator α Id β] [Produc
         return .yield (IterM.Intermediate.stepSize it' (n - 1) n) out (by
           refine .zero_yield ?_
           simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, IterM.Intermediate.stepSize,
-            IterM.Intermediate.stepSize])
+            IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) -- TODO
       | .skip it' h => return IterM.not_isPlausibleNthOutputStep_skip.elim h
       | .done h =>
         return .done (by
           refine .done ?_
           simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Intermediate.stepSize,
-            IterM.Intermediate.stepSize])) := by
+            IterM.Intermediate.stepSize, StepSizeIterator.instIterator])) := by -- TODO
   induction it, i using IterM.atIdxSlow?.induct_unfolding
   rw [IterM.nextAtIdxSlow?_eq_match]
   simp only [IterM.Intermediate.stepSize, IterM.step_eq, IterM.internalState_mk,
@@ -181,11 +151,6 @@ theorem _root_.Std.IterM.nextAtIdxSlow?_stepSize_aux [Iterator α Id β] [Produc
   · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
   · simp
 
-@[simp]
-theorem Not.elim_eq {hP : P} {hnP : ¬ P} :
-    hnP.elim hP = x ↔ True :=
-  hnP.elim hP
-
 theorem _root_.Std.IterM.length_nextAtIdxSlow? [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
     {it : IterM (α := α) m β} :
     (do match ← it.nextAtIdxSlow? n with
@@ -203,28 +168,24 @@ theorem _root_.Std.IterM.length_nextAtIdxSlow? [Monad m] [LawfulMonad m] [Iterat
     · simp only [Nat.succ_eq_add_one, Nat.add_sub_add_right, bind_map_left]
       rw [← ihy ‹_›]
       apply bind_congr; intro step
-      cases step using PlausibleIterStep.casesOn <;> simp
+      cases step using PlausibleIterStep.casesOn <;> simp [Not.elim, absurd]
   · simp only [bind_pure_comp, bind_map_left, id_map']
     rw [← ihs ‹_›]
     apply bind_congr; intro step
-    cases step using PlausibleIterStep.casesOn <;> simp
+    cases step using PlausibleIterStep.casesOn <;> simp [Not.elim, absurd]
   · simp
 
--- TODO: rename
-theorem length_nextAtIdxSlow? [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
-    {it : Iter (α := α) β} :
-    (match it.nextAtIdxSlow? n with
-      | .yield it' _out _ => it'.length
-      | .skip _it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
-      | .done _h => 0) = it.length - n - 1 := by
+theorem length_nextAtIdxSlow? [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} :
+    (it.nextAtIdxSlow? n).val.successor.elim 0 Iter.length = it.length - n - 1 := by
   have := IterM.length_nextAtIdxSlow? (it := it.toIterM) (n := n)
   replace this := congrArg (fun x => ULift.down (Id.run x)) this
   simp only [Id.run_bind, Id.run_map] at this
   simp only [nextAtIdxSlow?, length, ← this]
   split at this
-  · simp [*]
+  · simpa [Option.elim, *]
   · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
-  · simp [*]
+  · simp [Option.elim, *]
 
 theorem nextAtIdxSlow?_zero_intermediate_stepSize [Iterator α Id β] [Productive α Id]
     [LawfulDeterministicIterator α Id]
@@ -235,13 +196,13 @@ theorem nextAtIdxSlow?_zero_intermediate_stepSize [Iterator α Id β] [Productiv
         .yield (Intermediate.stepSize it' (n - 1) n) out (by
           refine .zero_yield ?_
           simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-            Intermediate.stepSize, IterM.Intermediate.stepSize])
+            Intermediate.stepSize, IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) -- TODO
       | .skip it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
       | .done h =>
         .done (by
           refine .done ?_
           simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-            Intermediate.stepSize, IterM.Intermediate.stepSize]) := by
+            Intermediate.stepSize, IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) := by -- TODO
   simp only [Iter.nextAtIdxSlow?, Intermediate.stepSize, toIterM_toIter,
     IterM.nextAtIdxSlow?_stepSize_aux, Id.run_bind]
   apply Subtype.ext
@@ -320,7 +281,7 @@ private theorem nextAtIdxSlow?_zero_intermediate_stepSize_val [Iterator α Id β
   | skip _ h => exact IterM.not_isPlausibleNthOutputStep_skip.elim h
   | done => simp [IterStep.mapIterator]
 
-theorem atIdxSlow?_intermediate_stepSize [Iterator α Id β] [Productive α Id]
+theorem atIdxSlow?_intermediate_stepSize {α β} [Iterator α Id β] [Productive α Id]
     [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] {it : Iter (α := α) β} {i k n : Nat} :
     (Intermediate.stepSize it i n).atIdxSlow? k = it.atIdxSlow? (i + (n - 1 + 1) * k) := by
@@ -336,38 +297,32 @@ theorem atIdxSlow?_intermediate_stepSize [Iterator α Id β] [Productive α Id]
   | succ k ih =>
     cases hstep : (it.nextAtIdxSlow? i).val with
     | yield it' out =>
-      have hss : ((Intermediate.stepSize it i n).nextAtIdxSlow? 0).val =
-          .yield (Intermediate.stepSize it' (n - 1) n) out := by
-        rw [nextAtIdxSlow?_zero_intermediate_stepSize_val, hstep]; rfl
-      have h1 : (Intermediate.stepSize it i n).atIdxSlow? (0 + 1 + k) =
-          (Intermediate.stepSize it' (n - 1) n).atIdxSlow? k :=
-        atIdxSlow?_succ_of_nextAtIdxSlow?_yield hss
-      have h2 : (Intermediate.stepSize it i n).atIdxSlow? (k + 1) =
-          (Intermediate.stepSize it i n).atIdxSlow? (0 + 1 + k) := by
-        congr 1; omega
-      have h3 : it.atIdxSlow? (i + 1 + ((n - 1) + (n - 1 + 1) * k)) =
-          it'.atIdxSlow? ((n - 1) + (n - 1 + 1) * k) :=
-        atIdxSlow?_succ_of_nextAtIdxSlow?_yield hstep
-      have h4 : i + (n - 1 + 1) * (k + 1) = i + 1 + ((n - 1) + (n - 1 + 1) * k) := by
-        rw [Nat.mul_succ]; omega
-      rw [h2, h1, ih, ← h3, h4]
+      have h_nextAtIdxSlow?_zero :
+          ((Intermediate.stepSize it i n).nextAtIdxSlow? 0).val =
+            .yield (Intermediate.stepSize it' (n - 1) n) out := by
+        rw [nextAtIdxSlow?_zero_intermediate_stepSize_val, hstep, IterStep.mapIterator]
+      have h_atIdxSlow?_succ : (Intermediate.stepSize it i n).atIdxSlow? (k + 1) =
+          (Intermediate.stepSize it' (n - 1) n).atIdxSlow? k := by
+        rw [show k + 1 = 0 + 1 + k by omega, ← atIdxSlow?_succ_of_nextAtIdxSlow?_yield h_nextAtIdxSlow?_zero]
+      rw [h_atIdxSlow?_succ, ih, ← atIdxSlow?_succ_of_nextAtIdxSlow?_yield hstep]
+      congr 1
+      rw [Nat.mul_add]
+      omega
     | skip it' =>
-      exfalso
-      have := (it.nextAtIdxSlow? i).property
-      rw [hstep] at this
-      exact IterM.not_isPlausibleNthOutputStep_skip this
+      exact IterM.not_isPlausibleNthOutputStep_skip.elim
+        (by simpa [hstep] using (it.nextAtIdxSlow? i).property)
     | done =>
-      have hss : ((Intermediate.stepSize it i n).nextAtIdxSlow? 0).val = .done := by
+      have h_nextAtIdxSlow?_zero :
+          ((Intermediate.stepSize it i n).nextAtIdxSlow? 0).val = .done := by
         rw [nextAtIdxSlow?_zero_intermediate_stepSize_val, hstep]; rfl
-      rw [atIdxSlow?_none_of_nextAtIdxSlow?_done hss (by omega)]
+      rw [atIdxSlow?_none_of_nextAtIdxSlow?_done h_nextAtIdxSlow?_zero (by omega)]
       exact (atIdxSlow?_none_of_nextAtIdxSlow?_done hstep (by omega)).symm
 
 theorem atIdxSlow?_stepSize [Iterator α Id β] [Productive α Id]
     [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] {it : Iter (α := α) β} {k n : Nat} :
     (it.stepSize n).atIdxSlow? k = it.atIdxSlow? ((n - 1 + 1) * k) := by
-  show (Intermediate.stepSize it 0 n).atIdxSlow? k = _
-  rw [atIdxSlow?_intermediate_stepSize]; simp
+  simp [stepSize_eq_intermediateStepSize, atIdxSlow?_intermediate_stepSize]
 
 theorem getElem?_toList_stepSize [Iterator α Id β] [Productive α Id]
     [LawfulDeterministicIterator α Id]
@@ -376,7 +331,7 @@ theorem getElem?_toList_stepSize [Iterator α Id β] [Productive α Id]
     (it.stepSize n).toList[k]? = it.toList[(n - 1 + 1) * k]? := by
   simp only [getElem?_toList_eq_atIdxSlow?, atIdxSlow?_stepSize]
 
-private theorem step_eq_nextAtIdxSlow?_zero_val [Iterator α Id β] [Productive α Id]
+private theorem val_nextAtIdxSlow?_zero_eq_val_step [Iterator α Id β] [Productive α Id]
     {it : Iter (α := α) β} :
     (∀ (it' : Iter (α := α) β), ¬ it.IsPlausibleStep (.skip it')) →
     it.step.val = (it.nextAtIdxSlow? 0).val := by
@@ -384,79 +339,25 @@ private theorem step_eq_nextAtIdxSlow?_zero_val [Iterator α Id β] [Productive
   rw [nextAtIdxSlow?_eq_match]
   cases it.step using PlausibleIterStep.casesOn with
   | yield => simp
-  | skip _ hp => exact absurd hp (hno_skip _)
+  | skip _ hp => exact (hno_skip _).elim hp
   | done => simp
 
-private theorem not_isPlausibleStep_skip_intermediate_stepSize [Iterator α Id β]
+private theorem not_isPlausibleStep_skip_intermediateStepSize [Iterator α Id β]
     [IteratorAccess α Id] {it : Iter (α := α) β} {i n : Nat}
     {it' : Iter (α := Types.StepSizeIterator α Id β) β} :
     ¬ (Intermediate.stepSize it i n).IsPlausibleStep (.skip it') := by
   simp only [Iter.IsPlausibleStep, IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
     IterStep.mapIterator, Intermediate.stepSize, IterM.Intermediate.stepSize]
-  intro ⟨h, _⟩
-  exact IterM.not_isPlausibleNthOutputStep_skip h
+  exact fun h => IterM.not_isPlausibleNthOutputStep_skip.elim h.1
 
-private theorem step_intermediate_stepSize_val [Iterator α Id β] [Productive α Id]
+private theorem val_step_intermediateStepSize [Iterator α Id β] [Productive α Id]
     [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] {it : Iter (α := α) β} {i n : Nat} :
     (Intermediate.stepSize it i n).step.val =
       (it.nextAtIdxSlow? i).val.mapIterator (fun it' => Intermediate.stepSize it' (n - 1) n) := by
-  rw [step_eq_nextAtIdxSlow?_zero_val (fun _ => not_isPlausibleStep_skip_intermediate_stepSize),
+  rw [val_nextAtIdxSlow?_zero_eq_val_step (fun _ => not_isPlausibleStep_skip_intermediateStepSize),
     nextAtIdxSlow?_zero_intermediate_stepSize_val]
 
-private theorem lt_length_of_nextAtIdxSlow?_yield [Iterator α Id β] [Finite α Id]
-    [Productive α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
-    {it it' : Iter (α := α) β} {i : Nat} {out : β}
-    (h : (it.nextAtIdxSlow? i).val = .yield it' out) :
-    i < it.length := by
-  induction it using Iter.inductSteps generalizing i it' out with
-  | step it ihy ihs =>
-    rw [Std.Iter.length_eq_match_step]
-    rw [nextAtIdxSlow?_eq_match] at h
-    cases hstep : it.step using PlausibleIterStep.casesOn with
-    | yield it'' out'' hp =>
-      simp only [hstep] at h
-      simp only
-      cases i with
-      | zero => omega
-      | succ k =>
-        simp only at h
-        exact Nat.succ_lt_succ (ihy hp h)
-    | skip it'' hp =>
-      simp only [hstep] at h
-      simp only
-      exact ihs hp h
-    | done hp =>
-      simp [hstep] at h
-
-private theorem length_le_of_nextAtIdxSlow?_done [Iterator α Id β] [Finite α Id]
-    [Productive α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
-    {it : Iter (α := α) β} {i : Nat}
-    (h : (it.nextAtIdxSlow? i).val = .done) :
-    it.length ≤ i := by
-  induction it using Iter.inductSteps generalizing i with
-  | step it ihy ihs =>
-    rw [Std.Iter.length_eq_match_step]
-    rw [nextAtIdxSlow?_eq_match] at h
-    cases hstep : it.step using PlausibleIterStep.casesOn with
-    | yield it'' out'' hp =>
-      simp only [hstep] at h
-      simp only
-      cases i with
-      | zero => simp at h
-      | succ k =>
-        simp only at h
-        have := ihy hp h
-        omega
-    | skip it'' hp =>
-      simp only [hstep] at h
-      simp only
-      have := ihs hp h
-      omega
-    | done hp =>
-      simp only
-      omega
-
 theorem Intermediate.length_stepSize [Iterator α Id β] [Finite α Id]
     [Productive α Id] [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
@@ -464,33 +365,27 @@ theorem Intermediate.length_stepSize [Iterator α Id β] [Finite α Id]
     (Intermediate.stepSize it i n).length = (it.length + (n - 1) - i) / (n - 1 + 1) := by
   generalize hsit : Intermediate.stepSize it i n = sit
   replace hsit := hsit.symm
-  induction sit using Iter.inductSteps generalizing it i with
-  | step oit ih_yield ih_skip =>
-    rw [Std.Iter.length_eq_match_step]
-    subst hsit
-    rw [step_intermediate_stepSize_val]
-    cases h : (it.nextAtIdxSlow? i) using PlausibleIterStep.casesOn with
-    | yield it' out hp =>
-      simp only [IterStep.mapIterator]
-      rw [ih_yield (it := it') (i := n - 1) (out := out) _ rfl]
-      · have hlength := length_nextAtIdxSlow? (it := it) (n := i)
-        simp only [h] at hlength
-        simp only [hlength, Nat.add_sub_cancel, Nat.zero_lt_succ, ← Nat.add_div_right]
-        have hi := lt_length_of_nextAtIdxSlow?_yield (by rw [h])
-        congr 1; omega
-      · have := (Intermediate.stepSize it i n).step.property
-        simpa [step_intermediate_stepSize_val, h, IterStep.mapIterator]
-    | skip _ hp => exact IterM.not_isPlausibleNthOutputStep_skip.elim hp
-    | done hp =>
-      simp only [IterStep.mapIterator]
-      apply Nat.div_eq_of_lt _ |>.symm
-      have hi := length_le_of_nextAtIdxSlow?_done (by rw [h])
-      omega
-
-theorem stepSize_eq_intermediateStepSize [Iterator α Id β] [IteratorAccess α Id]
-    {it : Iter (α := α) β} {n : Nat} :
-    it.stepSize n = Intermediate.stepSize it 0 n :=
-  rfl
+  induction sit using Iter.inductSteps generalizing it i with | step it ihy ihs
+  rw [Std.Iter.length_eq_match_step]
+  subst hsit
+  rw [val_step_intermediateStepSize]
+  cases h : (it.nextAtIdxSlow? i) using PlausibleIterStep.casesOn with
+  | yield it' out hp =>
+    simp only [IterStep.mapIterator]
+    rw [ihy (it := it') (i := n - 1) (out := out) _ rfl]
+    · have hlength := length_nextAtIdxSlow? (it := it) (n := i)
+      simp only [h, IterStep.successor_yield, Option.elim] at hlength
+      simp only [hlength, Nat.add_sub_cancel, Nat.zero_lt_succ, ← Nat.add_div_right]
+      have hi := lt_length_of_nextAtIdxSlow?_eq_yield (by rw [h])
+      congr 1; omega
+    · have := (Intermediate.stepSize it i n).step.property
+      simpa [val_step_intermediateStepSize, h, IterStep.mapIterator]
+  | skip _ hp => exact IterM.not_isPlausibleNthOutputStep_skip.elim hp
+  | done hp =>
+    simp only [IterStep.mapIterator]
+    apply Nat.div_eq_of_lt _ |>.symm
+    have hi := length_le_of_nextAtIdxSlow?_eq_done (by rw [h])
+    omega
 
 theorem length_stepSize [Iterator α Id β] [Finite α Id] [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
diff --git a/src/Std/Data/Iterators/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
index f293c322743b..5c8fef0bb4e4 100644
--- a/src/Std/Data/Iterators/Producers/Monadic/Array.lean
+++ b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
@@ -131,15 +131,15 @@ instance : IteratorAccess (ArrayIterator α) Id where
       induction n generalizing it
       · split
         · refine .zero_yield ?_
-          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, *]
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, ArrayIterator.instIterator, *] -- TODO
         · refine .done ?_
-          simp_all [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          simp_all [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, ArrayIterator.instIterator] -- TODO
       · rename_i n ih
         by_cases h : it.internalState.pos < it.internalState.array.size
         · refine .yield (it' := ?it') (out := ?_) ?_ ?_
           · exact ⟨⟨it.internalState.array, it.internalState.pos + 1⟩⟩
           · exact it.internalState.array[it.internalState.pos]
-          · simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          · simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, ArrayIterator.instIterator] -- TODO
           · specialize ih ?it'
             simp only [Nat.add_comm 1, Nat.add_assoc] at ih ⊢
             split

From fa96b5c37e2819e6e52f03fb19529daca179f3ae Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 16:44:25 +0100
Subject: [PATCH 08/18] cleanups

---
 .../Iterators/Consumers/Monadic/Access.lean   | 45 +++++++++++++++
 .../Combinators/Monadic/StepSize.lean         |  4 +-
 .../Lemmas/Combinators/StepSize.lean          | 55 ++-----------------
 .../Lemmas/Producers/Monadic/Array.lean       |  2 +-
 .../Lemmas/Producers/Monadic/List.lean        |  2 +-
 .../Lemmas/Producers/Monadic/Vector.lean      |  2 +-
 6 files changed, 55 insertions(+), 55 deletions(-)

diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
index 424e131c8d2a..dc76b55b69f9 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Iterators.Basic
 public import Init.WFExtrinsicFix
 import Init.RCases
+import Init.Data.Iterators.Lemmas.Monadic.Basic
 
 set_option linter.missingDocs true
 
@@ -98,6 +99,50 @@ theorem IterM.isPlausibleNthOutputStep_trans_of_done {α β : Type w} {m : Type
     cases hs
     exact .done ‹_›
 
+theorem IterM.IsPlausibleNthOutputStep.unique [Iterator α Id β]
+    [LawfulDeterministicIterator α Id] {it : IterM (α := α) Id β} {s s'}
+    (hs : it.IsPlausibleNthOutputStep n s) (hs' : it.IsPlausibleNthOutputStep n s') :
+    s = s' := by
+  induction hs
+  case zero_yield h =>
+    match hs' with
+    | .zero_yield h' ..
+    | .skip h' ..
+    | .done h' =>
+      replace h' := h'.eq_step
+      rw [← h.eq_step] at h'
+      cases h'
+      all_goals simp
+  case done h =>
+    match hs' with
+    | .zero_yield h' ..
+    | .yield h' ..
+    | .skip h' .. =>
+      replace h := h.eq_step
+      replace h' := h'.eq_step
+      rw [← h] at h'
+      cases h'
+    | .done h' => simp
+  case yield h _ ih =>
+    match hs' with
+    | .yield h' ..
+    | .skip h' ..
+    | .done h' =>
+      replace h' := h'.eq_step
+      rw [← h.eq_step] at h'
+      cases h'
+      all_goals apply ih ‹_›
+  case skip h _ ih =>
+    match hs' with
+    | .zero_yield h' ..
+    | .yield h' ..
+    | .skip h' ..
+    | .done h' =>
+      replace h' := h'.eq_step
+      rw [← h.eq_step] at h'
+      cases h'
+      all_goals apply ih ‹_›
+
 /--
 `IteratorAccess α m` provides efficient implementations for random access or iterators that support
 it. `it.nextAtIdx? n` either returns the step in which the `n`th value of `it` is emitted
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
index 9ccc460c028e..1c2851a913f5 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
@@ -92,7 +92,7 @@ def StepSizeIterator.instFinitenessRelation [Iterator α m β] [IteratorAccess 
     apply WellFoundedRelation.wf
   subrelation {it it'} h := by
     obtain ⟨step, hs, h⟩ := h
-    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIterator] at h -- TODO
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIterator] at h -- TODO: remove `inst...` argument as soon as possible
     simp only [InvImage]
     obtain ⟨⟨n, it⟩⟩ := it
     simp only at ⊢ h
@@ -125,7 +125,7 @@ def StepSizeIterator.instProductivenessRelation [Iterator α m β] [IteratorAcce
     apply InvImage.wf
     apply WellFoundedRelation.wf
   subrelation {it it'} h := by
-    simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIterator] at h -- TODO
+    simp only [IterM.IsPlausibleSkipSuccessorOf, IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIterator] at h -- TODO: remove `inst...` argument as soon as possible
     simp only [InvImage]
     obtain ⟨⟨n, it⟩⟩ := it
     simp only [IterStep.mapIterator_skip, Function.comp_apply] at ⊢ h
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
index bc8a73765c8c..2db9879d01a9 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Iterators.Consumers.Access
+public import Init.Data.Iterators.Consumers.Monadic.Access
 public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Combinators.Take
@@ -31,52 +32,6 @@ theorem stepSize_eq_intermediateStepSize [Iterator α Id β] [IteratorAccess α
     it.stepSize n = Intermediate.stepSize it 0 n :=
   rfl
 
-theorem _root_.Std.IterM.IsPlausibleNthOutputStep.unique [Iterator α Id β]
-    [LawfulDeterministicIterator α Id]
-    {it : IterM (α := α) Id β} {s s'}
-    (hs : it.IsPlausibleNthOutputStep n s)
-    (hs' : it.IsPlausibleNthOutputStep n s') :
-    s = s' := by
-  induction hs
-  case zero_yield h =>
-    match hs' with
-    | .zero_yield h' ..
-    | .skip h' ..
-    | .done h' =>
-      replace h' := h'.eq_step
-      rw [← h.eq_step] at h'
-      cases h'
-      all_goals simp
-  case done h =>
-    match hs' with
-    | .zero_yield h' ..
-    | .yield h' ..
-    | .skip h' .. =>
-      replace h := h.eq_step
-      replace h' := h'.eq_step
-      rw [← h] at h'
-      cases h'
-    | .done h' => simp
-  case yield h _ ih =>
-    match hs' with
-    | .yield h' ..
-    | .skip h' ..
-    | .done h' =>
-      replace h' := h'.eq_step
-      rw [← h.eq_step] at h'
-      cases h'
-      all_goals apply ih ‹_›
-  case skip h _ ih =>
-    match hs' with
-    | .zero_yield h' ..
-    | .yield h' ..
-    | .skip h' ..
-    | .done h' =>
-      replace h' := h'.eq_step
-      rw [← h.eq_step] at h'
-      cases h'
-      all_goals apply ih ‹_›
-
 instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α := α) Id β} :
     Subsingleton (PlausibleIterStep (it.IsPlausibleNthOutputStep n)) where
   allEq s s' := by
@@ -134,13 +89,13 @@ theorem _root_.Std.IterM.nextAtIdxSlow?_stepSize_aux [Iterator α Id β] [Produc
         return .yield (IterM.Intermediate.stepSize it' (n - 1) n) out (by
           refine .zero_yield ?_
           simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, IterM.Intermediate.stepSize,
-            IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) -- TODO
+            IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) -- TODO: remove `inst...` argument as soon as possible
       | .skip it' h => return IterM.not_isPlausibleNthOutputStep_skip.elim h
       | .done h =>
         return .done (by
           refine .done ?_
           simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Intermediate.stepSize,
-            IterM.Intermediate.stepSize, StepSizeIterator.instIterator])) := by -- TODO
+            IterM.Intermediate.stepSize, StepSizeIterator.instIterator])) := by -- TODO: remove `inst...` argument as soon as possible
   induction it, i using IterM.atIdxSlow?.induct_unfolding
   rw [IterM.nextAtIdxSlow?_eq_match]
   simp only [IterM.Intermediate.stepSize, IterM.step_eq, IterM.internalState_mk,
@@ -196,13 +151,13 @@ theorem nextAtIdxSlow?_zero_intermediate_stepSize [Iterator α Id β] [Productiv
         .yield (Intermediate.stepSize it' (n - 1) n) out (by
           refine .zero_yield ?_
           simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-            Intermediate.stepSize, IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) -- TODO
+            Intermediate.stepSize, IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) -- TODO: remove `inst...` argument as soon as possible
       | .skip it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
       | .done h =>
         .done (by
           refine .done ?_
           simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-            Intermediate.stepSize, IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) := by -- TODO
+            Intermediate.stepSize, IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) := by -- TODO: remove `inst...` argument as soon as possible
   simp only [Iter.nextAtIdxSlow?, Intermediate.stepSize, toIterM_toIter,
     IterM.nextAtIdxSlow?_stepSize_aux, Id.run_bind]
   apply Subtype.ext
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
index ee41fc51db27..774cbd9fa188 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
@@ -60,7 +60,7 @@ theorem Std.Iterators.Types.ArrayIterator.stepAsHetT_iterFromIdxM [LawfulMonad m
     else
       pure .done) := by
   simp only [Array.iterFromIdxM, pure, HetT.ext_iff, Equivalence.property_step,
-    IterM.IsPlausibleStep, instIterator, -- TODO
+    IterM.IsPlausibleStep, instIterator, -- TODO: remove `inst...` argument as soon as possible
     Iterator.IsPlausibleStep, Equivalence.prun_step, ge_iff_le]
   refine ⟨?_, ?_⟩
   · ext step
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
index e2a949d6178d..045db900f9ce 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
@@ -22,7 +22,7 @@ public theorem Types.ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β}
       | x :: xs => pure (.yield (xs.iterM m) x)) := by
   simp only [List.iterM, HetT.ext_iff, Equivalence.property_step, IterM.IsPlausibleStep,
     Equivalence.prun_step,
-    -- TODO: get rid of these
+    -- TODO: remove `inst...` argument as soon as possible: get rid of these
     Iterator.IsPlausibleStep, ListIterator.instIterator]
   refine ⟨?_, ?_⟩
   · ext step
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Vector.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Vector.lean
index aec910212457..9bdba2656c80 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Vector.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Vector.lean
@@ -46,7 +46,7 @@ theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdxM_of_lt {xs : Vector β
 theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdxM_of_not_lt {xs : Vector β n} {pos : Nat}
     (h : ¬ pos < n) :
     (xs.iterFromIdxM m pos).IsPlausibleStep .done := by
-  simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Types.ArrayIterator.instIterator] -- TODO
+  simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Types.ArrayIterator.instIterator] -- TODO: remove `inst...` argument as soon as possible
   simpa [Vector.iterFromIdxM, Array.iterFromIdxM, Nat.not_lt] using h
 
 theorem Std.Iterators.Vector.isPlausibleStep_iterM_of_pos {xs : Vector β n}

From f6a56da39af9e48ccdada0b3c14d33974425df4e Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 16:57:56 +0100
Subject: [PATCH 09/18] help orphan

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

diff --git a/src/Std/Data/Iterators/Lemmas/Combinators.lean b/src/Std/Data/Iterators/Lemmas/Combinators.lean
index 70b5d2c4212a..c96202e8d3de 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators.lean
@@ -11,3 +11,4 @@ public import Std.Data.Iterators.Lemmas.Combinators.TakeWhile
 public import Std.Data.Iterators.Lemmas.Combinators.Drop
 public import Std.Data.Iterators.Lemmas.Combinators.DropWhile
 public import Std.Data.Iterators.Lemmas.Combinators.Zip
+public import Std.Data.Iterators.Lemmas.Combinators.StepSize

From bb59d9c00ffb526d00cc4985b9f1e2214c0e3519 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 17:00:52 +0000
Subject: [PATCH 10/18] feat: add LawfulDeterministicIterator instances for
 base iterators and combinators

This PR adds LawfulDeterministicIterator instances for ListIterator,
ArrayIterator, Zipper, AssocListIterator, FilterMap (pure), Map (pure),
and Flatten combinators, enabling deterministic reasoning about
tree map and hash map iterators built from these components.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 .../Lemmas/Combinators/FilterMap.lean         | 119 ++++++++++++++++++
 .../Iterators/Lemmas/Combinators/FlatMap.lean |  74 +++++++++++
 .../Data/Iterators/Lemmas/Producers/List.lean |  20 +++
 .../DHashMap/Internal/AssocList/Iterator.lean |  21 ++++
 src/Std/Data/DTreeMap/Internal/Zipper.lean    |   6 +
 .../Iterators/Lemmas/Producers/Array.lean     |  25 ++++
 6 files changed, 265 insertions(+)

diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
index d90a4013d772..0c86afaaa771 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
@@ -1055,4 +1055,123 @@ theorem Iter.all_map {α β β' : Type w}
   · simp [ihs ‹_›]
   · simp
 
+section LawfulDeterministic
+
+variable {α β γ : Type w} [Iterator α Id β] [LawfulDeterministicIterator α Id]
+
+private theorem PostconditionT.map_some_pure_property' {v : Option γ} {x : γ}
+    (h : (PostconditionT.map some (PostconditionT.pure (m := Id) x)).Property v) : v = some x := by
+  obtain ⟨⟨a, ha⟩, rfl⟩ := h; congr 1; exact ha.symm
+
+instance instLawfulDeterministicIteratorFilterMapPure
+    {lift : ⦃α : Type w⦄ → Id α → Id α}
+    {f : β → Option γ} :
+    LawfulDeterministicIterator
+      (Iterators.Types.FilterMap α Id Id lift (fun b => pure (f b))) Id where
+  isPlausibleStep_eq_eq it := by
+    obtain ⟨innerStep, hinner⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq
+      it.internalState.inner
+    cases innerStep with
+    | done =>
+      exact ⟨.done, by
+        ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+        constructor
+        · intro h; cases h with
+          | done h => rfl
+          | yieldNone h => rw [hinner] at h; cases h
+          | yieldSome h => rw [hinner] at h; cases h
+          | skip h => rw [hinner] at h; cases h
+        · intro h; cases h; exact .done (by rw [hinner])⟩
+    | skip it' =>
+      exact ⟨.skip (IterM.InternalCombinators.filterMap lift _ it'), by
+        ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+        constructor
+        · intro h; cases h with
+          | skip h => rw [hinner] at h; cases h; rfl
+          | done h => rw [hinner] at h; cases h
+          | yieldNone h => rw [hinner] at h; cases h
+          | yieldSome h => rw [hinner] at h; cases h
+        · intro h; cases h; exact .skip (by rw [hinner])⟩
+    | yield it' out =>
+      cases hfout : f out with
+      | none =>
+        exact ⟨.skip (IterM.InternalCombinators.filterMap lift _ it'), by
+          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          constructor
+          · intro h; cases h with
+            | yieldNone h hp =>
+              rw [hinner] at h; cases h; rfl
+            | yieldSome h hp =>
+              rw [hinner] at h; cases h
+              rw [hfout] at hp; cases hp
+            | skip h => rw [hinner] at h; cases h
+            | done h => rw [hinner] at h; cases h
+          · intro h; cases h
+            exact .yieldNone (by rw [hinner]) (show f out = none from hfout)⟩
+      | some out' =>
+        exact ⟨.yield (IterM.InternalCombinators.filterMap lift _ it') out', by
+          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          constructor
+          · intro h; cases h with
+            | yieldSome h hp =>
+              rw [hinner] at h; cases h
+              rw [hfout] at hp; cases hp; rfl
+            | yieldNone h hp =>
+              rw [hinner] at h; cases h
+              rw [hfout] at hp; cases hp
+            | skip h => rw [hinner] at h; cases h
+            | done h => rw [hinner] at h; cases h
+          · intro h; cases h
+            exact .yieldSome (by rw [hinner]) (show f out = some out' from hfout)⟩
+
+instance instLawfulDeterministicIteratorMapPure
+    {lift : ⦃α : Type w⦄ → Id α → Id α}
+    {f : β → γ} :
+    LawfulDeterministicIterator
+      (Iterators.Types.Map α Id Id lift (fun b => pure (f b))) Id where
+  isPlausibleStep_eq_eq it := by
+    obtain ⟨innerStep, hinner⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq
+      it.internalState.inner
+    cases innerStep with
+    | done =>
+      exact ⟨.done, by
+        ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+        constructor
+        · intro h; cases h with
+          | done h => rfl
+          | yieldNone h => rw [hinner] at h; cases h
+          | yieldSome h => rw [hinner] at h; cases h
+          | skip h => rw [hinner] at h; cases h
+        · intro h; cases h; exact .done (by rw [hinner])⟩
+    | skip it' =>
+      exact ⟨.skip (IterM.InternalCombinators.filterMap lift _ it'), by
+        ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+        constructor
+        · intro h; cases h with
+          | skip h => rw [hinner] at h; cases h; rfl
+          | done h => rw [hinner] at h; cases h
+          | yieldNone h => rw [hinner] at h; cases h
+          | yieldSome h => rw [hinner] at h; cases h
+        · intro h; cases h; exact .skip (by rw [hinner])⟩
+    | yield it' out =>
+      exact ⟨.yield (IterM.InternalCombinators.filterMap lift _ it') (f out), by
+        ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+        constructor
+        · intro h; cases h with
+          | yieldSome h hp =>
+            rw [hinner] at h; cases h
+            have := PostconditionT.map_some_pure_property' hp
+            cases this; rfl
+          | yieldNone h hp =>
+            rw [hinner] at h; cases h
+            have := PostconditionT.map_some_pure_property' hp
+            cases this
+          | skip h => rw [hinner] at h; cases h
+          | done h => rw [hinner] at h; cases h
+        · intro h; cases h
+          refine .yieldSome (by rw [hinner]) ?_
+          exact ⟨⟨f out, rfl⟩, rfl⟩⟩
+
+end LawfulDeterministic
+
 end Std
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
index af874ee622f2..b44153620eb4 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
@@ -268,4 +268,78 @@ public theorem Iter.toArray_flatMap {α α₂ β γ : Type w} [Iterator α Id β
     (it₁.flatMap f).toArray = (it₁.map fun b => (f b).toArray).toArray.flatten := by
   simp [flatMap, toArray_flatMapAfter]
 
+section LawfulDeterministic
+
+variable {α α₂ β : Type w}
+
+instance instLawfulDeterministicIteratorFlatten
+    [Iterator α Id (IterM (α := α₂) Id β)] [Iterator α₂ Id β]
+    [LawfulDeterministicIterator α Id] [LawfulDeterministicIterator α₂ Id] :
+    LawfulDeterministicIterator (Iterators.Types.Flatten α α₂ β Id) Id where
+  isPlausibleStep_eq_eq it := by
+    rcases it with ⟨⟨it₁, it₂⟩⟩
+    cases it₂ with
+    | none =>
+      obtain ⟨outerStep, houter⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq it₁
+      cases outerStep with
+      | done =>
+        exact ⟨.done, by
+          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          constructor
+          · intro h; cases h with
+            | outerDone h => rfl
+            | outerYield h => rw [houter] at h; cases h
+            | outerSkip h => rw [houter] at h; cases h
+          · intro h; cases h; exact .outerDone (by rw [houter])⟩
+      | skip it₁' =>
+        exact ⟨.skip ⟨⟨it₁', none⟩⟩, by
+          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          constructor
+          · intro h; cases h with
+            | outerSkip h => rw [houter] at h; cases h; rfl
+            | outerDone h => rw [houter] at h; cases h
+            | outerYield h => rw [houter] at h; cases h
+          · intro h; cases h; exact .outerSkip (by rw [houter])⟩
+      | yield it₁' it₂' =>
+        exact ⟨.skip ⟨⟨it₁', some it₂'⟩⟩, by
+          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          constructor
+          · intro h; cases h with
+            | outerYield h => rw [houter] at h; cases h; rfl
+            | outerDone h => rw [houter] at h; cases h
+            | outerSkip h => rw [houter] at h; cases h
+          · intro h; cases h; exact .outerYield (by rw [houter])⟩
+    | some it₂ =>
+      obtain ⟨innerStep, hinner⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq it₂
+      cases innerStep with
+      | done =>
+        exact ⟨.skip ⟨⟨it₁, none⟩⟩, by
+          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          constructor
+          · intro h; cases h with
+            | innerDone h => rfl
+            | innerYield h => rw [hinner] at h; cases h
+            | innerSkip h => rw [hinner] at h; cases h
+          · intro h; cases h; exact .innerDone (by rw [hinner])⟩
+      | skip it₂' =>
+        exact ⟨.skip ⟨⟨it₁, some it₂'⟩⟩, by
+          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          constructor
+          · intro h; cases h with
+            | innerSkip h => rw [hinner] at h; cases h; rfl
+            | innerDone h => rw [hinner] at h; cases h
+            | innerYield h => rw [hinner] at h; cases h
+          · intro h; cases h; exact .innerSkip (by rw [hinner])⟩
+      | yield it₂' b =>
+        exact ⟨.yield ⟨⟨it₁, some it₂'⟩⟩ b, by
+          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          constructor
+          · intro h; cases h with
+            | innerYield h => rw [hinner] at h; cases h; rfl
+            | innerDone h => rw [hinner] at h; cases h
+            | innerSkip h => rw [hinner] at h; cases h
+          · intro h; cases h; exact .innerYield (by rw [hinner])⟩
+
+end LawfulDeterministic
+
 end Std
diff --git a/src/Init/Data/Iterators/Lemmas/Producers/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/List.lean
index 32a61c13061d..460960ef90f1 100644
--- a/src/Init/Data/Iterators/Lemmas/Producers/List.lean
+++ b/src/Init/Data/Iterators/Lemmas/Producers/List.lean
@@ -23,6 +23,26 @@ open Std Std.Iterators
 
 variable {β : Type w}
 
+instance : LawfulDeterministicIterator (Iterators.Types.ListIterator β) Id where
+  isPlausibleStep_eq_eq it := by
+    rcases it with ⟨⟨_ | ⟨x, xs⟩⟩⟩
+    · exact ⟨.done, by
+        ext step
+        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          Iterators.Types.ListIterator.instIterator]
+        cases step <;> simp⟩
+    · exact ⟨.yield ⟨⟨xs⟩⟩ x, by
+        ext step
+        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          Iterators.Types.ListIterator.instIterator]
+        cases step with
+        | yield it' out =>
+          constructor
+          · intro h; rcases it' with ⟨⟨l⟩⟩; simp_all
+          · intro h; cases h; rfl
+        | skip => simp
+        | done => simp⟩
+
 @[simp]
 theorem List.step_iter_nil :
     (([] : List β).iter).step = ⟨.done, rfl⟩ := by
diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
index e2c212224966..165f3a9b1126 100644
--- a/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
+++ b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
@@ -34,6 +34,27 @@ public instance : Iterator (α := AssocListIterator α β) Id ((a : α) × β a)
         | ⟨⟨.nil⟩⟩ => .deflate ⟨.done, rfl⟩
         | ⟨⟨.cons k v l⟩⟩ => .deflate ⟨.yield ⟨⟨l⟩⟩ ⟨k, v⟩, rfl⟩)
 
+public instance : LawfulDeterministicIterator (AssocListIterator α β) Id where
+  isPlausibleStep_eq_eq it := by
+    rcases it with ⟨⟨_ | ⟨k, v, l⟩⟩⟩
+    · exact ⟨.done, by
+        ext step
+        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          instIteratorAssocListIteratorIdSigma]
+        cases step <;> simp⟩
+    · exact ⟨.yield ⟨⟨l⟩⟩ ⟨k, v⟩, by
+        ext step
+        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          instIteratorAssocListIteratorIdSigma]
+        cases step with
+        | yield it' out =>
+          constructor
+          · intro h; rcases it' with ⟨⟨l'⟩⟩; rcases out with ⟨k', v'⟩
+            cases h; rfl
+          · intro h; cases h; rfl
+        | skip => simp
+        | done => simp⟩
+
 def AssocListIterator.finitenessRelation :
     FinitenessRelation (AssocListIterator α β) Id where
   Rel := InvImage WellFoundedRelation.rel (AssocListIterator.l ∘ IterM.internalState)
diff --git a/src/Std/Data/DTreeMap/Internal/Zipper.lean b/src/Std/Data/DTreeMap/Internal/Zipper.lean
index 46c61398b5d8..138648f9ffc6 100644
--- a/src/Std/Data/DTreeMap/Internal/Zipper.lean
+++ b/src/Std/Data/DTreeMap/Internal/Zipper.lean
@@ -337,6 +337,12 @@ public instance : Iterator (Zipper α β) Id ((a : α) × β a) where
   IsPlausibleStep it step := it.internalState.step = step
   step it := pure <| Shrink.deflate ⟨it.internalState.step, rfl⟩
 
+public instance : LawfulDeterministicIterator (Zipper α β) Id where
+  isPlausibleStep_eq_eq it := ⟨it.internalState.step, by
+    ext step
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorZipperIdSigma,
+      eq_comm]⟩
+
 def Zipper.FinitenessRelation : FinitenessRelation (Zipper α β) Id where
   Rel t' t := t'.internalState.size < t.internalState.size
   wf := by
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
index 7e2061c31dbd..28c85e8d353a 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
@@ -12,6 +12,7 @@ import Init.Data.List.TakeDrop
 public import Std.Data.Iterators.Producers.Array
 public import Init.Data.Iterators.Producers.List
 public import Std.Data.Iterators.Lemmas.Producers.Monadic.Array
+import Init.Omega
 
 @[expose] public section
 
@@ -26,6 +27,30 @@ open Std Std.Iterators
 
 variable {β : Type w}
 
+instance : LawfulDeterministicIterator (Iterators.Types.ArrayIterator β) Id where
+  isPlausibleStep_eq_eq it := by
+    rcases it with ⟨⟨array, pos⟩⟩
+    refine if h : pos < array.size then ?_ else ?_
+    · exact ⟨.yield ⟨⟨array, pos + 1⟩⟩ array[pos], by
+        ext step
+        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          Iterators.Types.ArrayIterator.instIterator]
+        cases step with
+        | yield it' out =>
+          constructor
+          · rintro ⟨ha, hp, hlt, hv⟩; rcases it' with ⟨⟨a', p'⟩⟩; simp_all
+          · intro heq; cases heq; exact ⟨rfl, rfl, h, rfl⟩
+        | skip => simp
+        | done => simp; omega⟩
+    · exact ⟨.done, by
+        ext step
+        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          Iterators.Types.ArrayIterator.instIterator]
+        cases step with
+        | yield => simp; intro _ _ hlt; omega
+        | skip => simp
+        | done => simp; omega⟩
+
 theorem Array.iter_eq_toIter_iterM {array : Array β} :
     array.iter = (array.iterM Id).toIter :=
   rfl

From 59036e9442988ade56d4b92a6a4ea3b169cfdf84 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 17:35:45 +0000
Subject: [PATCH 11/18] feat: add getElem?_toArray_stepSize theorem

This PR adds a theorem relating toArray indexing on stepSize iterators
to toArray indexing on the underlying iterator, complementing the
existing toList and atIdxSlow? versions.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
index 2db9879d01a9..23a8dc7dd270 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -286,6 +286,13 @@ theorem getElem?_toList_stepSize [Iterator α Id β] [Productive α Id]
     (it.stepSize n).toList[k]? = it.toList[(n - 1 + 1) * k]? := by
   simp only [getElem?_toList_eq_atIdxSlow?, atIdxSlow?_stepSize]
 
+theorem getElem?_toArray_stepSize [Iterator α Id β] [Productive α Id]
+    [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] [Finite α Id]
+    {it : Iter (α := α) β} {k n : Nat} :
+    (it.stepSize n).toArray[k]? = it.toArray[(n - 1 + 1) * k]? := by
+  simp only [← Array.getElem?_toList, Iter.toList_toArray, getElem?_toList_stepSize]
+
 private theorem val_nextAtIdxSlow?_zero_eq_val_step [Iterator α Id β] [Productive α Id]
     {it : Iter (α := α) β} :
     (∀ (it' : Iter (α := α) β), ¬ it.IsPlausibleStep (.skip it')) →

From 75d57290c59496353eae9a3b45b7d62a0b3bbcea Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 18:43:55 +0000
Subject: [PATCH 12/18] feat: add LawfulDeterministicIterator instances for
 RxcIterator and RxoIterator

This PR adds LawfulDeterministicIterator instances for the tree map range
iterators RxcIterator and RxoIterator, complementing the existing Zipper
instance.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/Std/Data/DTreeMap/Internal/Zipper.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/Std/Data/DTreeMap/Internal/Zipper.lean b/src/Std/Data/DTreeMap/Internal/Zipper.lean
index 138648f9ffc6..7ecc8111b80c 100644
--- a/src/Std/Data/DTreeMap/Internal/Zipper.lean
+++ b/src/Std/Data/DTreeMap/Internal/Zipper.lean
@@ -487,6 +487,12 @@ def RxcIterator.FinitenessRelation [Ord α] : FinitenessRelation (RxcIterator α
 public instance instFinite [Ord α] : Finite (RxcIterator α β) Id :=
   .of_finitenessRelation RxcIterator.FinitenessRelation
 
+public instance [Ord α] : LawfulDeterministicIterator (RxcIterator α β) Id where
+  isPlausibleStep_eq_eq it := ⟨it.internalState.step, by
+    ext step
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorRxcIteratorIdSigma,
+      eq_comm]⟩
+
 @[simp]
 theorem RxcIterator.step_done [Ord α] {upper : α} : ({ iter := .done, upper := upper } : RxcIterator α β).step = .done := rfl
 
@@ -616,6 +622,12 @@ def RxoIterator.instFinitenessRelation [Ord α] : FinitenessRelation (RxoIterato
 public instance Rxo.instFinite [Ord α] : Finite (RxoIterator α β) Id :=
   .of_finitenessRelation RxoIterator.instFinitenessRelation
 
+public instance [Ord α] : LawfulDeterministicIterator (RxoIterator α β) Id where
+  isPlausibleStep_eq_eq it := ⟨it.internalState.step, by
+    ext step
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorRxoIteratorIdSigma,
+      eq_comm]⟩
+
 @[simp]
 theorem RxoIterator.step_done [Ord α] {upper : α} : ({ iter := .done, upper := upper } : RxoIterator α β).step = .done := rfl
 

From 67c0d1e1e10a8caf29107bbbea69d454da9e4a77 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 19:53:54 +0100
Subject: [PATCH 13/18] cleanups

---
 .../Lemmas/Combinators/FilterMap.lean         | 110 ++++++++----------
 .../Iterators/Lemmas/Combinators/FlatMap.lean |  42 +++++--
 .../Data/Iterators/Lemmas/Producers/List.lean |  40 +++----
 .../DHashMap/Internal/AssocList/Iterator.lean |  45 +++----
 src/Std/Data/DTreeMap/Internal/Zipper.lean    |   2 +-
 .../Lemmas/Combinators/StepSize.lean          |   4 +-
 .../Iterators/Lemmas/Producers/Array.lean     |  48 ++++----
 7 files changed, 151 insertions(+), 140 deletions(-)

diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
index 0c86afaaa771..d197aa3719cf 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
@@ -1063,11 +1063,10 @@ private theorem PostconditionT.map_some_pure_property' {v : Option γ} {x : γ}
     (h : (PostconditionT.map some (PostconditionT.pure (m := Id) x)).Property v) : v = some x := by
   obtain ⟨⟨a, ha⟩, rfl⟩ := h; congr 1; exact ha.symm
 
-instance instLawfulDeterministicIteratorFilterMapPure
-    {lift : ⦃α : Type w⦄ → Id α → Id α}
-    {f : β → Option γ} :
+private theorem instLawfulDeterministicIteratorFilterMap
+    {lift : ⦃α : Type w⦄ → Id α → Id α} {f : β → PostconditionT Id (Option γ)} (h : ∀ b, Subsingleton (Subtype (f b).Property)) :
     LawfulDeterministicIterator
-      (Iterators.Types.FilterMap α Id Id lift (fun b => pure (f b))) Id where
+      (Iterators.Types.FilterMap α Id Id lift f) Id where
   isPlausibleStep_eq_eq it := by
     obtain ⟨innerStep, hinner⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq
       it.internalState.inner
@@ -1076,101 +1075,92 @@ instance instLawfulDeterministicIteratorFilterMapPure
       exact ⟨.done, by
         ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
         constructor
-        · intro h; cases h with
+        · intro h
+          cases h with
           | done h => rfl
           | yieldNone h => rw [hinner] at h; cases h
           | yieldSome h => rw [hinner] at h; cases h
           | skip h => rw [hinner] at h; cases h
-        · intro h; cases h; exact .done (by rw [hinner])⟩
+        · intro h
+          cases h
+          exact .done (by rw [hinner])⟩
     | skip it' =>
       exact ⟨.skip (IterM.InternalCombinators.filterMap lift _ it'), by
         ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
         constructor
-        · intro h; cases h with
+        · intro h
+          cases h with
           | skip h => rw [hinner] at h; cases h; rfl
           | done h => rw [hinner] at h; cases h
           | yieldNone h => rw [hinner] at h; cases h
           | yieldSome h => rw [hinner] at h; cases h
-        · intro h; cases h; exact .skip (by rw [hinner])⟩
+        · intro h
+          cases h
+          exact .skip (by rw [hinner])⟩
     | yield it' out =>
-      cases hfout : f out with
+      cases hfout : (f out).operation.run.val with
       | none =>
         exact ⟨.skip (IterM.InternalCombinators.filterMap lift _ it'), by
           ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
-          · intro h; cases h with
+          · intro h
+            cases h with
             | yieldNone h hp =>
               rw [hinner] at h; cases h; rfl
             | yieldSome h hp =>
               rw [hinner] at h; cases h
-              rw [hfout] at hp; cases hp
+              have : (f out).Property none := hfout ▸ (f out).operation.run.property
+              cases (h out).allEq ⟨none, this⟩ ⟨some _, hp⟩
             | skip h => rw [hinner] at h; cases h
             | done h => rw [hinner] at h; cases h
           · intro h; cases h
-            exact .yieldNone (by rw [hinner]) (show f out = none from hfout)⟩
+            exact .yieldNone (by rw [hinner]) (hfout ▸ (f out).operation.run.property)⟩
       | some out' =>
+        replace hfout : (f out).Property (some out') := hfout ▸ (f out).operation.run.property
         exact ⟨.yield (IterM.InternalCombinators.filterMap lift _ it') out', by
           ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
-          · intro h; cases h with
+          · intro h
+            cases h with
             | yieldSome h hp =>
               rw [hinner] at h; cases h
-              rw [hfout] at hp; cases hp; rfl
+              cases (h out).allEq ⟨_, hfout⟩ ⟨_, hp⟩
+              simp
             | yieldNone h hp =>
               rw [hinner] at h; cases h
-              rw [hfout] at hp; cases hp
+              cases (h out).allEq ⟨_, hfout⟩ ⟨_, hp⟩
             | skip h => rw [hinner] at h; cases h
             | done h => rw [hinner] at h; cases h
-          · intro h; cases h
-            exact .yieldSome (by rw [hinner]) (show f out = some out' from hfout)⟩
+          · intro h
+            cases h
+            exact .yieldSome (by rw [hinner]) hfout⟩
+
+instance instLawfulDeterministicIteratorFilterMapPure
+    {lift : ⦃α : Type w⦄ → Id α → Id α}
+    {f : β → Option γ} :
+    LawfulDeterministicIterator
+      (Iterators.Types.FilterMap α Id Id lift (fun b => pure (f b))) Id := by
+  apply instLawfulDeterministicIteratorFilterMap
+  intro b
+  simp only [PostconditionT.property_pure]
+  apply Subsingleton.intro
+  intro ⟨x, hx⟩ ⟨y, hy⟩
+  cases hx; cases hy
+  rfl
 
 instance instLawfulDeterministicIteratorMapPure
     {lift : ⦃α : Type w⦄ → Id α → Id α}
     {f : β → γ} :
     LawfulDeterministicIterator
-      (Iterators.Types.Map α Id Id lift (fun b => pure (f b))) Id where
-  isPlausibleStep_eq_eq it := by
-    obtain ⟨innerStep, hinner⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq
-      it.internalState.inner
-    cases innerStep with
-    | done =>
-      exact ⟨.done, by
-        ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
-        constructor
-        · intro h; cases h with
-          | done h => rfl
-          | yieldNone h => rw [hinner] at h; cases h
-          | yieldSome h => rw [hinner] at h; cases h
-          | skip h => rw [hinner] at h; cases h
-        · intro h; cases h; exact .done (by rw [hinner])⟩
-    | skip it' =>
-      exact ⟨.skip (IterM.InternalCombinators.filterMap lift _ it'), by
-        ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
-        constructor
-        · intro h; cases h with
-          | skip h => rw [hinner] at h; cases h; rfl
-          | done h => rw [hinner] at h; cases h
-          | yieldNone h => rw [hinner] at h; cases h
-          | yieldSome h => rw [hinner] at h; cases h
-        · intro h; cases h; exact .skip (by rw [hinner])⟩
-    | yield it' out =>
-      exact ⟨.yield (IterM.InternalCombinators.filterMap lift _ it') (f out), by
-        ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
-        constructor
-        · intro h; cases h with
-          | yieldSome h hp =>
-            rw [hinner] at h; cases h
-            have := PostconditionT.map_some_pure_property' hp
-            cases this; rfl
-          | yieldNone h hp =>
-            rw [hinner] at h; cases h
-            have := PostconditionT.map_some_pure_property' hp
-            cases this
-          | skip h => rw [hinner] at h; cases h
-          | done h => rw [hinner] at h; cases h
-        · intro h; cases h
-          refine .yieldSome (by rw [hinner]) ?_
-          exact ⟨⟨f out, rfl⟩, rfl⟩⟩
+      (Iterators.Types.Map α Id Id lift (fun b => pure (f b))) Id := by
+  apply instLawfulDeterministicIteratorFilterMap
+  intro b
+  simp only [PostconditionT.map_eq_pure_bind, PostconditionT.pure_bind, Function.comp_apply,
+    PostconditionT.property_pure]
+  apply Subsingleton.intro
+  intro ⟨x, hx⟩ ⟨y, hy⟩
+  cases hx; cases hy
+  rfl
 
 end LawfulDeterministic
 
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
index b44153620eb4..f37bd1d86bb3 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
@@ -284,31 +284,40 @@ instance instLawfulDeterministicIteratorFlatten
       cases outerStep with
       | done =>
         exact ⟨.done, by
-          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          ext step
+          simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
           · intro h; cases h with
             | outerDone h => rfl
             | outerYield h => rw [houter] at h; cases h
             | outerSkip h => rw [houter] at h; cases h
-          · intro h; cases h; exact .outerDone (by rw [houter])⟩
+          · intro h
+            cases h
+            exact .outerDone (by rw [houter])⟩
       | skip it₁' =>
         exact ⟨.skip ⟨⟨it₁', none⟩⟩, by
-          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          ext step
+          simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
           · intro h; cases h with
             | outerSkip h => rw [houter] at h; cases h; rfl
             | outerDone h => rw [houter] at h; cases h
             | outerYield h => rw [houter] at h; cases h
-          · intro h; cases h; exact .outerSkip (by rw [houter])⟩
+          · intro h
+            cases h
+            exact .outerSkip (by rw [houter])⟩
       | yield it₁' it₂' =>
         exact ⟨.skip ⟨⟨it₁', some it₂'⟩⟩, by
-          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          ext step
+          simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
           · intro h; cases h with
             | outerYield h => rw [houter] at h; cases h; rfl
             | outerDone h => rw [houter] at h; cases h
             | outerSkip h => rw [houter] at h; cases h
-          · intro h; cases h; exact .outerYield (by rw [houter])⟩
+          · intro h
+            cases h
+            exact .outerYield (by rw [houter])⟩
     | some it₂ =>
       obtain ⟨innerStep, hinner⟩ := LawfulDeterministicIterator.isPlausibleStep_eq_eq it₂
       cases innerStep with
@@ -316,29 +325,38 @@ instance instLawfulDeterministicIteratorFlatten
         exact ⟨.skip ⟨⟨it₁, none⟩⟩, by
           ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
-          · intro h; cases h with
+          · intro h
+            cases h with
             | innerDone h => rfl
             | innerYield h => rw [hinner] at h; cases h
             | innerSkip h => rw [hinner] at h; cases h
-          · intro h; cases h; exact .innerDone (by rw [hinner])⟩
+          · intro h
+            cases h
+            exact .innerDone (by rw [hinner])⟩
       | skip it₂' =>
         exact ⟨.skip ⟨⟨it₁, some it₂'⟩⟩, by
-          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          ext step
+          simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
           · intro h; cases h with
             | innerSkip h => rw [hinner] at h; cases h; rfl
             | innerDone h => rw [hinner] at h; cases h
             | innerYield h => rw [hinner] at h; cases h
-          · intro h; cases h; exact .innerSkip (by rw [hinner])⟩
+          · intro h
+            cases h
+            exact .innerSkip (by rw [hinner])⟩
       | yield it₂' b =>
         exact ⟨.yield ⟨⟨it₁, some it₂'⟩⟩ b, by
-          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          ext step
+          simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
           · intro h; cases h with
             | innerYield h => rw [hinner] at h; cases h; rfl
             | innerDone h => rw [hinner] at h; cases h
             | innerSkip h => rw [hinner] at h; cases h
-          · intro h; cases h; exact .innerYield (by rw [hinner])⟩
+          · intro h
+            cases h
+            exact .innerYield (by rw [hinner])⟩
 
 end LawfulDeterministic
 
diff --git a/src/Init/Data/Iterators/Lemmas/Producers/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/List.lean
index 460960ef90f1..bbd484e03ddb 100644
--- a/src/Init/Data/Iterators/Lemmas/Producers/List.lean
+++ b/src/Init/Data/Iterators/Lemmas/Producers/List.lean
@@ -23,26 +23,6 @@ open Std Std.Iterators
 
 variable {β : Type w}
 
-instance : LawfulDeterministicIterator (Iterators.Types.ListIterator β) Id where
-  isPlausibleStep_eq_eq it := by
-    rcases it with ⟨⟨_ | ⟨x, xs⟩⟩⟩
-    · exact ⟨.done, by
-        ext step
-        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-          Iterators.Types.ListIterator.instIterator]
-        cases step <;> simp⟩
-    · exact ⟨.yield ⟨⟨xs⟩⟩ x, by
-        ext step
-        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-          Iterators.Types.ListIterator.instIterator]
-        cases step with
-        | yield it' out =>
-          constructor
-          · intro h; rcases it' with ⟨⟨l⟩⟩; simp_all
-          · intro h; cases h; rfl
-        | skip => simp
-        | done => simp⟩
-
 @[simp]
 theorem List.step_iter_nil :
     (([] : List β).iter).step = ⟨.done, rfl⟩ := by
@@ -67,3 +47,23 @@ theorem List.toList_iter {l : List β} :
 theorem List.toListRev_iter {l : List β} :
     l.iter.toListRev = l.reverse := by
   simp [List.iter, Iter.toListRev_eq_toListRev_toIterM, List.toListRev_iterM]
+
+instance : LawfulDeterministicIterator (Iterators.Types.ListIterator β) Id where
+  isPlausibleStep_eq_eq it := by
+    rcases it with ⟨⟨_ | ⟨x, xs⟩⟩⟩
+    · exact ⟨.done, by
+        ext step
+        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          Iterators.Types.ListIterator.instIterator] -- TODO: remove `inst...` argument as soon as possible
+        cases step <;> simp⟩
+    · exact ⟨.yield ⟨⟨xs⟩⟩ x, by
+        ext step
+        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          Iterators.Types.ListIterator.instIterator] -- TODO: remove `inst...` argument as soon as possible
+        cases step with
+        | yield it' out =>
+          constructor
+          · intro h; rcases it' with ⟨⟨l⟩⟩; simp_all
+          · intro h; cases h; rfl
+        | skip => simp
+        | done => simp⟩
diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
index 165f3a9b1126..89ff3679c5c9 100644
--- a/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
+++ b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
@@ -34,27 +34,6 @@ public instance : Iterator (α := AssocListIterator α β) Id ((a : α) × β a)
         | ⟨⟨.nil⟩⟩ => .deflate ⟨.done, rfl⟩
         | ⟨⟨.cons k v l⟩⟩ => .deflate ⟨.yield ⟨⟨l⟩⟩ ⟨k, v⟩, rfl⟩)
 
-public instance : LawfulDeterministicIterator (AssocListIterator α β) Id where
-  isPlausibleStep_eq_eq it := by
-    rcases it with ⟨⟨_ | ⟨k, v, l⟩⟩⟩
-    · exact ⟨.done, by
-        ext step
-        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-          instIteratorAssocListIteratorIdSigma]
-        cases step <;> simp⟩
-    · exact ⟨.yield ⟨⟨l⟩⟩ ⟨k, v⟩, by
-        ext step
-        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-          instIteratorAssocListIteratorIdSigma]
-        cases step with
-        | yield it' out =>
-          constructor
-          · intro h; rcases it' with ⟨⟨l'⟩⟩; rcases out with ⟨k', v'⟩
-            cases h; rfl
-          · intro h; cases h; rfl
-        | skip => simp
-        | done => simp⟩
-
 def AssocListIterator.finitenessRelation :
     FinitenessRelation (AssocListIterator α β) Id where
   Rel := InvImage WellFoundedRelation.rel (AssocListIterator.l ∘ IterM.internalState)
@@ -79,4 +58,28 @@ public def iter {α : Type u} {β : α → Type v} (l : AssocList α β) :
     Iter (α := AssocListIterator α β) ((a : α) × β a) :=
   ⟨⟨l⟩⟩
 
+public instance : LawfulDeterministicIterator (AssocListIterator α β) Id where
+  isPlausibleStep_eq_eq it := by
+    rcases it with ⟨⟨_ | ⟨k, v, l⟩⟩⟩
+    · exact ⟨.done, by
+        ext step
+        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          instIteratorAssocListIteratorIdSigma] -- TODO: remove `inst...` argument as soon as possible
+        cases step <;> simp⟩
+    · exact ⟨.yield ⟨⟨l⟩⟩ ⟨k, v⟩, by
+        ext step
+        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+          instIteratorAssocListIteratorIdSigma] -- TODO: remove `inst...` argument as soon as possible
+        cases step with
+        | yield it' out =>
+          constructor
+          · intro h
+            rcases it' with ⟨⟨l'⟩⟩
+            rcases out with ⟨k', v'⟩
+            cases h
+            rfl
+          · intro h; cases h; rfl
+        | skip => simp
+        | done => simp⟩
+
 end Std.DHashMap.Internal.AssocList
diff --git a/src/Std/Data/DTreeMap/Internal/Zipper.lean b/src/Std/Data/DTreeMap/Internal/Zipper.lean
index 7ecc8111b80c..abe022ecc7d8 100644
--- a/src/Std/Data/DTreeMap/Internal/Zipper.lean
+++ b/src/Std/Data/DTreeMap/Internal/Zipper.lean
@@ -341,7 +341,7 @@ public instance : LawfulDeterministicIterator (Zipper α β) Id where
   isPlausibleStep_eq_eq it := ⟨it.internalState.step, by
     ext step
     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorZipperIdSigma,
-      eq_comm]⟩
+      eq_comm]⟩ -- TODO: remove `inst...` argument as soon as possible
 
 def Zipper.FinitenessRelation : FinitenessRelation (Zipper α β) Id where
   Rel t' t := t'.internalState.size < t.internalState.size
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
index 23a8dc7dd270..0940cc65798b 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -279,14 +279,14 @@ theorem atIdxSlow?_stepSize [Iterator α Id β] [Productive α Id]
     (it.stepSize n).atIdxSlow? k = it.atIdxSlow? ((n - 1 + 1) * k) := by
   simp [stepSize_eq_intermediateStepSize, atIdxSlow?_intermediate_stepSize]
 
-theorem getElem?_toList_stepSize [Iterator α Id β] [Productive α Id]
+theorem getElem?_toList_stepSize [Iterator α Id β]
     [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] [Finite α Id]
     {it : Iter (α := α) β} {k n : Nat} :
     (it.stepSize n).toList[k]? = it.toList[(n - 1 + 1) * k]? := by
   simp only [getElem?_toList_eq_atIdxSlow?, atIdxSlow?_stepSize]
 
-theorem getElem?_toArray_stepSize [Iterator α Id β] [Productive α Id]
+theorem getElem?_toArray_stepSize [Iterator α Id β]
     [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] [Finite α Id]
     {it : Iter (α := α) β} {k n : Nat} :
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
index 28c85e8d353a..fb0819f4967d 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
@@ -27,30 +27,6 @@ open Std Std.Iterators
 
 variable {β : Type w}
 
-instance : LawfulDeterministicIterator (Iterators.Types.ArrayIterator β) Id where
-  isPlausibleStep_eq_eq it := by
-    rcases it with ⟨⟨array, pos⟩⟩
-    refine if h : pos < array.size then ?_ else ?_
-    · exact ⟨.yield ⟨⟨array, pos + 1⟩⟩ array[pos], by
-        ext step
-        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-          Iterators.Types.ArrayIterator.instIterator]
-        cases step with
-        | yield it' out =>
-          constructor
-          · rintro ⟨ha, hp, hlt, hv⟩; rcases it' with ⟨⟨a', p'⟩⟩; simp_all
-          · intro heq; cases heq; exact ⟨rfl, rfl, h, rfl⟩
-        | skip => simp
-        | done => simp; omega⟩
-    · exact ⟨.done, by
-        ext step
-        simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
-          Iterators.Types.ArrayIterator.instIterator]
-        cases step with
-        | yield => simp; intro _ _ hlt; omega
-        | skip => simp
-        | done => simp; omega⟩
-
 theorem Array.iter_eq_toIter_iterM {array : Array β} :
     array.iter = (array.iterM Id).toIter :=
   rfl
@@ -140,3 +116,27 @@ theorem Array.iter_equiv_iter_toList {α : Type w} {array : Array α} :
   simpa using iterFromIdx_equiv_iter_drop_toList
 
 end Equivalence
+
+instance : LawfulDeterministicIterator (Iterators.Types.ArrayIterator β) Id where
+  isPlausibleStep_eq_eq it := by
+    rcases it with ⟨⟨array, pos⟩⟩
+    refine if h : pos < array.size then ?_ else ?_
+    · exact ⟨.yield ⟨⟨array, pos + 1⟩⟩ array[pos], by
+          ext step
+          simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+            Iterators.Types.ArrayIterator.instIterator] -- TODO: remove `inst...` argument as soon as possible
+          cases step with
+          | yield it' out =>
+            constructor
+            · rintro ⟨ha, hp, hlt, hv⟩; rcases it' with ⟨⟨a', p'⟩⟩; simp_all
+            · intro heq; cases heq; exact ⟨rfl, rfl, h, rfl⟩
+          | skip => simp
+          | done => simp; omega⟩
+    · exact ⟨.done, by
+          ext step
+          simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep,
+            Iterators.Types.ArrayIterator.instIterator] -- TODO: remove `inst...` argument as soon as possible
+          cases step with
+          | yield => simp; omega
+          | skip => simp
+          | done => simp; omega⟩

From a08d5a5f8e2e814c872acc2fbfc542558ba99bb7 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 19:54:55 +0100
Subject: [PATCH 14/18] add todos

---
 src/Std/Data/DTreeMap/Internal/Zipper.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Std/Data/DTreeMap/Internal/Zipper.lean b/src/Std/Data/DTreeMap/Internal/Zipper.lean
index abe022ecc7d8..583294806b5c 100644
--- a/src/Std/Data/DTreeMap/Internal/Zipper.lean
+++ b/src/Std/Data/DTreeMap/Internal/Zipper.lean
@@ -491,7 +491,7 @@ public instance [Ord α] : LawfulDeterministicIterator (RxcIterator α β) Id wh
   isPlausibleStep_eq_eq it := ⟨it.internalState.step, by
     ext step
     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorRxcIteratorIdSigma,
-      eq_comm]⟩
+      eq_comm]⟩ -- TODO: remove `inst...` argument as soon as possible
 
 @[simp]
 theorem RxcIterator.step_done [Ord α] {upper : α} : ({ iter := .done, upper := upper } : RxcIterator α β).step = .done := rfl
@@ -626,7 +626,7 @@ public instance [Ord α] : LawfulDeterministicIterator (RxoIterator α β) Id wh
   isPlausibleStep_eq_eq it := ⟨it.internalState.step, by
     ext step
     simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIteratorRxoIteratorIdSigma,
-      eq_comm]⟩
+      eq_comm]⟩ -- TODO: remove `inst...` argument as soon as possible
 
 @[simp]
 theorem RxoIterator.step_done [Ord α] {upper : α} : ({ iter := .done, upper := upper } : RxoIterator α β).step = .done := rfl

From a60be4e9921a1ef7509dace82913054782384656 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 20:40:33 +0100
Subject: [PATCH 15/18] cleanups

---
 .../Iterators/Lemmas/Consumers/Access.lean    |  17 +++
 .../Iterators/Lemmas/Consumers/Monadic.lean   |   1 +
 .../Lemmas/Consumers/Monadic/Access.lean      |  40 ++++++
 .../Lemmas/Combinators/Monadic/StepSize.lean  |  57 ++++++++
 .../Lemmas/Combinators/StepSize.lean          | 124 ++----------------
 5 files changed, 123 insertions(+), 116 deletions(-)

diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
index 1150800e5917..f55bb3553a4d 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
@@ -99,4 +99,21 @@ public theorem length_le_of_nextAtIdxSlow?_eq_done [Iterator α Id β] [Finite 
       simp only
       omega
 
+public theorem nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
+    it.nextAtIdx? n = it.nextAtIdxSlow? n := by
+  simp [Iter.nextAtIdx?, Iter.nextAtIdxSlow?, IterM.nextAtIdx?_eq_nextAtIdxSlow?]
+
+public theorem length_nextAtIdxSlow? [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} :
+    (it.nextAtIdxSlow? n).val.successor.elim 0 Iter.length = it.length - n - 1 := by
+  have := IterM.length_nextAtIdxSlow? (it := it.toIterM) (n := n)
+  replace this := congrArg (fun x => ULift.down (Id.run x)) this
+  simp only [Id.run_bind, Id.run_map] at this
+  simp only [nextAtIdxSlow?, length, ← this]
+  split at this
+  · simpa [Option.elim, *]
+  · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
+  · simp [Option.elim, *]
+
 end Std.Iter
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean
index 590aa8908d7a..5cc1527d2b68 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean
@@ -8,3 +8,4 @@ module
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Access
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
index d28251be41f1..a7c49c35236a 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Iterators.Consumers.Monadic.Access
 import all Init.Data.Iterators.Consumers.Monadic.Access
 public import Init.Data.Iterators.Consumers.Monadic.Loop
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 public import Init.Control.Lawful.Basic
 import Init.Control.Lawful.Lemmas
 
@@ -140,3 +141,42 @@ public theorem nextAtIdxSlow?_add_one [Monad m] [LawfulMonad m] [Iterator α m 
       | .skip _ hp => not_isPlausibleNthOutputStep_skip.elim hp
       | .done hp => return ⟨.done, isPlausibleNthOutputStep_trans_of_done (k := 0) hp (Nat.zero_le _)⟩) := by
   rw [nextAtIdxSlow?_eq_match_nextAtIdxSlow?]
+
+public local instance instSubsingletonPlausibleIterStepIsPlausibleNthOutputStep [Iterator α Id β]
+    [LawfulDeterministicIterator α Id] {it : IterM (α := α) Id β} :
+    Subsingleton (PlausibleIterStep (it.IsPlausibleNthOutputStep n)) where
+  allEq s s' := by
+    obtain ⟨s, hs⟩ := s
+    obtain ⟨s', hs'⟩ := s'
+    have := hs.unique hs'
+    rwa [Subtype.mk.injEq]
+
+public theorem nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id]
+    [LawfulDeterministicIterator α Id] [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
+    it.nextAtIdx? n = it.nextAtIdxSlow? n := by
+  apply Id.ext
+  apply Subsingleton.allEq
+
+public theorem length_nextAtIdxSlow? [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} :
+    (do match ← it.nextAtIdxSlow? n with
+      | .yield it' _out _ => it'.length
+      | .skip _it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
+      | .done _h => return .up 0) = (fun len => .up (len.down - n - 1)) <$> it.length := by
+  induction it using IterM.inductSteps generalizing n with | step it ihy ihs
+  rw [it.nextAtIdxSlow?_eq_match, it.length_eq_match_step]
+  simp only [map_eq_pure_bind, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp only [bind_pure_comp, Functor.map_map]
+    split
+    · simp only [pure_bind, Nat.sub_zero, Nat.add_one_sub_one, id_map']
+    · simp only [Nat.succ_eq_add_one, Nat.add_sub_add_right, bind_map_left]
+      rw [← ihy ‹_›]
+      apply bind_congr; intro step
+      cases step using PlausibleIterStep.casesOn <;> simp [Not.elim, absurd]
+  · simp only [bind_pure_comp, bind_map_left, id_map']
+    rw [← ihs ‹_›]
+    apply bind_congr; intro step
+    cases step using PlausibleIterStep.casesOn <;> simp [Not.elim, absurd]
+  · simp
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean
index 9eddfd7bd5a9..178d70635820 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean
@@ -7,11 +7,68 @@ module
 
 prelude
 public import Std.Data.Iterators.Combinators.Monadic.StepSize
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Access
+import all Init.Data.Iterators.Consumers.Monadic.Access
+import Init.Classical
 
 public section
 open Std Std.Iterators Std.Iterators.Types
 
 namespace Std.IterM
 
+instance instLawfulDeterministicIteratorStepSizeIterator
+    [Iterator α Id β] [LawfulDeterministicIterator α Id] [IteratorAccess α Id] :
+    LawfulDeterministicIterator (Types.StepSizeIterator α Id β) Id where
+  isPlausibleStep_eq_eq it := by
+    refine ⟨it.step.run.inflate.val, ?_⟩
+    have hp := it.step.run.inflate.property
+    ext step
+    constructor
+    · intro ⟨h₁, h₂⟩
+      obtain ⟨hp₁, hp₂⟩ := hp
+      simp only [IterStep.mapIterator] at h₁ hp₁
+      have heq := h₁.unique hp₁
+      generalize it.step.run.inflate.val = cstep at heq hp₁ hp₂ ⊢
+      cases step with
+      | skip _ => exact IterM.not_isPlausibleNthOutputStep_skip.elim (by simpa using h₁)
+      | done =>
+        cases cstep with
+        | done => simp
+        | yield _ _ => simp at heq
+        | skip _ => exact IterM.not_isPlausibleNthOutputStep_skip.elim (by simpa using hp₁)
+      | yield it₁ out₁ =>
+        cases cstep with
+        | done => simp at heq
+        | skip _ => exact IterM.not_isPlausibleNthOutputStep_skip.elim (by simpa using hp₁)
+        | yield it₂ out₂ =>
+          rcases it₁ with ⟨⟨_, _, _⟩⟩
+          rcases it₂ with ⟨⟨_, _, _⟩⟩
+          simp_all
+    · simpa +contextual using fun _ => hp
+
+theorem nextAtIdxSlow?_stepSize_aux [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
+    [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
+    (IterM.Intermediate.stepSize it i n).nextAtIdxSlow? 0 = (do
+      match (← it.nextAtIdxSlow? i) with
+      | .yield it' out h =>
+        return .yield (IterM.Intermediate.stepSize it' (n - 1) n) out (by
+          refine .zero_yield ?_
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, IterM.Intermediate.stepSize,
+            IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) -- TODO: remove `inst...` argument as soon as possible
+      | .skip it' h => return IterM.not_isPlausibleNthOutputStep_skip.elim h
+      | .done h =>
+        return .done (by
+          refine .done ?_
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Intermediate.stepSize,
+            IterM.Intermediate.stepSize, StepSizeIterator.instIterator])) := by -- TODO: remove `inst...` argument as soon as possible
+  induction it, i using IterM.atIdxSlow?.induct_unfolding
+  rw [IterM.nextAtIdxSlow?_eq_match]
+  simp only [IterM.Intermediate.stepSize, IterM.step_eq, IterM.internalState_mk,
+    IterM.nextAtIdx?_eq_nextAtIdxSlow?, bind_pure_comp, bind_map_left, Shrink.inflate_deflate]
+  apply bind_congr; intro step
+  cases step using PlausibleIterStep.casesOn
+  · simp
+  · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
+  · simp
 
 end Std.IterM
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
index 0940cc65798b..9a2fc4690231 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -13,7 +13,9 @@ public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Combinators.Take
 public import Std.Data.Iterators.Combinators.StepSize
 import all Std.Data.Iterators.Combinators.StepSize
+import Std.Data.Iterators.Lemmas.Combinators.Monadic.StepSize
 import Init.Data.Iterators.Lemmas.Consumers.Access
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Access
 import Init.Data.Iterators.Lemmas.Consumers.Collect
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Access
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
@@ -32,116 +34,6 @@ theorem stepSize_eq_intermediateStepSize [Iterator α Id β] [IteratorAccess α
     it.stepSize n = Intermediate.stepSize it 0 n :=
   rfl
 
-instance [Iterator α Id β] [LawfulDeterministicIterator α Id] {it : IterM (α := α) Id β} :
-    Subsingleton (PlausibleIterStep (it.IsPlausibleNthOutputStep n)) where
-  allEq s s' := by
-    obtain ⟨s, hs⟩ := s
-    obtain ⟨s', hs'⟩ := s'
-    have := hs.unique hs'
-    rwa [Subtype.mk.injEq]
-
-instance instLawfulDeterministicIteratorStepSizeIterator
-    [Iterator α Id β] [LawfulDeterministicIterator α Id] [IteratorAccess α Id] :
-    LawfulDeterministicIterator (Types.StepSizeIterator α Id β) Id where
-  isPlausibleStep_eq_eq it := by
-    refine ⟨it.step.run.inflate.val, ?_⟩
-    have hp := it.step.run.inflate.property
-    ext step
-    constructor
-    · intro ⟨h₁, h₂⟩
-      obtain ⟨hp₁, hp₂⟩ := hp
-      simp only [IterStep.mapIterator] at h₁ hp₁
-      have heq := h₁.unique hp₁
-      generalize it.step.run.inflate.val = cstep at heq hp₁ hp₂ ⊢
-      cases step with
-      | skip _ => exact IterM.not_isPlausibleNthOutputStep_skip.elim (by simpa using h₁)
-      | done =>
-        cases cstep with
-        | done => simp
-        | yield _ _ => simp at heq
-        | skip _ => exact IterM.not_isPlausibleNthOutputStep_skip.elim (by simpa using hp₁)
-      | yield it₁ out₁ =>
-        cases cstep with
-        | done => simp at heq
-        | skip _ => exact IterM.not_isPlausibleNthOutputStep_skip.elim (by simpa using hp₁)
-        | yield it₂ out₂ =>
-          rcases it₁ with ⟨⟨_, _, _⟩⟩
-          rcases it₂ with ⟨⟨_, _, _⟩⟩
-          simp_all
-    · simpa +contextual using fun _ => hp
-
-theorem _root_.Std.IterM.nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id]
-    [LawfulDeterministicIterator α Id] [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
-    it.nextAtIdx? n = it.nextAtIdxSlow? n := by
-  apply Id.ext
-  apply Subsingleton.allEq
-
-theorem nextAtIdx?_eq_nextAtIdxSlow? [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
-    [IteratorAccess α Id] {it : Iter (α := α) β} {n : Nat} :
-    it.nextAtIdx? n = it.nextAtIdxSlow? n := by
-  simp [Iter.nextAtIdx?, Iter.nextAtIdxSlow?, IterM.nextAtIdx?_eq_nextAtIdxSlow?]
-
-theorem _root_.Std.IterM.nextAtIdxSlow?_stepSize_aux [Iterator α Id β] [Productive α Id] [LawfulDeterministicIterator α Id]
-    [IteratorAccess α Id] {it : IterM (α := α) Id β} {n : Nat} :
-    (IterM.Intermediate.stepSize it i n).nextAtIdxSlow? 0 = (do
-      match (← it.nextAtIdxSlow? i) with
-      | .yield it' out h =>
-        return .yield (IterM.Intermediate.stepSize it' (n - 1) n) out (by
-          refine .zero_yield ?_
-          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, IterM.Intermediate.stepSize,
-            IterM.Intermediate.stepSize, StepSizeIterator.instIterator]) -- TODO: remove `inst...` argument as soon as possible
-      | .skip it' h => return IterM.not_isPlausibleNthOutputStep_skip.elim h
-      | .done h =>
-        return .done (by
-          refine .done ?_
-          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, Intermediate.stepSize,
-            IterM.Intermediate.stepSize, StepSizeIterator.instIterator])) := by -- TODO: remove `inst...` argument as soon as possible
-  induction it, i using IterM.atIdxSlow?.induct_unfolding
-  rw [IterM.nextAtIdxSlow?_eq_match]
-  simp only [IterM.Intermediate.stepSize, IterM.step_eq, IterM.internalState_mk,
-    IterM.nextAtIdx?_eq_nextAtIdxSlow?, bind_pure_comp, bind_map_left, Shrink.inflate_deflate]
-  apply bind_congr; intro step
-  cases step using PlausibleIterStep.casesOn
-  · simp
-  · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
-  · simp
-
-theorem _root_.Std.IterM.length_nextAtIdxSlow? [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
-    {it : IterM (α := α) m β} :
-    (do match ← it.nextAtIdxSlow? n with
-      | .yield it' _out _ => it'.length
-      | .skip _it' h => IterM.not_isPlausibleNthOutputStep_skip.elim h
-      | .done _h => return .up 0) = (fun len => .up (len.down - n - 1)) <$> it.length := by
-  induction it using IterM.inductSteps generalizing n with | step it ihy ihs
-  rw [it.nextAtIdxSlow?_eq_match, it.length_eq_match_step]
-  simp only [map_eq_pure_bind, bind_assoc]
-  apply bind_congr; intro step
-  cases step.inflate using PlausibleIterStep.casesOn
-  · simp only [bind_pure_comp, Functor.map_map]
-    split
-    · simp only [pure_bind, Nat.sub_zero, Nat.add_one_sub_one, id_map']
-    · simp only [Nat.succ_eq_add_one, Nat.add_sub_add_right, bind_map_left]
-      rw [← ihy ‹_›]
-      apply bind_congr; intro step
-      cases step using PlausibleIterStep.casesOn <;> simp [Not.elim, absurd]
-  · simp only [bind_pure_comp, bind_map_left, id_map']
-    rw [← ihs ‹_›]
-    apply bind_congr; intro step
-    cases step using PlausibleIterStep.casesOn <;> simp [Not.elim, absurd]
-  · simp
-
-theorem length_nextAtIdxSlow? [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
-    [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} :
-    (it.nextAtIdxSlow? n).val.successor.elim 0 Iter.length = it.length - n - 1 := by
-  have := IterM.length_nextAtIdxSlow? (it := it.toIterM) (n := n)
-  replace this := congrArg (fun x => ULift.down (Id.run x)) this
-  simp only [Id.run_bind, Id.run_map] at this
-  simp only [nextAtIdxSlow?, length, ← this]
-  split at this
-  · simpa [Option.elim, *]
-  · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
-  · simp [Option.elim, *]
-
 theorem nextAtIdxSlow?_zero_intermediate_stepSize [Iterator α Id β] [Productive α Id]
     [LawfulDeterministicIterator α Id]
     [IteratorAccess α Id] {it : Iter (α := α) β} {i n : Nat} :
@@ -176,7 +68,7 @@ private theorem atIdxSlow?_eq_of_nextAtIdxSlow? [Iterator α Id β] [Productive
   induction i, it using Iter.atIdxSlow?.induct_unfolding <;>
     (rw [nextAtIdxSlow?_eq_match]; simp [*])
 
-private theorem atIdxSlow?_none_of_nextAtIdxSlow?_done [Iterator α Id β] [Productive α Id]
+private theorem atIdxSlow?_none_of_nextAtIdxSlow?_eq_done [Iterator α Id β] [Productive α Id]
     {it : Iter (α := α) β} {i j : Nat}
     (h : (it.nextAtIdxSlow? i).val = .done) (hij : i ≤ j) :
     it.atIdxSlow? j = none := by
@@ -200,7 +92,7 @@ private theorem atIdxSlow?_none_of_nextAtIdxSlow?_done [Iterator α Id β] [Prod
       exact ih_skip hp h
     | done hp => simp
 
-private theorem atIdxSlow?_succ_of_nextAtIdxSlow?_yield [Iterator α Id β] [Productive α Id]
+private theorem atIdxSlow?_succ_of_nextAtIdxSlow?_eq_yield [Iterator α Id β] [Productive α Id]
     {it it' : Iter (α := α) β} {i j : Nat} {out : β}
     (h : (it.nextAtIdxSlow? i).val = .yield it' out) :
     it.atIdxSlow? (i + 1 + j) = it'.atIdxSlow? j := by
@@ -258,8 +150,8 @@ theorem atIdxSlow?_intermediate_stepSize {α β} [Iterator α Id β] [Productive
         rw [nextAtIdxSlow?_zero_intermediate_stepSize_val, hstep, IterStep.mapIterator]
       have h_atIdxSlow?_succ : (Intermediate.stepSize it i n).atIdxSlow? (k + 1) =
           (Intermediate.stepSize it' (n - 1) n).atIdxSlow? k := by
-        rw [show k + 1 = 0 + 1 + k by omega, ← atIdxSlow?_succ_of_nextAtIdxSlow?_yield h_nextAtIdxSlow?_zero]
-      rw [h_atIdxSlow?_succ, ih, ← atIdxSlow?_succ_of_nextAtIdxSlow?_yield hstep]
+        rw [show k + 1 = 0 + 1 + k by omega, ← atIdxSlow?_succ_of_nextAtIdxSlow?_eq_yield h_nextAtIdxSlow?_zero]
+      rw [h_atIdxSlow?_succ, ih, ← atIdxSlow?_succ_of_nextAtIdxSlow?_eq_yield hstep]
       congr 1
       rw [Nat.mul_add]
       omega
@@ -270,8 +162,8 @@ theorem atIdxSlow?_intermediate_stepSize {α β} [Iterator α Id β] [Productive
       have h_nextAtIdxSlow?_zero :
           ((Intermediate.stepSize it i n).nextAtIdxSlow? 0).val = .done := by
         rw [nextAtIdxSlow?_zero_intermediate_stepSize_val, hstep]; rfl
-      rw [atIdxSlow?_none_of_nextAtIdxSlow?_done h_nextAtIdxSlow?_zero (by omega)]
-      exact (atIdxSlow?_none_of_nextAtIdxSlow?_done hstep (by omega)).symm
+      rw [atIdxSlow?_none_of_nextAtIdxSlow?_eq_done h_nextAtIdxSlow?_zero (by omega)]
+      exact (atIdxSlow?_none_of_nextAtIdxSlow?_eq_done hstep (by omega)).symm
 
 theorem atIdxSlow?_stepSize [Iterator α Id β] [Productive α Id]
     [LawfulDeterministicIterator α Id]

From 8ecd00c9c50b4b6206d6c0ccfa27ef26f000a45a Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Sun, 1 Mar 2026 20:41:13 +0100
Subject: [PATCH 16/18] orphan module

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

diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean
index 98d3b5e1e65f..33e62ee3c032 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean
@@ -11,3 +11,4 @@ public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
+public import Std.Data.Iterators.Lemmas.Combinators.Monadic.StepSize

From 71f51b5a45f67419640a4ff1d9448c5b118dce26 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 9 Mar 2026 21:32:47 +0100
Subject: [PATCH 17/18] cleanups

---
 .../Iterators/Lemmas/Combinators/FlatMap.lean     | 15 ++++++++++-----
 .../Lemmas/Consumers/Monadic/Access.lean          | 10 ++++------
 2 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
index f37bd1d86bb3..dff4a5019960 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
@@ -287,7 +287,8 @@ instance instLawfulDeterministicIteratorFlatten
           ext step
           simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
-          · intro h; cases h with
+          · intro h
+            cases h with
             | outerDone h => rfl
             | outerYield h => rw [houter] at h; cases h
             | outerSkip h => rw [houter] at h; cases h
@@ -299,7 +300,8 @@ instance instLawfulDeterministicIteratorFlatten
           ext step
           simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
-          · intro h; cases h with
+          · intro h
+            cases h with
             | outerSkip h => rw [houter] at h; cases h; rfl
             | outerDone h => rw [houter] at h; cases h
             | outerYield h => rw [houter] at h; cases h
@@ -323,7 +325,8 @@ instance instLawfulDeterministicIteratorFlatten
       cases innerStep with
       | done =>
         exact ⟨.skip ⟨⟨it₁, none⟩⟩, by
-          ext step; simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
+          ext step
+          simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
           · intro h
             cases h with
@@ -338,7 +341,8 @@ instance instLawfulDeterministicIteratorFlatten
           ext step
           simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
-          · intro h; cases h with
+          · intro h
+            cases h with
             | innerSkip h => rw [hinner] at h; cases h; rfl
             | innerDone h => rw [hinner] at h; cases h
             | innerYield h => rw [hinner] at h; cases h
@@ -350,7 +354,8 @@ instance instLawfulDeterministicIteratorFlatten
           ext step
           simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
           constructor
-          · intro h; cases h with
+          · intro h
+            cases h with
             | innerYield h => rw [hinner] at h; cases h; rfl
             | innerDone h => rw [hinner] at h; cases h
             | innerSkip h => rw [hinner] at h; cases h
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
index a7c49c35236a..3f5b6d77378e 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
@@ -115,20 +115,18 @@ public theorem nextAtIdxSlow?_eq_match_nextAtIdxSlow? [Monad m] [LawfulMonad m]
   apply bind_congr; intro step
   cases step.inflate using PlausibleIterStep.casesOn
   · simp
-  · simp
-    simp at ih₁ ih₂
+  · simp only [bind_pure_comp, bind_map_left] at ih₁ ih₂ ⊢
     rw [ih₂]
-    · simp
+    · simp only [map_bind]
       apply bind_congr; intro step'
       split
       · simp
-      · simp
-        split
+      · split
         · simp
         · exact not_isPlausibleNthOutputStep_skip.elim ‹_›
         · simp
     · assumption
-  · simp
+  · simp only [bind_pure_comp, pure_bind]
     split <;> simp
 
 public theorem nextAtIdxSlow?_add_one [Monad m] [LawfulMonad m] [Iterator α m β] [Productive α m]

From 9f7df0ef5284534d790c9994037dbb54c766d764 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 9 Mar 2026 21:40:56 +0100
Subject: [PATCH 18/18] cleanups

---
 src/Init/Data/Iterators/Lemmas/Consumers/Access.lean      | 3 +--
 .../Data/Iterators/Lemmas/Consumers/Monadic/Access.lean   | 2 +-
 src/Std/Data/Iterators/Producers/Monadic/Array.lean       | 8 ++++----
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
index f55bb3553a4d..36947ba440c0 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
@@ -29,9 +29,8 @@ public theorem nextAtIdxSlow?_eq_match [Iterator α Id β] [Productive α Id]
         let s := it'.nextAtIdxSlow? n
         ⟨s.val, .skip hp s.property⟩
       | .done hp => .done (.done hp)) := by
-  simp [Iter.nextAtIdxSlow?]
   apply Subtype.ext
-  simp only
+  simp only [nextAtIdxSlow?]
   rw [IterM.nextAtIdxSlow?_eq_match]
   simp only [bind_pure_comp, Id.run_bind, step]
   split
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
index 3f5b6d77378e..e4c1339e8d9a 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
@@ -41,7 +41,7 @@ private theorem val_nextAtIdxSlow?Go [Monad m] [LawfulMonad m] [Iterator α m β
   apply bind_congr; intro step
   rename_i it' n' ih₁ ih₂
   cases step.inflate using PlausibleIterStep.casesOn
-  · simp
+  · simp only [bind_pure_comp]
     cases n'
     · simp
     · simp only at ih₁
diff --git a/src/Std/Data/Iterators/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
index 5c8fef0bb4e4..1c70c9263f9c 100644
--- a/src/Std/Data/Iterators/Producers/Monadic/Array.lean
+++ b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
@@ -127,19 +127,19 @@ instance : IteratorAccess (ArrayIterator α) Id where
       else
         .done
     haveI : IterM.IsPlausibleNthOutputStep n it step := by
-      simp only [step]; clear step
+      simp only [step]
       induction n generalizing it
       · split
         · refine .zero_yield ?_
-          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, ArrayIterator.instIterator, *] -- TODO
+          simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, ArrayIterator.instIterator, *] -- TODO: remove `inst...` argument as soon as possible
         · refine .done ?_
-          simp_all [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, ArrayIterator.instIterator] -- TODO
+          simp_all [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, ArrayIterator.instIterator] -- TODO: remove `inst...` argument as soon as possible
       · rename_i n ih
         by_cases h : it.internalState.pos < it.internalState.array.size
         · refine .yield (it' := ?it') (out := ?_) ?_ ?_
           · exact ⟨⟨it.internalState.array, it.internalState.pos + 1⟩⟩
           · exact it.internalState.array[it.internalState.pos]
-          · simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, ArrayIterator.instIterator] -- TODO
+          · simpa [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, ArrayIterator.instIterator] -- TODO: remove `inst...` argument as soon as possible
           · specialize ih ?it'
             simp only [Nat.add_comm 1, Nat.add_assoc] at ih ⊢
             split