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..cccb1da23263 100644
--- a/src/Init/Data/Iterators/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Access.lean
@@ -19,6 +19,45 @@ 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)
+
+/--
+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..dc76b55b69f9 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Access.lean
@@ -7,6 +7,9 @@ module
 
 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
 
@@ -46,7 +49,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
@@ -57,6 +60,89 @@ 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 ‹_›
+
+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
@@ -95,6 +181,53 @@ 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.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]
+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/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/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/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
index d90a4013d772..d197aa3719cf 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean
@@ -1055,4 +1055,113 @@ 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
+
+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 f) 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).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
+            | yieldNone h hp =>
+              rw [hinner] at h; cases h; rfl
+            | yieldSome h hp =>
+              rw [hinner] at h; cases h
+              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]) (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
+            | yieldSome h hp =>
+              rw [hinner] at h; cases h
+              cases (h out).allEq ⟨_, hfout⟩ ⟨_, hp⟩
+              simp
+            | yieldNone h hp =>
+              rw [hinner] at h; cases h
+              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]) 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 := 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
+
 end Std
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
index af874ee622f2..dff4a5019960 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
@@ -268,4 +268,101 @@ 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/Consumers/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
index 43bd0f8c9ddc..36947ba440c0 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
@@ -7,10 +7,37 @@ 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
 
+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
+  apply Subtype.ext
+  simp only [nextAtIdxSlow?]
+  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 =
@@ -23,4 +50,69 @@ 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
+
+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
new file mode 100644
index 000000000000..e4c1339e8d9a
--- /dev/null
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Access.lean
@@ -0,0 +1,180 @@
+/-
+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.Data.Iterators.Consumers.Monadic.Loop
+import Init.Data.Iterators.Lemmas.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
+      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
+  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} :
+    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 only [bind_pure_comp]
+    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 only [bind_pure_comp, bind_map_left] at ih₁ ih₂ ⊢
+    rw [ih₂]
+    · simp only [map_bind]
+      apply bind_congr; intro step'
+      split
+      · simp
+      · split
+        · simp
+        · exact not_isPlausibleNthOutputStep_skip.elim ‹_›
+        · simp
+    · assumption
+  · simp only [bind_pure_comp, pure_bind]
+    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?]
+
+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/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/Init/Data/Iterators/Lemmas/Producers/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/List.lean
index 32a61c13061d..bbd484e03ddb 100644
--- a/src/Init/Data/Iterators/Lemmas/Producers/List.lean
+++ b/src/Init/Data/Iterators/Lemmas/Producers/List.lean
@@ -47,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 e2c212224966..89ff3679c5c9 100644
--- a/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
+++ b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
@@ -58,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 46c61398b5d8..583294806b5c 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]⟩ -- TODO: remove `inst...` argument as soon as possible
+
 def Zipper.FinitenessRelation : FinitenessRelation (Zipper α β) Id where
   Rel t' t := t'.internalState.size < t.internalState.size
   wf := by
@@ -481,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]⟩ -- TODO: remove `inst...` argument as soon as possible
+
 @[simp]
 theorem RxcIterator.step_done [Ord α] {upper : α} : ({ iter := .done, upper := upper } : RxcIterator α β).step = .done := rfl
 
@@ -610,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]⟩ -- TODO: remove `inst...` argument as soon as possible
+
 @[simp]
 theorem RxoIterator.step_done [Ord α] {upper : α} : ({ iter := .done, upper := upper } : RxoIterator α β).step = .done := rfl
 
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
index 440d1cbd8399..1c2851a913f5 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 β :=
+  ⟨⟨nextIdx, n - 1, it⟩⟩
+
 namespace Iterators.Types
 
 instance StepSizeIterator.instIterator [Iterator α m β] [IteratorAccess α m] [Monad m] :
@@ -86,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
@@ -119,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/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.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
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
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..178d70635820
--- /dev/null
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/StepSize.lean
@@ -0,0 +1,74 @@
+/-
+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
+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
new file mode 100644
index 000000000000..9a2fc4690231
--- /dev/null
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/StepSize.lean
@@ -0,0 +1,250 @@
+/-
+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.Monadic.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 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
+import all Init.Data.Iterators.Consumers.Monadic.Access
+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
+
+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 =>
+        .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: 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: 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
+  let step := (it.toIterM.nextAtIdxSlow? i).run
+  cases hs : step using PlausibleIterStep.casesOn
+  · simp [hs, step]
+  · exact IterM.not_isPlausibleNthOutputStep_skip.elim ‹_›
+  · simp [hs, step]
+
+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 <;>
+    (rw [nextAtIdxSlow?_eq_match]; simp [*])
+
+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
+  induction j generalizing it i with
+  | zero =>
+    cases show i = 0 from Nat.le_antisymm hij (Nat.zero_le _)
+    rw [atIdxSlow?_eq_of_nextAtIdxSlow?, h]
+  | succ j ih =>
+    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 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 only [hstep] at h
+      exact ih_skip hp h
+    | done hp => simp
+
+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
+  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 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 = j + 1 from by omega, atIdxSlow?_eq_match]
+    simp [hs]
+  | yield_succ it it'' out' hp hs k ih =>
+    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, 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
+
+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 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?_eq_yield h_nextAtIdxSlow?_zero]
+      rw [h_atIdxSlow?_succ, ih, ← atIdxSlow?_succ_of_nextAtIdxSlow?_eq_yield hstep]
+      congr 1
+      rw [Nat.mul_add]
+      omega
+    | skip it' =>
+      exact IterM.not_isPlausibleNthOutputStep_skip.elim
+        (by simpa [hstep] using (it.nextAtIdxSlow? i).property)
+    | done =>
+      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?_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]
+    [IteratorAccess α Id] {it : Iter (α := α) β} {k n : Nat} :
+    (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 β]
+    [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 β]
+    [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')) →
+    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 (hno_skip _).elim hp
+  | done => simp
+
+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]
+  exact fun h => IterM.not_isPlausibleNthOutputStep_skip.elim h.1
+
+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 [val_nextAtIdxSlow?_zero_eq_val_step (fun _ => not_isPlausibleStep_skip_intermediateStepSize),
+    nextAtIdxSlow?_zero_intermediate_stepSize_val]
+
+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
+  generalize hsit : Intermediate.stepSize it i n = sit
+  replace hsit := hsit.symm
+  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]
+    {it : Iter (α := α) β} {n : Nat} :
+    (it.stepSize n).length = (it.length + (n - 1)) / (n - 1 + 1) := by
+  simp [stepSize_eq_intermediateStepSize, Intermediate.length_stepSize]
+
+end Std.Iter
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
index 7e2061c31dbd..fb0819f4967d 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
 
@@ -115,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⟩
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}
diff --git a/src/Std/Data/Iterators/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
index 0a3ad4c7f97a..1c70c9263f9c 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]
+      induction n generalizing it
+      · split
+        · refine .zero_yield ?_
+          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: 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: remove `inst...` argument as soon as possible
+          · 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