From 16919852d9deccb39055506cef2b978afd93ff8c Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 29 Jan 2026 08:22:19 +0100
Subject: [PATCH] refactor: remove last appearances of `allowNontermination`
 (#12211)

This PR updates docstrings and function signatures in order to complete
the transition from `Iter.Partial` to `Iter.Total` (extrinsically
terminating by default). It also deprecates `allowNontermination` and
adds `Iter.Total.atIdxSlow?`.
---
 src/Init/Data/Iterators/Basic.lean            | 34 +++++--
 src/Init/Data/Iterators/Consumers/Access.lean | 98 ++++++++++++++-----
 .../Iterators/Consumers/Monadic/Partial.lean  |  2 +-
 .../Data/Iterators/Consumers/Partial.lean     |  2 +-
 .../Iterators/Lemmas/Combinators/Take.lean    | 18 ++--
 .../Iterators/Lemmas/Consumers/Access.lean    |  3 +-
 .../Iterators/Lemmas/Consumers/Collect.lean   | 14 +--
 src/Lean/Elab/Parallel.lean                   | 10 +-
 .../Iterators/Lemmas/Combinators/Drop.lean    |  2 +-
 .../Lemmas/Combinators/TakeWhile.lean         | 20 ++--
 .../Iterators/Lemmas/Combinators/Zip.lean     | 24 ++---
 .../Iterators/Lemmas/Producers/Repeat.lean    |  6 +-
 tests/bench/hashmap.lean                      | 16 +--
 tests/bench/phashmap.lean                     | 14 +--
 tests/bench/treemap.lean                      | 16 +--
 tests/lean/run/task_iterators.lean            |  8 +-
 16 files changed, 180 insertions(+), 107 deletions(-)

diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean
index 943f04186f..da02f9fd67 100644
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -94,8 +94,9 @@ By convention, the monadic iterator associated with an object can be obtained vi
 For example, `List.iterM IO` creates an iterator over a list in the monad `IO`.
 
 See `Init.Data.Iterators.Consumers` for ways to use an iterator. For example, `it.toList` will
-convert a provably finite iterator `it` into a list and `it.allowNontermination.toList` will
-do so even if finiteness cannot be proved. It is also always possible to manually iterate using
+convert an iterator `it` into a list and `it.ensureTermination.toList` guarantees that this
+operation will terminate, given a proof that the iterator is finite.
+It is also always possible to manually iterate using
 `it.step`, relying on the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
 
 See `Iter` for a more convenient interface in case that no monadic effects are needed (`m = Id`).
@@ -139,8 +140,9 @@ By convention, the monadic iterator associated with an object can be obtained vi
 For example, `List.iterM IO` creates an iterator over a list in the monad `IO`.
 
 See `Init.Data.Iterators.Consumers` for ways to use an iterator. For example, `it.toList` will
-convert a provably finite iterator `it` into a list and `it.allowNontermination.toList` will
-do so even if finiteness cannot be proved. It is also always possible to manually iterate using
+convert an iterator `it` into a list and `it.ensureTermination.toList` guarantees that this
+operation will terminate, given a proof that the iterator is finite.
+It is also always possible to manually iterate using
 `it.step`, relying on the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
 
 See `IterM` for iterators that operate in a monad.
@@ -754,8 +756,8 @@ def IterM.finitelyManySteps {α : Type w} {m : Type w → Type w'} {β : Type w}
   ⟨it⟩
 
 /--
-Termination measure to be used in well-founded recursive functions recursing over a finite iterator
-(see also `Finite`).
+Termination measure to be used in recursive functions built with `WellFounded.extrinsicFix`
+recursing over a finite iterator without requiring a proof of finiteness (see also `Finite`).
 -/
 @[expose]
 def IterM.finitelyManySteps! {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
@@ -796,6 +798,11 @@ def Iter.finitelyManySteps {α : Type w} {β : Type w} [Iterator α Id β] [Iter
     (it : Iter (α := α) β) : IterM.TerminationMeasures.Finite α Id :=
   it.toIterM.finitelyManySteps
 
+@[inherit_doc IterM.finitelyManySteps!, expose]
+def Iter.finitelyManySteps! {α : Type w} {β : Type w} [Iterator α Id β]
+    (it : Iter (α := α) β) : IterM.TerminationMeasures.Finite α Id :=
+  it.toIterM.finitelyManySteps!
+
 /--
 This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
 with `IterM.finitelyManySteps`.
@@ -902,6 +909,16 @@ def IterM.finitelyManySkips {α : Type w} {m : Type w → Type w'} {β : Type w}
     [Iterators.Productive α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Productive α m :=
   ⟨it⟩
 
+/--
+Termination measure to be used in recursive functions built with `WellFounded.extrinsicFix`
+recursing over a productive iterator without requiring a proof of productiveness
+(see also `Productive`).
+-/
+@[expose]
+def IterM.finitelyManySkips! {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it : IterM (α := α) m β) : IterM.TerminationMeasures.Productive α m :=
+  ⟨it⟩
+
 /--
 This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
 with `IterM.finitelyManySkips`.
@@ -922,6 +939,11 @@ def Iter.finitelyManySkips {α : Type w} {β : Type w} [Iterator α Id β] [Iter
     (it : Iter (α := α) β) : IterM.TerminationMeasures.Productive α Id :=
   it.toIterM.finitelyManySkips
 
+@[inherit_doc IterM.finitelyManySkips!, expose]
+def Iter.finitelyManySkips! {α : Type w} {β : Type w} [Iterator α Id β]
+    (it : Iter (α := α) β) : IterM.TerminationMeasures.Productive α Id :=
+  it.toIterM.finitelyManySkips!
+
 /--
 This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
 with `Iter.finitelyManySkips`.
diff --git a/src/Init/Data/Iterators/Consumers/Access.lean b/src/Init/Data/Iterators/Consumers/Access.lean
index 8e3e0b9f70..27f64e257c 100644
--- a/src/Init/Data/Iterators/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Access.lean
@@ -21,21 +21,70 @@ If possible, takes `n` steps with the iterator `it` and
 returns the `n`-th emitted value, or `none` if `it` finished
 before emitting `n` values.
 
-This function requires a `Productive` instance proving that the iterator will always emit a value
-after a finite number of skips. If the iterator is not productive or such an instance is not
-available, consider using `it.allowNontermination.atIdxSlow?` instead of `it.atIdxSlow?`. However,
-it is not possible to formally verify the behavior of the partial variant.
+If the iterator is not productive, this function might run forever in an endless loop of iterator
+steps. The variant `it.ensureTermination.atIdxSlow?` is guaranteed to terminate after finitely many
+steps.
 -/
 @[specialize]
-def Iter.atIdxSlow? {α β} [Iterator α Id β] [Productive α Id]
+def Iter.atIdxSlow? {α β} [Iterator α Id β]
     (n : Nat) (it : Iter (α := α) β) : Option β :=
-  match it.step with
-  | .yield it' out _ =>
-    match n with
-    | 0 => some out
-    | k + 1 => it'.atIdxSlow? k
-  | .skip it' _ => it'.atIdxSlow? n
-  | .done _ => none
+  WellFounded.extrinsicFix₂ (C₂ := fun _ _ => Option β) (α := Iter (α := α) β) (β := fun _ => Nat)
+    (InvImage
+      (Prod.Lex WellFoundedRelation.rel IterM.TerminationMeasures.Productive.Rel)
+      (fun p => (p.2, p.1.finitelyManySkips!)))
+    (fun it n recur =>
+      match it.step with
+      | .yield it' out _ =>
+        match n with
+        | 0 => some out
+        | k + 1 => recur it' k (by decreasing_tactic)
+      | .skip it' _ => recur it' n (by decreasing_tactic)
+      | .done _ => none) it n
+
+-- We provide the functional induction principle by hand because `atIdxSlow?` is implemented using
+-- `extrinsicFix₂` and not using well-founded recursion.
+/-
+An induction principle for `Iter.atIdxSlow?`.
+
+This lemma provides a functional induction principle for reasoning about `Iter.atIdxSlow? n it`.
+
+The induction follows the structure of iterator steps.
+- base case: when we reach the desired index (`n = 0`) and get a `.yield` step
+- inductive case: when we have a `.yield` step but need to continue (`n > 0`)
+- skip case: when we encounter a `.skip` step and continue with the same index
+- done case: when the iterator is exhausted and we return `none`
+-/
+theorem Iter.atIdxSlow?.induct_unfolding {α β : Type u} [Iterator α Id β] [Productive α Id]
+    (motive : Nat → Iter β → Option β → Prop)
+    -- Base case: we have reached index 0 and found a value
+    (yield_zero : ∀ (it it' : Iter (α := α) β) (out : β) (property : it.IsPlausibleStep (IterStep.yield it' out)),
+        it.step = ⟨IterStep.yield it' out, property⟩ → motive 0 it (some out))
+    -- Inductive case: we have a yield but need to continue to a higher index
+    (yield_succ : ∀ (it it' : Iter (α := α) β) (out : β) (property : it.IsPlausibleStep (IterStep.yield it' out)),
+        it.step = ⟨IterStep.yield it' out, property⟩ →
+        ∀ (k : Nat), motive k it' (Iter.atIdxSlow? k it') → motive k.succ it (Iter.atIdxSlow? k it'))
+    -- Skip case: we encounter a skip and continue with the same index
+    (skip_case : ∀ (n : Nat) (it it' : Iter β) (property : it.IsPlausibleStep (IterStep.skip it')),
+        it.step = ⟨IterStep.skip it', property⟩ →
+        motive n it' (Iter.atIdxSlow? n it') → motive n it (Iter.atIdxSlow? n it'))
+    -- Done case: the iterator is exhausted, return none
+    (done_case : ∀ (n : Nat) (it : Iter β) (property : it.IsPlausibleStep IterStep.done),
+        it.step = ⟨IterStep.done, property⟩ → motive n it none)
+    -- The conclusion: the property holds for all indices and iterators
+    (n : Nat) (it : Iter β) : motive n it (Iter.atIdxSlow? n it) := by
+  simp only [atIdxSlow?] at *
+  rw [WellFounded.extrinsicFix₂_eq_apply]
+  · split
+    · split
+      · apply yield_zero <;> assumption
+      · apply yield_succ
+        all_goals try assumption
+        apply Iter.atIdxSlow?.induct_unfolding <;> assumption
+    · apply skip_case
+      all_goals try assumption
+      apply Iter.atIdxSlow?.induct_unfolding <;> assumption
+    · apply done_case <;> assumption
+  · exact InvImage.wf _ WellFoundedRelation.wf
 termination_by (n, it.finitelyManySkips)
 
 /--
@@ -43,22 +92,21 @@ If possible, takes `n` steps with the iterator `it` and
 returns the `n`-th emitted value, or `none` if `it` finished
 before emitting `n` values.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Productive` instance, consider using `Iter.atIdxSlow?` instead.
+This variant terminates after finitely many steps and requires a proof that the iterator is
+productive. If such a proof is not available, consider using `Iter.toArray`.
 -/
-@[specialize]
-partial def Iter.Partial.atIdxSlow? {α β} [Iterator α Id β] [Monad Id]
-    (n : Nat) (it : Iter.Partial (α := α) β) : Option β := do
-  match it.it.step with
-  | .yield it' out _ =>
-    match n with
-    | 0 => some out
-    | k + 1 => (⟨it'⟩ : Iter.Partial (α := α) β).atIdxSlow? k
-  | .skip it' _ => (⟨it'⟩ : Iter.Partial (α := α) β).atIdxSlow? n
-  | .done _ => none
+@[inline]
+def Iter.Total.atIdxSlow? {α β} [Iterator α Id β] [Productive α Id]
+    (n : Nat) (it : Iter.Total (α := α) β) : Option β :=
+  it.it.atIdxSlow? n
+
+@[inline, inherit_doc Iter.atIdxSlow?, deprecated Iter.atIdxSlow? (since := "2026-01-28")]
+def Iter.Partial.atIdxSlow? {α β} [Iterator α Id β]
+    (n : Nat) (it : Iter.Partial (α := α) β) : Option β :=
+  it.it.atIdxSlow? n
 
 @[always_inline, inline, inherit_doc IterM.atIdx?]
-def Iter.atIdx? {α β} [Iterator α Id β] [Productive α Id] [IteratorAccess α Id]
+def Iter.atIdx? {α β} [Iterator α Id β] [IteratorAccess α Id]
     (n : Nat) (it : Iter (α := α) β) : Option β :=
   match (IteratorAccess.nextAtIdx? it.toIterM n).run.val with
   | .yield _ out => some out
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean b/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean
index 41545adc42..ab284a8181 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Partial.lean
@@ -29,7 +29,7 @@ consumers such as `toList`. They can be used without any proof of termination su
 or `Productive`, but as they are implemented with the `partial` declaration modifier, they are
 opaque for the kernel and it is impossible to prove anything about them.
 -/
-@[always_inline, inline]
+@[always_inline, inline, deprecated "The consumers on iterators do not require proofs of termination anymore. For example, use `it.toList` instead of `it.allowNontermination.toList`." (since := "2026-01-28")]
 def IterM.allowNontermination {α : Type w} {m : Type w → Type w'} {β : Type w}
     (it : IterM (α := α) m β) : IterM.Partial (α := α) m β :=
   ⟨it⟩
diff --git a/src/Init/Data/Iterators/Consumers/Partial.lean b/src/Init/Data/Iterators/Consumers/Partial.lean
index 2eee2bf5ec..e306f4c2d6 100644
--- a/src/Init/Data/Iterators/Consumers/Partial.lean
+++ b/src/Init/Data/Iterators/Consumers/Partial.lean
@@ -29,7 +29,7 @@ consumers such as `toList`. They can be used without any proof of termination su
 or `Productive`, but as they are implemented with the `partial` declaration modifier, they are
 opaque for the kernel and it is impossible to prove anything about them.
 -/
-@[always_inline, inline]
+@[always_inline, inline, deprecated "The consumers on iterators do not require proofs of termination anymore. For example, use `it.toList` instead of `it.allowNontermination.toList`." (since := "2026-01-28")]
 def Iter.allowNontermination {α : Type w} {β : Type w}
     (it : Iter (α := α) β) : Iter.Partial (α := α) β :=
   ⟨it⟩
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean
index 1394fccdef..7ebed8cedc 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Take.lean
@@ -47,18 +47,18 @@ theorem Iter.atIdxSlow?_take {α β}
     [Iterator α Id β] [Productive α Id] {k l : Nat}
     {it : Iter (α := α) β} :
     (it.take k).atIdxSlow? l = if l < k then it.atIdxSlow? l else none := by
-  fun_induction it.atIdxSlow? l generalizing k
-  case case1 it it' out h h' =>
-    simp only [atIdxSlow?.eq_def (it := it.take k), step_take, h']
+  induction l, it using Iter.atIdxSlow?.induct_unfolding generalizing k
+  case yield_zero it it' out h h' =>
+    simp only [atIdxSlow?_eq_match (it := it.take k), step_take, h']
     cases k <;> simp
-  case case2 it it' out h h' l ih =>
-    simp only [Nat.succ_eq_add_one, atIdxSlow?.eq_def (it := it.take k), step_take, h']
+  case yield_succ it it' out h h' l ih =>
+    simp only [Nat.succ_eq_add_one, atIdxSlow?_eq_match (it := it.take k), step_take, h']
     cases k <;> cases l <;> simp [ih]
-  case case3 l it it' h h' ih =>
-    simp only [atIdxSlow?.eq_def (it := it.take k), step_take, h']
+  case skip_case l it it' h h' ih =>
+    simp only [atIdxSlow?_eq_match (it := it.take k), step_take, h']
     cases k <;> cases l <;> simp [ih]
-  case case4 l it h h' =>
-    simp only [atIdxSlow?.eq_def (it := it.take k), step_take, h']
+  case done_case l it h h' =>
+    simp only [atIdxSlow?_eq_match (it := it.take k), step_take, h']
     cases k <;> cases l <;> simp
 
 @[simp]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
index 8dc8779832..7f65ada4eb 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Access.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Iterators.Consumers.Access
+import Init.Data.Iterators.Lemmas.Basic
 
 namespace Std.Iter
 open Std.Iterators
@@ -21,6 +22,6 @@ public theorem atIdxSlow?_eq_match [Iterator α Id β] [Productive α Id]
         | n + 1 => it'.atIdxSlow? n
       | .skip it' => it'.atIdxSlow? n
       | .done => none) := by
-  fun_induction it.atIdxSlow? n <;> simp_all
+  induction n, it using Iter.atIdxSlow?.induct_unfolding <;> simp_all
 
 end Std.Iter
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
index ccc4c14126..4fc3944908 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
@@ -163,12 +163,14 @@ theorem Iter.getElem?_toList_eq_atIdxSlow? {α β}
     {it : Iter (α := α) β} {k : Nat} :
     it.toList[k]? = it.atIdxSlow? k := by
   induction it using Iter.inductSteps generalizing k with | step it ihy ihs
-  rw [toList_eq_match_step, atIdxSlow?]
-  obtain ⟨step, h⟩ := it.step
-  cases step
-  · cases k <;> simp [ihy h]
-  · simp [ihs h]
-  · simp
+  rw [toList_eq_match_step, atIdxSlow?, WellFounded.extrinsicFix₂_eq_apply]
+  · obtain ⟨step, h⟩ := it.step
+    cases step
+    · cases k <;> simp [ihy h, atIdxSlow?]
+    · simp [ihs h, atIdxSlow?]
+    · simp
+  · apply InvImage.wf
+    exact WellFoundedRelation.wf
 
 theorem Iter.toList_eq_of_atIdxSlow?_eq {α₁ α₂ β}
     [Iterator α₁ Id β] [Finite α₁ Id]
diff --git a/src/Lean/Elab/Parallel.lean b/src/Lean/Elab/Parallel.lean
index e35347d9aa..0cfc7c7182 100644
--- a/src/Lean/Elab/Parallel.lean
+++ b/src/Lean/Elab/Parallel.lean
@@ -58,7 +58,7 @@ This allows you to observe state changes (like logged messages, modified metavar
 as tasks complete, unlike `par`/`par'` which restore the initial state after collecting all results.
 
 Iterators do not have `Finite` instances, as we cannot prove termination from the available
-information. For consumers that require `Finite` (like `.toList`), use `.allowNontermination.toList`.
+information.
 -/
 
 public section
@@ -245,7 +245,7 @@ If `cancel := true` (the default), cancels all remaining tasks after the first s
 -/
 def parFirst {α : Type} (jobs : List (CoreM α)) (cancel : Bool := true) : CoreM α := do
   let (cancelHook, iter) ← parIterGreedyWithCancel jobs
-  for result in iter.allowNontermination do
+  for result in iter do
     match result with
     | .ok value =>
       if cancel then cancelHook
@@ -380,7 +380,7 @@ If `cancel := true` (the default), cancels all remaining tasks after the first s
 -/
 def parFirst {α : Type} (jobs : List (MetaM α)) (cancel : Bool := true) : MetaM α := do
   let (cancelHook, iter) ← parIterGreedyWithCancel jobs
-  for result in iter.allowNontermination do
+  for result in iter do
     match result with
     | .ok value =>
       if cancel then cancelHook
@@ -517,7 +517,7 @@ If `cancel := true` (the default), cancels all remaining tasks after the first s
 -/
 def parFirst {α : Type} (jobs : List (TermElabM α)) (cancel : Bool := true) : TermElabM α := do
   let (cancelHook, iter) ← parIterGreedyWithCancel jobs
-  for result in iter.allowNontermination do
+  for result in iter do
     match result with
     | .ok value =>
       if cancel then cancelHook
@@ -654,7 +654,7 @@ If `cancel := true` (the default), cancels all remaining tasks after the first s
 -/
 def parFirst {α : Type} (jobs : List (TacticM α)) (cancel : Bool := true) : TacticM α := do
   let (cancelHook, iter) ← parIterGreedyWithCancel jobs
-  for result in iter.allowNontermination do
+  for result in iter do
     match result with
     | .ok value =>
       if cancel then cancelHook
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
index a962aa0866..94fd78d9c8 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean
@@ -41,7 +41,7 @@ theorem Iter.atIdxSlow?_drop {α β}
   induction k generalizing it <;> induction l generalizing it
   all_goals
     induction it using Iter.inductSkips with | step it ih
-    rw [atIdxSlow?.eq_def, atIdxSlow?.eq_def, step_drop]
+    rw [atIdxSlow?_eq_match, atIdxSlow?_eq_match, step_drop]
     cases it.step using PlausibleIterStep.casesOn <;> simp [*]
 
 @[simp]
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean
index cbed3115f2..3573625adb 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean
@@ -57,11 +57,11 @@ theorem Iter.atIdxSlow?_takeWhile {α β}
     [Iterator α Id β] [Productive α Id] {l : Nat}
     {it : Iter (α := α) β} {P} :
     (it.takeWhile P).atIdxSlow? l = if ∀ k, k ≤ l → (it.atIdxSlow? k).any P then it.atIdxSlow? l else none := by
-  fun_induction it.atIdxSlow? l
-  case case1 it it' out h h' =>
+  induction l, it using atIdxSlow?.induct_unfolding
+  case yield_zero it it' out h h' =>
     rw [atIdxSlow?_eq_match]
     simp only [val_step_takeWhile, h', Nat.le_zero_eq, forall_eq]
-    rw [atIdxSlow?, h']
+    rw [atIdxSlow?_eq_match, h']
     simp only [Option.any_some]
     apply Eq.symm
     split
@@ -71,10 +71,10 @@ theorem Iter.atIdxSlow?_takeWhile {α β}
     · cases h' : P out
       · simp
       · exfalso; simp_all
-  case case2 it it' out h h' l ih =>
+  case yield_succ it it' out h h' l ih =>
     rw [atIdxSlow?_eq_match]
     simp only [Nat.succ_eq_add_one, val_step_takeWhile, h']
-    simp only [atIdxSlow?.eq_def (it := it), h']
+    simp only [atIdxSlow?_eq_match (it := it), h']
     cases hP : P out
     · simp
       intro h
@@ -96,11 +96,11 @@ theorem Iter.atIdxSlow?_takeWhile {α β}
         apply hl
         intro k hk
         exact hl' (k + 1) (Nat.succ_le_succ hk)
-  case case3 l it it' h h' ih =>
-    simp only [atIdxSlow?.eq_def (it := it.takeWhile P), step_takeWhile, h', ih]
-    simp only [atIdxSlow?.eq_def (it := it), h']
-  case case4 l it h h' =>
-    simp only [atIdxSlow?.eq_def (it := it), atIdxSlow?.eq_def (it := it.takeWhile P), h',
+  case skip_case l it it' h h' ih =>
+    simp only [atIdxSlow?_eq_match (it := it.takeWhile P), step_takeWhile, h', ih]
+    simp only [atIdxSlow?_eq_match (it := it), h']
+  case done_case l it h h' =>
+    simp only [atIdxSlow?_eq_match (it := it), atIdxSlow?_eq_match (it := it.takeWhile P), h',
       step_takeWhile]
     split <;> rfl
 
diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean
index f3d50fc2de..76258b2339 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean
@@ -184,9 +184,9 @@ theorem Iter.atIdxSlow?_intermediateZip [Iterator α₁ Id β₁] [Iterator α
         | n' + 1 => do return (← it₁.atIdxSlow? n', ← it₂.atIdxSlow? (n' + 1))) := by
   generalize h : Intermediate.zip it₁ memo it₂ = it
   revert h it₁ memo it₂
-  fun_induction it.atIdxSlow? n
+  induction n, it using atIdxSlow?.induct_unfolding
   rintro it₁ memo it₂ rfl
-  case case1 it it' out h h' =>
+  case yield_zero it it' out h h' =>
     rw [atIdxSlow?]
     simp only [Option.pure_def, Option.bind_eq_bind]
     simp only [step_intermediateZip, PlausibleIterStep.skip, PlausibleIterStep.done,
@@ -195,9 +195,9 @@ theorem Iter.atIdxSlow?_intermediateZip [Iterator α₁ Id β₁] [Iterator α
     · split at h' <;> cases h'
     · split at h' <;> cases h'
       rename_i hs₂
-      rw [atIdxSlow?, hs₂]
+      rw [atIdxSlow?_eq_match, hs₂]
       simp
-  case case2 it it' out h  h' n ih =>
+  case yield_succ it it' out h  h' n ih =>
     rintro it₁ memo it₂ rfl
     simp only [Nat.succ_eq_add_one, Option.pure_def, Option.bind_eq_bind]
     cases memo
@@ -211,8 +211,8 @@ theorem Iter.atIdxSlow?_intermediateZip [Iterator α₁ Id β₁] [Iterator α
       split at h' <;> cases h'
       rename_i hs₂
       simp only [ih rfl, Option.pure_def, Option.bind_eq_bind]
-      rw [atIdxSlow?.eq_def (it := it₂), hs₂]
-  case case3 it it' h h' ih =>
+      rw [atIdxSlow?_eq_match (it := it₂), hs₂]
+  case skip_case it it' h h' ih =>
     rintro it₁ memo it₂ rfl
     obtain ⟨it₁', memo', it₂', rfl⟩ := Intermediate.zip_surj it'
     specialize ih rfl
@@ -223,19 +223,19 @@ theorem Iter.atIdxSlow?_intermediateZip [Iterator α₁ Id β₁] [Iterator α
     · split at h' <;> rename_i hs₁
       · simp only [IterStep.skip.injEq, Intermediate.zip_inj] at h'
         obtain ⟨rfl, rfl, rfl⟩ := h'
-        simp only [ih, Option.pure_def, Option.bind_eq_bind, atIdxSlow?.eq_def (it := it₁), hs₁]
+        simp only [ih, Option.pure_def, Option.bind_eq_bind, atIdxSlow?_eq_match (it := it₁), hs₁]
         split <;> rfl
       · simp only [IterStep.skip.injEq, Intermediate.zip_inj] at h'
         obtain ⟨rfl, rfl, rfl⟩ := h'
-        simp [ih, atIdxSlow?.eq_def (it := it₁), hs₁]
+        simp [ih, atIdxSlow?_eq_match (it := it₁), hs₁]
       · cases h'
     · split at h' <;> rename_i hs₂ <;> (try cases h')
       simp only [IterStep.skip.injEq, Intermediate.zip_inj] at h'
       obtain ⟨rfl, rfl, rfl⟩ := h'
-      simp [ih, atIdxSlow?.eq_def (it := it₂), hs₂]
-  case case4 it _ h =>
+      simp [ih, atIdxSlow?_eq_match (it := it₂), hs₂]
+  case done_case it _ h =>
     rintro it₁ memo it₂ rfl
-    rw [atIdxSlow?]
+    rw [atIdxSlow?_eq_match]
     simp only [step_intermediateZip] at h
     cases memo
     case none =>
@@ -247,7 +247,7 @@ theorem Iter.atIdxSlow?_intermediateZip [Iterator α₁ Id β₁] [Iterator α
       simp only at h
       split at h <;> cases h
       rename_i hs₂
-      simp only [atIdxSlow?.eq_def (it := it₂), hs₂, Option.pure_def, Option.bind_eq_bind,
+      simp only [atIdxSlow?_eq_match (it := it₂), hs₂, Option.pure_def, Option.bind_eq_bind,
         Option.bind_none, Option.bind_fun_none]
       split <;> rfl
 
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean b/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean
index 2d26a3a553..d0216952d5 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean
@@ -22,15 +22,15 @@ theorem Iter.step_repeat :
 
 theorem Iter.atIdxSlow?_zero_repeat :
     (Iter.repeat f init).atIdxSlow? 0 = some init := by
-  rw [atIdxSlow?, step_repeat]
+  rw [atIdxSlow?_eq_match, step_repeat]
 
 theorem Iter.atIdxSlow?_succ_repeat {k : Nat} :
     (Iter.repeat f init).atIdxSlow? (k + 1) = (Iter.repeat f (f init)).atIdxSlow? k := by
-  rw [atIdxSlow?, step_repeat]
+  rw [atIdxSlow?_eq_match, step_repeat]
 
 theorem Iter.atIdxSlow?_succ_repeat_eq_map {k : Nat} :
     (Iter.repeat f init).atIdxSlow? (k + 1) = f <$> ((Iter.repeat f init).atIdxSlow? k) := by
-  rw [atIdxSlow?, step_repeat]
+  rw [atIdxSlow?_eq_match, step_repeat]
   simp only
   induction k generalizing init
   · simp [atIdxSlow?_zero_repeat, Functor.map]
diff --git a/tests/bench/hashmap.lean b/tests/bench/hashmap.lean
index a68bd7d038..a8c1830e3f 100644
--- a/tests/bench/hashmap.lean
+++ b/tests/bench/hashmap.lean
@@ -35,7 +35,7 @@ instance [Pure m] : Std.Iterator RandomIterator m UInt64 where
 
 def mkMapWithCap (seed : UInt64) (size : Nat) : Std.HashMap UInt64 UInt64 := Id.run do
   let mut map := Std.HashMap.emptyWithCapacity size
-  for val in iterRand seed |>.take size |>.allowNontermination do
+  for val in iterRand seed |>.take size do
     map := map.insert val val
   return map
 
@@ -56,7 +56,7 @@ def benchContainsHit (seed : UInt64) (size : Nat) : IO Float := do
   timeNanos checks do
     let mut todo := checks
     while todo != 0 do
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         if !map.contains val then
           throw <| .userError "Fail"
       todo := todo - size
@@ -71,7 +71,7 @@ def benchContainsMiss (seed : UInt64) (size : Nat) : IO Float := do
   timeNanos checks do
     let mut todo := checks
     while todo != 0 do
-      for val in iter |>.take size |>.allowNontermination do
+      for val in iter |>.take size do
         if map.contains val then
           throw <| .userError "Fail"
       todo := todo - size
@@ -103,7 +103,7 @@ def benchInsertIfNewHit (seed : UInt64) (size : Nat) : IO Float := do
     let mut todo := checks
     let mut map := map
     while todo != 0 do
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insertIfNew val val
         if map.size != size then
           throw <| .userError "Fail"
@@ -120,7 +120,7 @@ def benchInsertHit (seed : UInt64) (size : Nat) : IO Float := do
     let mut todo := checks
     let mut map := map
     while todo != 0 do
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insert val val
         if map.size != size then
           throw <| .userError "Fail"
@@ -135,7 +135,7 @@ def benchInsertMissEmpty (seed : UInt64) (size : Nat) : IO Float := do
     let mut todo := checks
     while todo != 0 do
       let mut map : Std.HashMap _ _ := {}
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insert val val
         if map.size > size then
           throw <| .userError "Fail"
@@ -150,7 +150,7 @@ def benchInsertMissEmptyWithCapacity (seed : UInt64) (size : Nat) : IO Float :=
     let mut todo := checks
     while todo != 0 do
       let mut map := Std.HashMap.emptyWithCapacity size
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insert val val
         if map.size > size then
           throw <| .userError "Fail"
@@ -168,7 +168,7 @@ def benchEraseInsert (seed : UInt64) (size : Nat) : IO Float := do
     let mut map := map
     let mut todo := checks
     while todo != 0 do
-      for (eraseVal, newVal) in eraseIter.zip newIter |>.take size |>.allowNontermination do
+      for (eraseVal, newVal) in eraseIter.zip newIter |>.take size do
         map := map.erase eraseVal |>.insert newVal newVal
         if map.size != size then
           throw <| .userError "Fail"
diff --git a/tests/bench/phashmap.lean b/tests/bench/phashmap.lean
index bbc7ec134c..ba4426c35b 100644
--- a/tests/bench/phashmap.lean
+++ b/tests/bench/phashmap.lean
@@ -33,7 +33,7 @@ instance [Pure m] : Std.Iterator RandomIterator m UInt64 where
 
 def mkMapWithCap (seed : UInt64) (size : Nat) : Lean.PersistentHashMap UInt64 UInt64 := Id.run do
   let mut map := Lean.PersistentHashMap.empty
-  for val in iterRand seed |>.take size |>.allowNontermination do
+  for val in iterRand seed |>.take size do
     map := map.insert val val
   return map
 
@@ -54,7 +54,7 @@ def benchContainsHit (seed : UInt64) (size : Nat) : IO Float := do
   timeNanos checks do
     let mut todo := checks
     while todo != 0 do
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         if !map.contains val then
           throw <| .userError "Fail"
       todo := todo - size
@@ -69,7 +69,7 @@ def benchContainsMiss (seed : UInt64) (size : Nat) : IO Float := do
   timeNanos checks do
     let mut todo := checks
     while todo != 0 do
-      for val in iter |>.take size |>.allowNontermination do
+      for val in iter |>.take size do
         if map.contains val then
           throw <| .userError "Fail"
       todo := todo - size
@@ -101,7 +101,7 @@ def benchInsertHit (seed : UInt64) (size : Nat) : IO Float := do
     let mut todo := checks
     let mut map := map
     while todo != 0 do
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insert val val
         if map.isEmpty then
           throw <| .userError "Fail"
@@ -116,7 +116,7 @@ def benchInsertMissEmpty (seed : UInt64) (size : Nat) : IO Float := do
     let mut todo := checks
     while todo != 0 do
       let mut map : Lean.PersistentHashMap _ _ := {}
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insert val val
         if map.isEmpty then
           throw <| .userError "Fail"
@@ -133,7 +133,7 @@ def benchInsertMissEmptyShared (seed : UInt64) (size : Nat) : IO Float := do
     while todo != 0 do
       let mut map : Lean.PersistentHashMap _ _ := {}
       let mut maps := Array.emptyWithCapacity size
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insert val val
         if map.isEmpty then
           throw <| .userError "Fail"
@@ -154,7 +154,7 @@ def benchEraseInsert (seed : UInt64) (size : Nat) : IO Float := do
     let mut map := map
     let mut todo := checks
     while todo != 0 do
-      for (eraseVal, newVal) in eraseIter.zip newIter |>.take size |>.allowNontermination do
+      for (eraseVal, newVal) in eraseIter.zip newIter |>.take size do
         map := map.erase eraseVal |>.insert newVal newVal
         if map.isEmpty then
           throw <| .userError "Fail"
diff --git a/tests/bench/treemap.lean b/tests/bench/treemap.lean
index 000454f570..dc25e1c9a9 100644
--- a/tests/bench/treemap.lean
+++ b/tests/bench/treemap.lean
@@ -30,7 +30,7 @@ instance [Pure m] : Std.Iterator RandomIterator m UInt64 where
 
 def mkMap (seed : UInt64) (size : Nat) : Std.TreeMap UInt64 UInt64 := Id.run do
   let mut map := {}
-  for val in iterRand seed |>.take size |>.allowNontermination do
+  for val in iterRand seed |>.take size do
     map := map.insert val val
   return map
 
@@ -51,7 +51,7 @@ def benchContainsHit (seed : UInt64) (size : Nat) : IO Float := do
   timeNanos checks do
     let mut todo := checks
     while todo != 0 do
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         if !map.contains val then
           throw <| .userError "Fail"
       todo := todo - size
@@ -66,7 +66,7 @@ def benchContainsMiss (seed : UInt64) (size : Nat) : IO Float := do
   timeNanos checks do
     let mut todo := checks
     while todo != 0 do
-      for val in iter |>.take size |>.allowNontermination do
+      for val in iter |>.take size do
         if map.contains val then
           throw <| .userError "Fail"
       todo := todo - size
@@ -98,7 +98,7 @@ def benchInsertIfNewHit (seed : UInt64) (size : Nat) : IO Float := do
     let mut todo := checks
     let mut map := map
     while todo != 0 do
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insertIfNew val val
         if map.size != size then
           throw <| .userError "Fail"
@@ -115,7 +115,7 @@ def benchInsertHit (seed : UInt64) (size : Nat) : IO Float := do
     let mut todo := checks
     let mut map := map
     while todo != 0 do
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insert val val
         if map.size != size then
           throw <| .userError "Fail"
@@ -130,7 +130,7 @@ def benchInsertRandomMissEmpty (seed : UInt64) (size : Nat) : IO Float := do
     let mut todo := checks
     while todo != 0 do
       let mut map : Std.TreeMap UInt64 _ := {}
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insert val val
         if map.size > size then
           throw <| .userError "Fail"
@@ -162,7 +162,7 @@ def benchInsertRandomMissEmptyShared (seed : UInt64) (size : Nat) : IO Float :=
     while todo != 0 do
       let mut map : Std.TreeMap UInt64 _ := {}
       let mut maps := Array.emptyWithCapacity size
-      for val in iterRand seed |>.take size |>.allowNontermination do
+      for val in iterRand seed |>.take size do
         map := map.insert val val
         if map.isEmpty then
           throw <| .userError "Fail"
@@ -183,7 +183,7 @@ def benchEraseInsert (seed : UInt64) (size : Nat) : IO Float := do
     let mut map := map
     let mut todo := checks
     while todo != 0 do
-      for (eraseVal, newVal) in eraseIter.zip newIter |>.take size |>.allowNontermination do
+      for (eraseVal, newVal) in eraseIter.zip newIter |>.take size do
         map := map.erase eraseVal |>.insert newVal newVal
         if map.size != size then
           throw <| .userError "Fail"
diff --git a/tests/lean/run/task_iterators.lean b/tests/lean/run/task_iterators.lean
index 896b33422c..02ffcb20d1 100644
--- a/tests/lean/run/task_iterators.lean
+++ b/tests/lean/run/task_iterators.lean
@@ -64,7 +64,7 @@ def testStateThreading : IO Unit := do
         let msgText ← msgs.headD default |>.data.toString
         return (value, count, msgText)
       | .error _ =>
-        return (0, 0, "error")).take 3 |>.allowNontermination.toList
+        return (0, 0, "error")).take 3 |>.toList
 
     return (results.map (·.1), results.map (·.2.1), results.map (·.2.2))
 
@@ -215,7 +215,7 @@ def testTacticMStateThreading : IO Unit := do
     let results ← (iter.mapM fun result =>
       match result with
       | .ok tacticName => return (tacticName, (← Lean.Elab.Tactic.getGoals).length)
-      | .error _ => return ("error", 999)).take 3 |>.allowNontermination.toList
+      | .error _ => return ("error", 999)).take 3 |>.toList
     return results.unzip
 
   let (tacticNames, goalCounts) ← runTacticTest tacticTest
@@ -249,7 +249,7 @@ def testTacticMParallel : IO Unit := do
     let (_, iter) ← Lean.Elab.Tactic.TacticM.parIterWithCancel tasks
 
     -- Consume the iterator and collect successful results
-    let results ← iter.take 3 |>.allowNontermination.toList
+    let results ← iter.take 3 |>.toList
     return results.filterMap fun r => match r with | .ok n => some n | .error _ => none
 
   let successResults ← runTacticTest tacticTest
@@ -289,7 +289,7 @@ def testParIterOrdering : IO Unit := do
 
     -- Consume all results from the iterator
     let mut results := []
-    for result in iter.allowNontermination do
+    for result in iter do
       match result with
       | .ok value => results := results.concat value
       | .error _ => pure ()