diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean
index 754d098d22..9fb865070b 100644
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -393,6 +393,16 @@ abbrev IterM.Step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator
     (it : IterM (α := α) m β) :=
   PlausibleIterStep it.IsPlausibleStep
 
+/--
+Makes a single step with the given iterator `it`, potentially emitting a value and providing a
+succeeding iterator. If this function is used recursively, termination can sometimes be proved with
+the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
+-/
+@[always_inline, inline, expose]
+def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it : IterM (α := α) m β) : m (Shrink it.Step) :=
+  Iterator.step it
+
 /--
 Asserts that a certain output value could plausibly be emitted by the given iterator in its next
 step.
@@ -420,16 +430,6 @@ def IterM.IsPlausibleSkipSuccessorOf {α : Type w} {m : Type w → Type w'} {β
     [Iterator α m β] (it' it : IterM (α := α) m β) : Prop :=
   it.IsPlausibleStep (.skip it')
 
-/--
-Makes a single step with the given iterator `it`, potentially emitting a value and providing a
-succeeding iterator. If this function is used recursively, termination can sometimes be proved with
-the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
--/
-@[always_inline, inline, expose]
-def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    (it : IterM (α := α) m β) : m (Shrink it.Step) :=
-  Iterator.step it
-
 end Monadic
 
 section Pure
@@ -717,6 +717,15 @@ def IterM.finitelyManySteps {α : Type w} {m : Type w → Type w'} {β : Type w}
     [Finite α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
   ⟨it⟩
 
+/--
+Termination measure to be used in well-founded recursive functions recursing over a finite iterator
+(see also `Finite`).
+-/
+@[expose]
+def IterM.finitelyManySteps! {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
+  ⟨it⟩
+
 /--
 This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
 with `IterM.finitelyManySteps`.
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
index c11d347974..a39d6240ec 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
@@ -91,21 +91,11 @@ instance Attach.instIteratorCollect {α β : Type w} {m : Type w → Type w'} [M
     IteratorCollect (Attach α m P) m n :=
   .defaultImplementation
 
-instance Attach.instIteratorCollectPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Monad n] {P : β → Prop} [Iterator α m β] :
-    IteratorCollectPartial (Attach α m P) m n :=
-  .defaultImplementation
-
 instance Attach.instIteratorLoop {α β : Type w} {m : Type w → Type w'} [Monad m]
     {n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] :
     IteratorLoop (Attach α m P) m n :=
   .defaultImplementation
 
-instance Attach.instIteratorLoopPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
-    {n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] :
-    IteratorLoopPartial (Attach α m P) m n :=
-  .defaultImplementation
-
 end Types
 
 /--
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
index 1c1bc4d347..cfd89dd82c 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
@@ -221,25 +221,11 @@ instance {α β γ : Type w} {m : Type w → Type w'}
     IteratorCollect (FilterMap α m n lift f) n o :=
   .defaultImplementation
 
-instance {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
-    {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n (Option γ)} [Finite α m] :
-    IteratorCollectPartial (FilterMap α m n lift f) n o :=
-  .defaultImplementation
-
 instance FilterMap.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type x → Type x'}
-    [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n (Option γ)} [Finite α m] :
-    IteratorLoop (FilterMap α m n lift f) n o :=
-  .defaultImplementation
-
-instance FilterMap.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type x → Type x'}
     [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} :
-    IteratorLoopPartial (FilterMap α m n lift f) n o :=
+    IteratorLoop (FilterMap α m n lift f) n o :=
   .defaultImplementation
 
 /--
@@ -249,7 +235,7 @@ instance FilterMap.instIteratorLoopPartial {α β γ : Type w} {m : Type w → T
 instance Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
     {lift₁ : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n γ} [IteratorCollect α m o] [Finite α m] :
+    {f : β → PostconditionT n γ} [IteratorCollect α m o] :
     IteratorCollect (Map α m n lift₁ f) n o where
   toArrayMapped lift₂ _ g it :=
     letI : MonadLift m n := ⟨lift₁ (α := _)⟩
@@ -259,18 +245,6 @@ instance Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
       (fun x => do g (← (f x).operation))
       it.internalState.inner (m := m)
 
-@[no_expose]
-instance Map.instIteratorCollectPartial {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
-    {lift₁ : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n γ} [IteratorCollectPartial α m o] :
-    IteratorCollectPartial (Map α m n lift₁ f) n o where
-  toArrayMappedPartial lift₂ _ g it :=
-    IteratorCollectPartial.toArrayMappedPartial
-      (lift := fun ⦃_⦄ a => lift₂ (lift₁ a))
-      (fun x => do g (← lift₂ (f x).operation))
-      it.internalState.inner (m := m)
-
 instance Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β]
     {lift : ⦃α : Type w⦄ → m α → n α}
@@ -278,13 +252,6 @@ instance Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
     IteratorLoop (Map α m n lift f) n o :=
   .defaultImplementation
 
-instance Map.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β]
-    {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n γ} :
-    IteratorLoopPartial (Map α m n lift f) n o :=
-  .defaultImplementation
-
 /--
 *Note: This is a very general combinator that requires an advanced understanding of monads, dependent
 types and termination proofs. The variants `map` and `mapM` are easier to use and sufficient
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean
index 5f268462ae..4b81a21064 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean
@@ -33,7 +33,7 @@ public structure Flatten (α α₂ β : Type w) (m) where
 /--
 Internal iterator combinator that is used to implement all `flatMap` variants
 -/
-@[always_inline]
+@[always_inline, inline]
 def IterM.flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     (it₁ : IterM (α := α) m (IterM (α := α₂) m β)) (it₂ : Option (IterM (α := α₂) m β)) :=
@@ -75,7 +75,7 @@ iterator.
 
 For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
 -/
-@[always_inline]
+@[always_inline, inline]
 public def IterM.flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
     (f : β → m (IterM (α := α₂) m γ)) (it₁ : IterM (α := α) m β) (it₂ : Option (IterM (α := α₂) m γ)) :=
@@ -114,7 +114,7 @@ This combinator incurs an additional O(1) cost with each output of `it` or an in
 
 For each value emitted by the outer iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, expose]
+@[always_inline, inline, expose]
 public def IterM.flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
     (f : β → m (IterM (α := α₂) m γ)) (it : IterM (α := α) m β) :=
@@ -156,7 +156,7 @@ iterator.
 
 For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
 -/
-@[always_inline]
+@[always_inline, inline]
 public def IterM.flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
     (f : β → IterM (α := α₂) m γ) (it₁ : IterM (α := α) m β) (it₂ : Option (IterM (α := α₂) m γ)) :=
@@ -195,7 +195,7 @@ This combinator incurs an additional O(1) cost with each output of `it` or an in
 
 For each value emitted by the outer iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, expose]
+@[always_inline, inline, expose]
 public def IterM.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
     (f : β → IterM (α := α₂) m γ) (it : IterM (α := α) m β) :=
@@ -370,16 +370,8 @@ public instance Flatten.instIteratorCollect [Monad m] [Monad n] [Iterator α m (
     [Iterator α₂ m β] : IteratorCollect (Flatten α α₂ β m) m n :=
   .defaultImplementation
 
-public instance Flatten.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
-    [Iterator α₂ m β] : IteratorCollectPartial (Flatten α α₂ β m) m n :=
-  .defaultImplementation
-
 public instance Flatten.instIteratorLoop [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
     [Iterator α₂ m β] : IteratorLoop (Flatten α α₂ β m) m n :=
   .defaultImplementation
 
-public instance Flatten.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
-    [Iterator α₂ m β] : IteratorLoopPartial (Flatten α α₂ β m) m n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/Take.lean b/src/Init/Data/Iterators/Combinators/Monadic/Take.lean
index 2eae2ad00a..54af3a9baa 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/Take.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/Take.lean
@@ -208,16 +208,8 @@ instance Take.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [
     IteratorCollect (Take α m) m n :=
   .defaultImplementation
 
-instance Take.instIteratorCollectPartial {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorCollectPartial (Take α m) m n :=
-  .defaultImplementation
-
 instance Take.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoop (Take α m) m n :=
   .defaultImplementation
 
-instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β] :
-    IteratorLoopPartial (Take α m) m n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
index 73d49ebdab..4f7e761f04 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
@@ -128,18 +128,10 @@ instance Types.ULiftIterator.instIteratorLoop {o : Type x → Type x'} [Monad n]
     IteratorLoop (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
-instance Types.ULiftIterator.instIteratorLoopPartial {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β] :
-    IteratorLoopPartial (ULiftIterator α m n β lift) n o :=
-  .defaultImplementation
-
 instance Types.ULiftIterator.instIteratorCollect [Monad n] [Monad o] [Iterator α m β] :
     IteratorCollect (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
-instance Types.ULiftIterator.instIteratorCollectPartial {o} [Monad n] [Monad o] [Iterator α m β] :
-    IteratorCollectPartial (ULiftIterator α m n β lift) n o :=
-  .defaultImplementation
-
 /--
 Transforms an `m`-monadic iterator with values in `β` into an `n`-monadic iterator with
 values in `ULift β`. Requires a `MonadLift m (ULiftT n)` instance.
diff --git a/src/Init/Data/Iterators/Consumers.lean b/src/Init/Data/Iterators/Consumers.lean
index 4b9e068574..1fef48b448 100644
--- a/src/Init/Data/Iterators/Consumers.lean
+++ b/src/Init/Data/Iterators/Consumers.lean
@@ -11,5 +11,6 @@ public import Init.Data.Iterators.Consumers.Access
 public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Partial
+public import Init.Data.Iterators.Consumers.Total
 
 public import Init.Data.Iterators.Consumers.Stream
diff --git a/src/Init/Data/Iterators/Consumers/Collect.lean b/src/Init/Data/Iterators/Consumers/Collect.lean
index 5c9f4b0fa7..e8a6d8d614 100644
--- a/src/Init/Data/Iterators/Consumers/Collect.lean
+++ b/src/Init/Data/Iterators/Consumers/Collect.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Iterators.Consumers.Partial
+public import Init.Data.Iterators.Consumers.Total
 public import Init.Data.Iterators.Consumers.Monadic.Collect
 
 @[expose] public section
@@ -21,40 +22,113 @@ Concretely, the following operations are provided:
 * `Iter.toListRev`, collecting the values in a list in reverse order but more efficiently
 * `Iter.toArray`, collecting the values in an array
 
-Some operations are implemented using the `IteratorCollect` and `IteratorCollectPartial`
-typeclasses.
+Some operations are implemented using the `IteratorCollect` type class.
 -/
 
 namespace Std.Iterators
 
-@[always_inline, inline, inherit_doc IterM.toArray]
+/--
+Traverses the given iterator and stores the emitted values in an array.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toArray` always terminates after finitely many steps.
+-/
+@[always_inline, inline]
 def Iter.toArray {α : Type w} {β : Type w}
-    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter (α := α) β) : Array β :=
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter (α := α) β) : Array β :=
   it.toIterM.toArray.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toArray]
-def Iter.Partial.toArray {α : Type w} {β : Type w}
-    [Iterator α Id β] [IteratorCollectPartial α Id Id] (it : Iter.Partial (α := α) β) : Array β :=
-  it.it.toIterM.allowNontermination.toArray.run
+/--
+Traverses the given iterator and stores the emitted values in an array.
 
-@[always_inline, inline, inherit_doc IterM.toListRev]
+This function is deprecated. Instead of `it.allowNontermination.toArray`, use `it.toArray`.
+-/
+@[always_inline, inline, deprecated Iter.toArray (since := "2025-12-04")]
+def Iter.Partial.toArray {α : Type w} {β : Type w}
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : Array β :=
+  it.it.toArray
+
+/--
+Traverses the given iterator and stores the emitted values in an array.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.toArray`.
+-/
+@[always_inline, inline]
+def Iter.Total.toArray {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter.Total (α := α) β) :
+    Array β :=
+  it.it.toArray
+
+/--
+Traverses the given iterator and stores the emitted values in reverse order in a list. Because
+lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toListRev` always terminates after finitely many steps.
+-/
+@[always_inline, inline]
 def Iter.toListRev {α : Type w} {β : Type w}
-    [Iterator α Id β] [Finite α Id] (it : Iter (α := α) β) : List β :=
+    [Iterator α Id β] (it : Iter (α := α) β) : List β :=
   it.toIterM.toListRev.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toListRev]
+/--
+Traverses the given iterator and stores the emitted values in reverse order in a list. Because
+lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
+
+This function is deprecated. Instead of `it.allowNontermination.toListRev`, use `it.toListRev`.
+-/
+@[always_inline, inline, deprecated Iter.toListRev (since := "2025-12-04")]
 def Iter.Partial.toListRev {α : Type w} {β : Type w}
     [Iterator α Id β] (it : Iter.Partial (α := α) β) : List β :=
-  it.it.toIterM.allowNontermination.toListRev.run
+  it.it.toListRev
 
-@[always_inline, inline, inherit_doc IterM.toList]
+/--
+Traverses the given iterator and stores the emitted values in reverse order in a list. Because
+lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.toListRev`.
+-/
+@[always_inline, inline]
+def Iter.Total.toListRev {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] (it : Iter.Total (α := α) β) : List β :=
+  it.it.toListRev
+
+/--
+Traverses the given iterator and stores the emitted values in a list. Because
+lists are prepend-only, `toListRev` is usually more efficient that `toList`.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toList` always terminates after finitely many steps.
+-/
+@[always_inline, inline]
 def Iter.toList {α : Type w} {β : Type w}
-    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter (α := α) β) : List β :=
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter (α := α) β) : List β :=
   it.toIterM.toList.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toList]
+/--
+Traverses the given iterator and stores the emitted values in a list. Because
+lists are prepend-only, `toListRev` is usually more efficient that `toList`.
+
+This function is deprecated. Instead of `it.allowNontermination.toList`, use `it.toList`.
+-/
+@[always_inline, deprecated Iter.toList (since := "2025-12-04")]
 def Iter.Partial.toList {α : Type w} {β : Type w}
-    [Iterator α Id β] [IteratorCollectPartial α Id Id] (it : Iter.Partial (α := α) β) : List β :=
-  it.it.toIterM.allowNontermination.toList.run
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : List β :=
+  it.it.toList
+
+/--
+Traverses the given iterator and stores the emitted values in a list. Because
+lists are prepend-only, `toListRev` is usually more efficient that `toList`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.toList`.
+-/
+@[always_inline, inline]
+def Iter.Total.toList {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter.Total (α := α) β) :
+    List β :=
+  it.it.toList
 
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean
index ed62dad7b7..3531e40507 100644
--- a/src/Init/Data/Iterators/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Loop.lean
@@ -23,7 +23,7 @@ function in every iteration. Concretely, the following operations are provided:
 * `Iter.fold`, the analogue of `List.foldl`
 * `Iter.foldM`, the analogue of `List.foldlM`
 
-These operations are implemented using the `IteratorLoop` and `IteratorLoopPartial` typeclasses.
+These operations are implemented using the `IteratorLoop` type class.
 -/
 
 namespace Std.Iterators
@@ -35,7 +35,7 @@ or future library improvements will make it more comfortable.
 -/
 @[always_inline, inline]
 def Iter.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
-    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
+    [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn' n (Iter (α := α) β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
   forIn' it init f :=
     IteratorLoop.finiteForIn' (fun _ _ f c => f c.run) |>.forIn' it.toIterM init
@@ -43,7 +43,7 @@ def Iter.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad
           f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc
 
 instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
-    [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
+    [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn n (Iter (α := α) β) β :=
   haveI : ForIn' n (Iter (α := α) β) β _ := Iter.instForIn'
   instForInOfForIn'
@@ -53,44 +53,58 @@ An implementation of `for h : ... in ... do ...` notation for partial iterators.
 -/
 @[always_inline, inline]
 def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
-    [Iterator α Id β] [IteratorLoopPartial α Id n] :
+    [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn' n (Iter.Partial (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
   forIn' it init f :=
-    IteratorLoopPartial.forInPartial (α := α) (m := Id) (n := n) (fun _ _ f c => f c.run)
-      it.it.toIterM init
-      fun out h acc =>
-        f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc
+    haveI := @Iter.instForIn'
+    forIn' it.it init f
 
 instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
-    [Iterator α Id β] [IteratorLoopPartial α Id n] :
+    [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn n (Iter.Partial (α := α) β) β :=
   haveI : ForIn' n (Iter.Partial (α := α) β) β _ := Iter.Partial.instForIn'
   instForInOfForIn'
 
+/--
+A `ForIn'` instance for iterators that is guaranteed to terminate after finitely many steps.
+It is not marked as an instance because the membership predicate is difficult to work with.
+-/
+@[always_inline, inline]
+def Iter.Total.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
+    [Iterator α Id β] [IteratorLoop α Id n] [Finite α Id] :
+    ForIn' n (Iter.Total (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
+  forIn' it init f := Iter.instForIn'.forIn' it.it init f
+
+instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
+    [Iterator α Id β] [IteratorLoop α Id n] [Finite α Id] :
+    ForIn n (Iter.Total (α := α) β) β :=
+  haveI : ForIn' n (Iter.Total (α := α) β) β _ := Iter.Total.instForIn'
+  instForInOfForIn'
+
 instance {m : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] [Monad m] :
+    {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id m] [Monad m] :
     ForM m (Iter (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
 instance {m : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] [Monad m] :
+    {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id m] [Monad m] :
     ForM m (Iter.Partial (α := α) β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
+instance {m : Type x → Type x'}
+    {α : Type w} {β : Type w} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id] :
+    ForM m (Iter.Total (α := α) β) β where
+  forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
+
 /--
 Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
 The accumulated value is combined with the each element of the list in order, using `f`.
 
 It is equivalent to `it.toList.foldlM`.
-
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.foldM` instead of `it.foldM`. However, it is not possible to formally
-verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
 def Iter.foldM {m : Type x → Type x'} [Monad m]
-    {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
+    {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
     [IteratorLoop α Id m] (f : γ → β → m γ)
     (init : γ) (it : Iter (α := α) β) : m γ :=
   ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
@@ -101,29 +115,39 @@ The accumulated value is combined with the each element of the list in order, us
 
 It is equivalent to `it.toList.foldlM`.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.foldM` instead.
+This function is deprecated. Instead of `it.allowNontermination.foldM`, use `it.foldM`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, deprecated Iter.foldM (since := "2025-12-04")]
 def Iter.Partial.foldM {m : Type x → Type x'} [Monad m]
     {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
-    [IteratorLoopPartial α Id m] (f : γ → β → m γ)
+    [IteratorLoop α Id m] (f : γ → β → m γ)
     (init : γ) (it : Iter.Partial (α := α) β) : m γ :=
-  ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
+  it.it.foldM (init := init) f
+
+/--
+Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+It is equivalent to `it.toList.foldlM`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.foldM`.
+-/
+@[always_inline, inline]
+def Iter.Total.foldM {m : Type x → Type x'} [Monad m]
+    {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
+    [IteratorLoop α Id m] [Finite α Id] (f : γ → β → m γ)
+    (init : γ) (it : Iter.Total (α := α) β) : m γ :=
+  it.it.foldM (init := init) f
 
 /--
 Folds a function over an iterator from the left, accumulating a value starting with `init`.
 The accumulated value is combined with the each element of the list in order, using `f`.
 
 It is equivalent to `it.toList.foldl`.
-
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.fold` instead of `it.fold`. However, it is not possible to formally
-verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
-def Iter.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
+def Iter.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
     [IteratorLoop α Id Id] (f : γ → β → γ)
     (init : γ) (it : Iter (α := α) β) : γ :=
   ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
@@ -134,14 +158,28 @@ The accumulated value is combined with the each element of the list in order, us
 
 It is equivalent to `it.toList.foldl`.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.fold` instead.
+This function is deprecated. Instead of `it.allowNontermination.fold`, use `it.fold`.
+-/
+@[always_inline, inline, deprecated Iter.fold (since := "2025-12-04")]
+def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
+    [IteratorLoop α Id Id] (f : γ → β → γ)
+    (init : γ) (it : Iter.Partial (α := α) β) : γ :=
+  it.it.fold (init := init) f
+
+/--
+Folds a function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+It is equivalent to `it.toList.foldl`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.fold`.
 -/
 @[always_inline, inline]
-def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
-    [IteratorLoopPartial α Id Id] (f : γ → β → γ)
-    (init : γ) (it : Iter.Partial (α := α) β) : γ :=
-  ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
+def Iter.Total.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
+    [IteratorLoop α Id Id] [Finite α Id] (f : γ → β → γ)
+    (init : γ) (it : Iter.Total (α := α) β) : γ :=
+  it.it.fold (init := init) f
 
 set_option doc.verso true in
 /--
@@ -151,9 +189,9 @@ any element emitted by the iterator {name}`it`.
 {lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
 examined in order of iteration.
 -/
-@[specialize]
+@[always_inline]
 def Iter.anyM {α β : Type w} {m : Type → Type w'} [Monad m]
-    [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
+    [Iterator α Id β] [IteratorLoop α Id m]
     (p : β → m Bool) (it : Iter (α := α) β) : m Bool :=
   ForIn.forIn it false (fun x _ => do
     if ← p x then
@@ -161,6 +199,23 @@ def Iter.anyM {α β : Type w} {m : Type → Type w'} [Monad m]
     else
       return .yield false)
 
+set_option doc.verso true in
+/--
+Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
+any element emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+examined in order of iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`Iter.anyM`.
+-/
+@[always_inline, inline]
+def Iter.Total.anyM {α β : Type w} {m : Type → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
+    (p : β → m Bool) (it : Iter.Total (α := α) β) : m Bool :=
+  it.it.anyM p
+
 set_option doc.verso true in
 /--
 Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
@@ -171,21 +226,38 @@ examined in order of iteration.
 -/
 @[inline]
 def Iter.any {α β : Type w}
-    [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
+    [Iterator α Id β] [IteratorLoop α Id Id]
     (p : β → Bool) (it : Iter (α := α) β) : Bool :=
   (it.anyM (fun x => pure (f := Id) (p x))).run
 
 set_option doc.verso true in
 /--
-Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
-all elements emitted by the iterator {name}`it`.
+Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
+any element emitted by the iterator {name}`it`.
 
-{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+examined in order of iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`Iter.any`.
+-/
+@[inline]
+def Iter.Total.any {α β : Type w}
+    [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
+    (p : β → Bool) (it : Iter.Total (α := α) β) : Bool :=
+  it.it.any p
+
+set_option doc.verso true in
+/--
+Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
+all element emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
 examined in order of iteration.
 -/
-@[specialize]
+@[always_inline, inline]
 def Iter.allM {α β : Type w} {m : Type → Type w'} [Monad m]
-    [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
+    [Iterator α Id β] [IteratorLoop α Id m]
     (p : β → m Bool) (it : Iter (α := α) β) : m Bool :=
   ForIn.forIn it true (fun x _ => do
     if ← p x then
@@ -195,36 +267,82 @@ def Iter.allM {α β : Type w} {m : Type → Type w'} [Monad m]
 
 set_option doc.verso true in
 /--
-Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
-all elements emitted by the iterator {name}`it`.
+Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
+all element emitted by the iterator {name}`it`.
 
-{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+examined in order of iteration.
+
+This variant terminates after finitely mall steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`Iter.allM`.
+-/
+@[always_inline, inline]
+def Iter.Total.allM {α β : Type w} {m : Type → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
+    (p : β → m Bool) (it : Iter.Total (α := α) β) : m Bool :=
+  it.it.allM p
+
+set_option doc.verso true in
+/--
+Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
+all element emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
 examined in order of iteration.
 -/
 @[inline]
 def Iter.all {α β : Type w}
-    [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
+    [Iterator α Id β] [IteratorLoop α Id Id]
     (p : β → Bool) (it : Iter (α := α) β) : Bool :=
   (it.allM (fun x => pure (f := Id) (p x))).run
 
+set_option doc.verso true in
 /--
-Steps through the iterator until the monadic function `f` returns `some` for an element, at which
-point iteration stops and the result of `f` is returned. If the iterator is completely consumed
-without `f` returning `some`, then the result is `none`.
+Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
+all element emitted by the iterator {name}`it`.
+
+{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+examined in order of iteration.
+
+This variant terminates after finitely mall steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`Iter.all`.
+-/
+@[inline]
+def Iter.Total.all {α β : Type w}
+    [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
+    (p : β → Bool) (it : Iter.Total (α := α) β) : Bool :=
+  it.it.all p
+
+/--
+Returns the first non-`none` result of applying the monadic function `f` to each output
+of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
+examined in order of iteration.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.findSomeM?` always terminates after finitely many steps.
+
+Example:
+```lean example
+#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
+  if i < 5 then
+    return some (i * 10)
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return none
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 10
+```
 -/
 @[inline]
 def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m] [Iterator α Id β]
-    [IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (Option γ)) :
-    m (Option γ) :=
-  ForIn.forIn it none (fun x _ => do
-    match ← f x with
-    | none => return .yield none
-    | some fx => return .done (some fx))
-
-@[inline, inherit_doc Iter.findSomeM?]
-def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
-    [Iterator α Id β] [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β)
-    (f : β → m (Option γ)) :
+    [IteratorLoop α Id m] (it : Iter (α := α) β) (f : β → m (Option γ)) :
     m (Option γ) :=
   ForIn.forIn it none (fun x _ => do
     match ← f x with
@@ -232,52 +350,284 @@ def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type
     | some fx => return .done (some fx))
 
 /--
-Steps through the iterator until `f` returns `some` for an element, at which point iteration stops
-and the result of `f` is returned. If the iterator is completely consumed without `f` returning
-`some`, then the result is `none`.
+Returns the first non-`none` result of applying the monadic function `f` to each output
+of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
+examined in order of iteration.
+
+This function is deprecated. Instead of `it.allowNontermination.findSomeM?`, use `it.findSomeM?`.
+
+Example:
+```lean example
+#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
+  if i < 5 then
+    return some (i * 10)
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return none
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 10
+```
+-/
+@[inline, deprecated Iter.findSomeM? (since := "2025-12-04")]
+def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] (it : Iter.Partial (α := α) β)
+    (f : β → m (Option γ)) :
+    m (Option γ) :=
+  it.it.findSomeM? f
+
+/--
+Returns the first non-`none` result of applying the monadic function `f` to each output
+of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
+examined in order of iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.findSomeM?`.
+
+Example:
+```lean example
+#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
+  if i < 5 then
+    return some (i * 10)
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return none
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 10
+```
+-/
+@[inline]
+def Iter.Total.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id] (it : Iter.Total (α := α) β)
+    (f : β → m (Option γ)) :
+    m (Option γ) :=
+  it.it.findSomeM? f
+
+/--
+Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
+Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
+iteration.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.findSome?` always terminates after finitely many steps.
+
+Examples:
+ * `[7, 6, 5, 8, 1, 2, 6].iter.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
+ * `[7, 6, 5, 8, 1, 2, 6].iter.findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
 @[inline]
 def Iter.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
-    [IteratorLoop α Id Id] [Finite α Id] (it : Iter (α := α) β) (f : β → Option γ) :
-    Option γ :=
-  Id.run (it.findSomeM? (pure <| f ·))
-
-@[inline, inherit_doc Iter.findSome?]
-def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
-    [IteratorLoopPartial α Id Id] (it : Iter.Partial (α := α) β) (f : β → Option γ) :
+    [IteratorLoop α Id Id] (it : Iter (α := α) β) (f : β → Option γ) :
     Option γ :=
   Id.run (it.findSomeM? (pure <| f ·))
 
 /--
-Steps through the iterator until an element satisfies the monadic predicate `f`, at which point
-iteration stops and the element is returned. If no element satisfies `f`, then the result is
-`none`.
+Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
+Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
+iteration.
+
+This function is deprecated. Instead of `it.allowNontermination.findSome?`, use `it.findSome?`.
+
+Examples:
+ * `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
+ * `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
+-/
+@[inline, deprecated Iter.findSome? (since := "2025-12-04")]
+def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
+    [IteratorLoop α Id Id] (it : Iter.Partial (α := α) β) (f : β → Option γ) :
+    Option γ :=
+  it.it.findSome? f
+
+/--
+Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
+Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
+iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.findSome?`.
+
+Examples:
+ * `[7, 6, 5, 8, 1, 2, 6].iter.ensureTermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
+ * `[7, 6, 5, 8, 1, 2, 6].iter.ensureTermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
+-/
+@[inline]
+def Iter.Total.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
+    [IteratorLoop α Id Id] [Finite α Id] (it : Iter.Total (α := α) β) (f : β → Option γ) :
+    Option γ :=
+  it.it.findSome? f
+
+/--
+Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
+`none` if no such element is found.
+
+`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
+iteration.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.findM?` always terminates after finitely many steps.
+
+Example:
+```lean example
+#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
+  if i < 5 then
+    return true
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return false
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 1
+```
 -/
 @[inline]
 def Iter.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
-    [IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (ULift Bool)) :
-    m (Option β) :=
-  it.findSomeM? (fun x => return if (← f x).down then some x else none)
-
-@[inline, inherit_doc Iter.findM?]
-def Iter.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
-    [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β) (f : β → m (ULift Bool)) :
+    [IteratorLoop α Id m] (it : Iter (α := α) β) (f : β → m (ULift Bool)) :
     m (Option β) :=
   it.findSomeM? (fun x => return if (← f x).down then some x else none)
 
 /--
-Steps through the iterator until an element satisfies `f`, at which point iteration stops and the
-element is returned. If no element satisfies `f`, then the result is `none`.
+Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
+`none` if no such element is found.
+
+`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
+iteration.
+
+This function is deprecated. Instead of `it.ensureTermination.findM?`, use `it.findM?`.
+
+Example:
+```lean example
+#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
+  if i < 5 then
+    return true
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return false
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 1
+```
+-/
+@[inline, deprecated Iter.findM? (since := "2025-12-04")]
+def Iter.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
+    [IteratorLoop α Id m] (it : Iter.Partial (α := α) β) (f : β → m (ULift Bool)) :
+    m (Option β) :=
+  it.it.findM? f
+
+/--
+Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
+`none` if no such element is found.
+
+`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
+iteration.
+
+This variant requires terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.findM?`.
+
+Example:
+```lean example
+#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
+  if i < 5 then
+    return true
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return false
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 1
+```
+-/
+@[inline]
+def Iter.Total.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
+    [IteratorLoop α Id m] [Finite α Id] (it : Iter.Total (α := α) β) (f : β → m (ULift Bool)) :
+    m (Option β) :=
+  it.it.findM? f
+
+/--
+Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
+no such output is found.
+
+`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
+order of iteration.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.find?` always terminates after finitely many steps.
+
+Examples:
+* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 5) = some 1`
+* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 1) = none`
 -/
 @[inline]
 def Iter.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
-    [Finite α Id] (it : Iter (α := α) β) (f : β → Bool) : Option β :=
+    (it : Iter (α := α) β) (f : β → Bool) : Option β :=
   Id.run (it.findM? (pure <| .up <| f ·))
 
-@[inline, inherit_doc Iter.find?]
-def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
+/--
+Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
+no such output is found.
+
+`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
+order of iteration.
+
+This function is deprecated. Instead of `it.allowNontermination.find?`, use `it.find?`.
+
+Examples:
+* `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.find? (· < 5) = some 1`
+* `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.find? (· < 1) = none`
+-/
+@[inline, deprecated Iter.find? (since := "2025-12-04")]
+def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter.Partial (α := α) β) (f : β → Bool) : Option β :=
-  Id.run (it.findM? (pure <| .up <| f ·))
+  it.it.find? f
+
+/--
+Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
+no such output is found.
+
+`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
+order of iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.find?`.
+
+Examples:
+* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 5) = some 1`
+* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 1) = none`
+-/
+@[inline]
+def Iter.Total.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
+    (it : Iter.Total (α := α) β) (f : β → Bool) : Option β :=
+  it.it.find? f
 
 /--
 Steps through the whole iterator, counting the number of outputs emitted.
@@ -287,7 +637,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
 This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline, expose]
-def Iter.count {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+def Iter.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter (α := α) β) : Nat :=
   it.toIterM.count.run.down
 
@@ -299,7 +649,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
 This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline, expose, deprecated Iter.count (since := "2025-10-29")]
-def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
+def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter (α := α) β) : Nat :=
    it.count
 
@@ -310,10 +660,10 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 This function's runtime is linear in the number of steps taken by the iterator.
 -/
-@[always_inline, inline, expose]
-def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
+@[always_inline, inline, expose, deprecated Iter.count (since := "2025-12-04")]
+def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter.Partial (α := α) β) : Nat :=
-  it.it.toIterM.allowNontermination.count.run.down
+  it.it.toIterM.count.run.down
 
 /--
 Steps through the whole iterator, counting the number of outputs emitted.
@@ -322,9 +672,9 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 This function's runtime is linear in the number of steps taken by the iterator.
 -/
-@[always_inline, inline, expose, deprecated Iter.Partial.count (since := "2025-10-29")]
-def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
+@[always_inline, inline, expose, deprecated Iter.count (since := "2025-10-29")]
+def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter.Partial (α := α) β) : Nat :=
-  it.count
+  it.it.count
 
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean b/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean
index 3627a18393..eee3d4e1b4 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Collect.lean
@@ -7,7 +7,9 @@ module
 
 prelude
 public import Init.Data.Iterators.Consumers.Monadic.Partial
+public import Init.Data.Iterators.Consumers.Monadic.Total
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
+public import Init.WFExtrinsicFix
 
 @[expose] public section
 
@@ -22,9 +24,9 @@ Concretely, the following operations are provided:
 * `IterM.toArray`, collecting the values in an array
 
 Some producers and combinators provide specialized implementations. These are captured by the
-`IteratorCollect` and `IteratorCollectPartial` typeclasses. They should be implemented by all
-types of iterators. A default implementation is provided. The typeclass `LawfulIteratorCollect`
-asserts that an `IteratorCollect` instance equals the default implementation.
+`IteratorCollect` type class. They should be implemented by all types of iterators. A default
+implementation is provided. The typeclass `LawfulIteratorCollect` asserts that an `IteratorCollect`
+instance equals the default implementation.
 -/
 
 namespace Std.Iterators
@@ -51,66 +53,58 @@ class IteratorCollect (α : Type w) (m : Type w → Type w') (n : Type w → Typ
   Maps the emitted values of an iterator using the given function and collects the results in an
   `Array`. This is an internal implementation detail. Consider using `it.map f |>.toArray` instead.
   -/
-  toArrayMapped [Finite α m] :
-    (lift : ⦃δ : Type w⦄ → m δ → n δ) → {γ : Type w} → (β → n γ) → IterM (α := α) m β → n (Array γ)
-
-/--
-`IteratorCollectPartial α m` provides efficient implementations of collectors for `α`-based
-iterators. Right now, it is limited to a potentially optimized partial `toArray` implementation.
-
-This class is experimental and users of the iterator API should not explicitly depend on it.
-They can, however, assume that consumers that require an instance will work for all iterators
-provided by the standard library.
--/
-class IteratorCollectPartial (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
-    {β : Type w} [Iterator α m β] where
-  /--
-  Maps the emitted values of an iterator using the given function and collects the results in an
-  `Array`. This is an internal implementation detail.
-  Consider using `it.map f |>.allowNontermination.toArray` instead.
-  -/
-  toArrayMappedPartial :
+  toArrayMapped :
     (lift : ⦃δ : Type w⦄ → m δ → n δ) → {γ : Type w} → (β → n γ) → IterM (α := α) m β → n (Array γ)
 
 end Typeclasses
 
 section ToArray
 
+def IterM.DefaultConsumers.toArrayMapped.RecursionRel {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β] {γ : Type w} (x' x : (_ : IterM (α := α) m β) ×' Array γ) : Prop :=
+  (∃ out, x.1.IsPlausibleStep (.yield x'.1 out) ∧ ∃ fx, x'.2 = x.2.push fx) ∨
+    (x.1.IsPlausibleStep (.skip x'.1) ∧ x'.2 = x.2)
+
 /--
 This is an internal function used in `IteratorCollect.defaultImplementation`.
 
 It iterates over an iterator and applies `f` whenever a value is emitted before inserting the result
 of `f` into an array.
 -/
-@[always_inline, inline]
+@[always_inline, no_expose]
 def IterM.DefaultConsumers.toArrayMapped {α β : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [Iterator α m β] [Finite α m]
+    {n : Type w → Type w''} [Monad n] [Iterator α m β]
     (lift : ⦃α : Type w⦄ → m α → n α) {γ : Type w} (f : β → n γ)
     (it : IterM (α := α) m β) : n (Array γ) :=
+  letI : MonadLift m n := ⟨lift (α := _)⟩
   go it #[]
 where
-  @[specialize]
-  go [Monad n] [Finite α m] (it : IterM (α := α) m β) a := letI : MonadLift m n := ⟨lift (α := _)⟩; do
-    match (← it.step).inflate with
-    | .yield it' b _ => go it' (a.push (← f b))
-    | .skip it' _ => go it' a
-    | .done _ => return a
-  termination_by it.finitelyManySteps
+  @[always_inline]
+  go it (acc : Array γ) : n (Array γ) :=
+    letI : MonadLift m n := ⟨lift (α := _)⟩
+    WellFounded.extrinsicFix₂ (C₂ := fun _ _ => n (Array γ)) (InvImage TerminationMeasures.Finite.Rel (·.1.finitelyManySteps!))
+    (fun (it : IterM (α := α) m β) acc recur => do
+      match (← it.step).inflate with
+      | .yield it' out h =>
+        recur it' (acc.push (← f out)) (by exact TerminationMeasures.Finite.rel_of_yield ‹_›)
+      | .skip it' h => recur it' acc (by exact TerminationMeasures.Finite.rel_of_skip ‹_›)
+      | .done _ => return acc) it acc
 
 /--
-This is the default implementation of the `IteratorLoop` class.
+This is the default implementation of the `IteratorCollect` class.
 It simply iterates through the iterator using `IterM.step`, incrementally building up the desired
 data structure. For certain iterators, more efficient implementations are possible and should be
 used instead.
 -/
-@[always_inline, inline]
+@[always_inline]
 def IteratorCollect.defaultImplementation {α β : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β] :
     IteratorCollect α m n where
   toArrayMapped := IterM.DefaultConsumers.toArrayMapped
 
 /--
-Asserts that a given `IteratorCollect` instance is equal to `IteratorCollect.defaultImplementation`.
+Asserts that a given `IteratorCollect` instance is equal to `IteratorCollect.defaultImplementation`
+*if the underlying iterator is finite*.
 (Even though equal, the given instance might be vastly more efficient.)
 -/
 class LawfulIteratorCollect (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
@@ -135,62 +129,38 @@ instance (α β : Type w) (m : Type w → Type w') (n : Type w → Type w'') [Mo
   letI : IteratorCollect α m n := .defaultImplementation
   ⟨fun _ => rfl⟩
 
-/--
-This is an internal function used in `IteratorCollectPartial.defaultImplementation`.
-
-It iterates over an iterator and applies `f` whenever a value is emitted before inserting the result
-of `f` into an array.
--/
-@[always_inline, inline]
-partial def IterM.DefaultConsumers.toArrayMappedPartial {α β : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [Iterator α m β]
-    (lift : {α : Type w} → m α → n α) {γ : Type w} (f : β → n γ)
-    (it : IterM (α := α) m β) : n (Array γ) :=
-  go it #[]
-where
-  @[specialize]
-  go [Monad n] (it : IterM (α := α) m β) a := letI : MonadLift m n := ⟨lift⟩; do
-    match (← it.step).inflate with
-    | .yield it' b _ => go it' (a.push (← f b))
-    | .skip it' _ => go it' a
-    | .done _ => return a
-
-/--
-This is the default implementation of the `IteratorLoopPartial` class.
-It simply iterates through the iterator using `IterM.step`, incrementally building up the desired
-data structure. For certain iterators, more efficient implementations are possible and should be
-used instead.
--/
-@[always_inline, inline]
-def IteratorCollectPartial.defaultImplementation {α β : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [Iterator α m β] :
-    IteratorCollectPartial α m n where
-  toArrayMappedPartial := IterM.DefaultConsumers.toArrayMappedPartial
-
 /--
 Traverses the given iterator and stores the emitted values in an array.
 
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.toArray` instead of `it.toArray`. However, it is not possible to formally
-verify the behavior of the partial variant.
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toArray` always terminates after finitely many steps.
 -/
 @[always_inline, inline]
-def IterM.toArray {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [Finite α m] [IteratorCollect α m m]
-    (it : IterM (α := α) m β) : m (Array β) :=
+def IterM.toArray {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorCollect α m m] (it : IterM (α := α) m β) : m (Array β) :=
   IteratorCollect.toArrayMapped (fun ⦃_⦄ => id) pure it
 
 /--
 Traverses the given iterator and stores the emitted values in an array.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.toArray` instead.
+This function is deprecated. Instead of `it.allowNontermination.toArray`, use `it.toArray`.
+-/
+@[always_inline, inline, deprecated IterM.toArray (since := "2025-10-23")]
+def IterM.Partial.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
+    [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollect α m m] : m (Array β) :=
+  it.it.toArray
+
+/--
+Traverses the given iterator and stores the emitted values in an array.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `IterM.toArray`.
 -/
 @[always_inline, inline]
-def IterM.Partial.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
-    [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollectPartial α m m] : m (Array β) :=
-  IteratorCollectPartial.toArrayMappedPartial (fun ⦃_⦄ => id) pure it.it
+def IterM.Total.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
+    [Iterator α m β] [Finite α m] (it : IterM.Total (α := α) m β) [IteratorCollect α m m] :
+    m (Array β) :=
+  it.it.toArray
 
 end ToArray
 
@@ -198,67 +168,82 @@ end ToArray
 Traverses the given iterator and stores the emitted values in reverse order in a list. Because
 lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
 
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.toListRev` instead of `it.toListRev`. However, it is not possible to
-formally verify the behavior of the partial variant.
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toListRev` always terminates after finitely many steps.
 -/
-@[inline]
+@[always_inline, inline]
 def IterM.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] [Finite α m] (it : IterM (α := α) m β) : m (List β) :=
+    [Iterator α m β] (it : IterM (α := α) m β) : m (List β) :=
   go it []
 where
-  go [Finite α m] it bs := do
-    match (← it.step).inflate with
-    | .yield it' b _ => go it' (b :: bs)
-    | .skip it' _ => go it' bs
-    | .done _ => return bs
-  termination_by it.finitelyManySteps
+  @[always_inline, inline]
+  go (it : IterM m β) acc :=
+    WellFounded.extrinsicFix₂ (InvImage TerminationMeasures.Finite.Rel (·.1.finitelyManySteps!))
+      (fun it acc recur => do
+        match (← it.step).inflate with
+        | .yield it' out h => recur it' (out :: acc) (TerminationMeasures.Finite.rel_of_yield h)
+        | .skip it' h => recur it' acc (TerminationMeasures.Finite.rel_of_skip h)
+        | .done _ => return acc) it acc
 
 /--
 Traverses the given iterator and stores the emitted values in reverse order in a list. Because
 lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.toListRev` instead.
+This function is deprecated. Instead of `it.allowNontermination.toListRev`, use `it.toListRev`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, deprecated IterM.toListRev (since := "2025-10-23")]
 partial def IterM.Partial.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
     [Iterator α m β] (it : IterM.Partial (α := α) m β) : m (List β) :=
-  go it.it []
-where
-  @[specialize]
-  go it bs := do
-    match (← it.step).inflate with
-    | .yield it' b _ => go it' (b :: bs)
-    | .skip it' _ => go it' bs
-    | .done _ => return bs
+  it.it.toListRev
+
+/--
+Traverses the given iterator and stores the emitted values in reverse order in a list. Because
+lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `IterM.toListRev`.
+-/
+@[always_inline, inline]
+def IterM.Total.toListRev {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
+    [Iterator α m β] [Finite α m] (it : IterM.Total (α := α) m β) :
+    m (List β) :=
+  it.it.toListRev
 
 /--
 Traverses the given iterator and stores the emitted values in a list. Because
 lists are prepend-only, `toListRev` is usually more efficient that `toList`.
 
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.toList` instead of `it.toList`. However, it is not possible to
-formally verify the behavior of the partial variant.
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toList` always terminates after finitely many steps.
 -/
 @[always_inline, inline]
 def IterM.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] [Finite α m] [IteratorCollect α m m] (it : IterM (α := α) m β) : m (List β) :=
+    [Iterator α m β] [IteratorCollect α m m] (it : IterM (α := α) m β) : m (List β) :=
   Array.toList <$> IterM.toArray it
 
 /--
 Traverses the given iterator and stores the emitted values in a list. Because
 lists are prepend-only, `toListRev` is usually more efficient that `toList`.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.toList` instead.
+This function is deprecated. Instead of `it.allowNontermination.toList`, use `it.toList`.
+-/
+@[always_inline, inline, deprecated IterM.toList (since := "2025-10-23")]
+def IterM.Partial.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollect α m m] :
+    m (List β) :=
+  Array.toList <$> it.it.toArray
+
+/--
+Traverses the given iterator and stores the emitted values in a list. Because
+lists are prepend-only, `toListRev` is usually more efficient that `toList`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `IterM.toList`.
 -/
 @[always_inline, inline]
-def IterM.Partial.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollectPartial α m m] :
+def IterM.Total.toList {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
+    [Iterator α m β] [Finite α m] (it : IterM.Total (α := α) m β) [IteratorCollect α m m] :
     m (List β) :=
-  Array.toList <$> it.toArray
+  it.it.toList
 
 end Std.Iterators
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
index 49f1a69949..31aabe1bc3 100644
--- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
@@ -8,6 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Consumers.Monadic.Partial
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
+public import Init.WFExtrinsicFix
+public import Init.Data.Iterators.Consumers.Monadic.Total
 
 public section
 
@@ -24,7 +26,7 @@ function in every iteration. Concretely, the following operations are provided:
   be used to apply the monadic effects of the iterator.
 
 Some producers and combinators provide specialized implementations. These are captured by the
-`IteratorLoop` and `IteratorLoopPartial` typeclasses. They should be implemented by all
+`IteratorLoop` type class. They should be implemented by all
 types of iterators. A default implementation is provided. The typeclass `LawfulIteratorLoop`
 asserts that an `IteratorLoop` instance equals the default implementation.
 -/
@@ -57,8 +59,9 @@ def IteratorLoop.WellFounded (α : Type w) (m : Type w → Type w') {β : Type w
 
 /--
 `IteratorLoop α m` provides efficient implementations of loop-based consumers for `α`-based
-iterators. The basis is a `ForIn`-style loop construct with the complication that it can be used
-for infinite iterators, too -- given a proof that the given loop will nevertheless terminate.
+iterators. The basis is a `ForIn`-style loop construct.
+
+Its behavior for well-founded loops is fully characterized by the `LawfulIteratorLoop` type class.
 
 This class is experimental and users of the iterator API should not explicitly depend on it.
 They can, however, assume that consumers that require an instance will work for all iterators
@@ -69,25 +72,10 @@ class IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterato
     (n : Type x → Type x') where
   forIn : ∀ (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x),
       (plausible_forInStep : β → γ → ForInStep γ → Prop) →
-      IteratorLoop.WellFounded α m plausible_forInStep →
       (it : IterM (α := α) m β) → γ →
       ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) →
       n γ
 
-/--
-`IteratorLoopPartial α m` provides efficient implementations of loop-based consumers for `α`-based
-iterators. The basis is a partial, i.e. potentially nonterminating, `ForIn` instance.
-
-This class is experimental and users of the iterator API should not explicitly depend on it.
-They can, however, assume that consumers that require an instance will work for all iterators
-provided by the standard library.
--/
-class IteratorLoopPartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
-    (n : Type x → Type x') where
-  forInPartial : ∀ (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) {γ : Type x},
-      (it : IterM (α := α) m β) → γ →
-      ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) → n γ
-
 end Typeclasses
 
 /-- Internal implementation detail of the iterator library. -/
@@ -108,27 +96,49 @@ instance IteratorLoop.WithWF.instWellFoundedRelation
 /--
 This is the loop implementation of the default instance `IteratorLoop.defaultImplementation`.
 -/
-@[specialize, expose]
+@[always_inline, inline, expose]
 def IterM.DefaultConsumers.forIn' {m : Type w → Type w'} {α : Type w} {β : Type w}
     [Iterator α m β]
     {n : Type x → Type x'} [Monad n]
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) (γ : Type x)
-    (plausible_forInStep : β → γ → ForInStep γ → Prop)
-    (wf : IteratorLoop.WellFounded α m plausible_forInStep)
+    (PlausibleForInStep : β → γ → ForInStep γ → Prop)
     (it : IterM (α := α) m β) (init : γ)
     (P : β → Prop) (hP : ∀ b, it.IsPlausibleIndirectOutput b → P b)
-    (f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ :=
+    (f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))) : n γ :=
+  haveI : Nonempty γ := ⟨init⟩
+  WellFounded.extrinsicFix₃ (C₃ := fun _ _ _ => n γ) (InvImage (IteratorLoop.rel α m PlausibleForInStep) (fun x => (x.1, x.2.1)))
+    (fun it acc (hP : ∀ b, it.IsPlausibleIndirectOutput b → P b) recur => (lift _ _ · it.step) fun s => do
+      match s.inflate with
+      | .yield it' out h =>
+        match ← f out (hP out <| .direct ⟨_, h⟩) acc with
+        | ⟨.yield c, h'⟩ => recur it' c (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') (Or.inl ⟨out, ‹_›, ‹_›⟩)
+        | ⟨.done c, h⟩ => return c
+      | .skip it' h => recur it' acc (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') (Or.inr ⟨‹_›, rfl⟩)
+      | .done _ => return acc) it init hP
+
+/--
+This is the loop implementation of the default instance `IteratorLoop.defaultImplementation`.
+-/
+@[specialize, expose]
+def IterM.DefaultConsumers.forIn'.wf {m : Type w → Type w'} {α : Type w} {β : Type w}
+    [Iterator α m β] {n : Type x → Type x'} [Monad n]
+    (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) (γ : Type x)
+    (PlausibleForInStep : β → γ → ForInStep γ → Prop)
+    (wf : IteratorLoop.WellFounded α m PlausibleForInStep)
+    (it : IterM (α := α) m β) (init : γ)
+    (P : β → Prop) (hP : ∀ b, it.IsPlausibleIndirectOutput b → P b)
+    (f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))) : n γ :=
   haveI : WellFounded _ := wf
   (lift _ _ · it.step) fun s =>
     match s.inflate with
     | .yield it' out h => do
       match ← f out (hP _ <| .direct ⟨_, h⟩) init with
       | ⟨.yield c, _⟩ =>
-        IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' c P
+        IterM.DefaultConsumers.forIn'.wf lift _ PlausibleForInStep wf it' c P
           (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
       | ⟨.done c, _⟩ => return c
     | .skip it' h =>
-      IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' init P
+      IterM.DefaultConsumers.forIn'.wf lift _ PlausibleForInStep wf it' init P
           (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
     | .done _ => return init
 termination_by IteratorLoop.WithWF.mk it init (hwf := wf)
@@ -136,38 +146,6 @@ decreasing_by
   · exact Or.inl ⟨out, ‹_›, ‹_›⟩
   · exact Or.inr ⟨‹_›, rfl⟩
 
-theorem IterM.DefaultConsumers.forIn'_eq_forIn' {m : Type w → Type w'} {α : Type w} {β : Type w}
-    [Iterator α m β]
-    {n : Type x → Type x'} [Monad n]
-    {lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
-    {Pl : β → γ → ForInStep γ → Prop}
-    {wf : IteratorLoop.WellFounded α m Pl}
-    {it : IterM (α := α) m β} {init : γ}
-    {P : β → Prop} {hP : ∀ b, it.IsPlausibleIndirectOutput b → P b}
-    {Q : β → Prop} {hQ : ∀ b, it.IsPlausibleIndirectOutput b → Q b}
-    {f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))}
-    {g : (b : β) → Q b → (c : γ) → n (Subtype (Pl b c))}
-    (hfg : ∀ b c, (hPb : P b) → (hQb : Q b) → f b hPb c = g b hQb c) :
-    IterM.DefaultConsumers.forIn' lift γ Pl wf it init P hP f =
-      IterM.DefaultConsumers.forIn' lift γ Pl wf it init Q hQ g := by
-  rw [forIn', forIn']
-  congr; ext step
-  split
-  · congr
-    · apply hfg
-    · ext
-      split
-      · apply IterM.DefaultConsumers.forIn'_eq_forIn'
-        assumption
-      · rfl
-  · apply IterM.DefaultConsumers.forIn'_eq_forIn'
-    assumption
-  · rfl
-termination_by IteratorLoop.WithWF.mk it init (hwf := wf)
-decreasing_by
-  · exact Or.inl ⟨_, ‹_›, ‹_›⟩
-  · exact Or.inr ⟨‹_›, rfl⟩
-
 /--
 This is the default implementation of the `IteratorLoop` class.
 It simply iterates through the iterator using `IterM.step`. For certain iterators, more efficient
@@ -177,7 +155,7 @@ implementations are possible and should be used instead.
 def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type x → Type x'}
     [Monad n] [Iterator α m β] :
     IteratorLoop α m n where
-  forIn lift γ Pl wf it init := IterM.DefaultConsumers.forIn' lift γ Pl wf it init _ (fun _ => id)
+  forIn lift γ Pl it init := IterM.DefaultConsumers.forIn' lift γ Pl it init _ (fun _ => id)
 
 /--
 Asserts that a given `IteratorLoop` instance is equal to `IteratorLoop.defaultImplementation`.
@@ -185,49 +163,18 @@ Asserts that a given `IteratorLoop` instance is equal to `IteratorLoop.defaultIm
 -/
 class LawfulIteratorLoop (α : Type w) (m : Type w → Type w') (n : Type x → Type x')
     [Monad m] [Monad n] [Iterator α m β] [i : IteratorLoop α m n] where
-  lawful : ∀ lift [LawfulMonadLiftBindFunction lift], i.forIn lift =
-      IteratorLoop.defaultImplementation.forIn lift
-
-/--
-This is the loop implementation of the default instance `IteratorLoopPartial.defaultImplementation`.
--/
-@[specialize]
-partial def IterM.DefaultConsumers.forInPartial {m : Type w → Type w'} {α : Type w} {β : Type w}
-    [Iterator α m β]
-    {n : Type x → Type x'} [Monad n]
-    (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) (γ : Type x)
-    (it : IterM (α := α) m β) (init : γ)
-    (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) : n γ :=
-  (lift _ _ · it.step) fun s =>
-      match s.inflate with
-      | .yield it' out h => do
-        match ← f out (.direct ⟨_, h⟩) init with
-        | .yield c =>
-          IterM.DefaultConsumers.forInPartial lift _ it' c
-            fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
-        | .done c => return c
-      | .skip it' h =>
-        IterM.DefaultConsumers.forInPartial lift _ it' init
-          fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
-      | .done _ => return init
-
-/--
-This is the default implementation of the `IteratorLoopPartial` class.
-It simply iterates through the iterator using `IterM.step`. For certain iterators, more efficient
-implementations are possible and should be used instead.
--/
-@[always_inline, inline]
-def IteratorLoopPartial.defaultImplementation {α : Type w} {m : Type w → Type w'}
-    {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorLoopPartial α m n where
-  forInPartial lift := IterM.DefaultConsumers.forInPartial lift _
+  lawful lift [LawfulMonadLiftBindFunction lift] γ it init
+      (Pl : β → γ → ForInStep γ → Prop) (wf : IteratorLoop.WellFounded α m Pl)
+      (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) :
+    i.forIn lift γ Pl it init f =
+      IteratorLoop.defaultImplementation.forIn lift γ Pl it init f
 
 instance (α : Type w) (m : Type w → Type w') (n : Type x → Type x')
     [Monad m] [Monad n] [Iterator α m β] [Finite α m] :
     letI : IteratorLoop α m n := .defaultImplementation
-    LawfulIteratorLoop α m n :=
+    LawfulIteratorLoop α m n := by
   letI : IteratorLoop α m n := .defaultImplementation
-  ⟨fun _ => rfl⟩
+  constructor; simp
 
 theorem IteratorLoop.wellFounded_of_finite {m : Type w → Type w'}
     {α β : Type w} {γ : Type x} [Iterator α m β] [Finite α m] :
@@ -247,13 +194,11 @@ This `ForIn'`-style loop construct traverses a finite iterator using an `Iterato
 -/
 @[always_inline, inline]
 def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n]
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) :
     ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
   forIn' {γ} it init f :=
-    IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
-      wellFounded_of_finite
-      it init (fun out h acc => (⟨·, .intro⟩) <$> f out h acc)
+    IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True) it init (return ⟨← f · · ·, trivial⟩)
 
 /--
 A `ForIn'` instance for iterators. Its generic membership relation is not easy to use,
@@ -262,13 +207,13 @@ or future library improvements will make it more comfortable.
 -/
 @[always_inline, inline]
 def IterM.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n]
     [MonadLiftT m n] :
     ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ :=
   IteratorLoop.finiteForIn' (fun _ _ f x => monadLift x >>= f)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n]
     [MonadLiftT m n] [Monad n] :
     ForIn n (IterM (α := α) m β) β :=
   haveI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
@@ -276,44 +221,55 @@ instance {m : Type w → Type w'} {n : Type w → Type w''}
 
 @[always_inline, inline]
 def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] [Monad n] :
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] :
     ForIn' n (IterM.Partial (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
-  forIn' it init f := IteratorLoopPartial.forInPartial (α := α) (m := m) (n := n)
-      (fun _ _ f x => monadLift x >>= f) it.it init f
+  forIn' it init f :=
+    haveI := @IterM.instForIn'; forIn' it.it init f
+
+@[always_inline, inline]
+def IterM.Total.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n]
+    [Finite α m] :
+    ForIn' n (IterM.Total (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
+  forIn' it init f := IterM.instForIn'.forIn' it.it init f
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] [Monad n] :
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] :
     ForIn n (IterM.Partial (α := α) m β) β :=
   haveI : ForIn' n (IterM.Partial (α := α) m β) β _ := IterM.Partial.instForIn'
   instForInOfForIn'
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n] [Monad n]
-    [MonadLiftT m n] :
-    ForM n (IterM (α := α) m β) β where
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n]
+    [Finite α m] :
+    ForIn n (IterM.Total (α := α) m β) β :=
+  haveI : ForIn' n (IterM.Total (α := α) m β) β _ := IterM.Total.instForIn'
+  instForInOfForIn'
+
+instance {m : Type w → Type w'} {n : Type w → Type w''} {α : Type w} {β : Type w} [Iterator α m β]
+    [IteratorLoop α m n] [Monad n] [MonadLiftT m n] : ForM n (IterM (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
-instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [Monad n]
-    [MonadLiftT m n] :
+instance {m : Type w → Type w'} {n : Type w → Type w''} {α : Type w} {β : Type w} [Monad n]
+    [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] :
     ForM n (IterM.Partial (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
+instance {m : Type w → Type w'} {n : Type w → Type w''} {α : Type w} {β : Type w} [Iterator α m β]
+    [IteratorLoop α m n] [Monad n] [MonadLiftT m n] [Finite α m] :
+    ForM n (IterM.Total (α := α) m β) β where
+  forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
+
 /--
 Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
 The accumulated value is combined with the each element of the list in order, using `f`.
 
 The monadic effects of `f` are interleaved with potential effects caused by the iterator's step
 function. Therefore, it may *not* be equivalent to `(← it.toList).foldlM`.
-
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.foldM` instead of `it.foldM`. However, it is not possible to formally
-verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
 def IterM.foldM {m : Type w → Type w'} {n : Type w → Type w''} [Monad n]
-    {α : Type w} {β : Type w} {γ : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
+    {α : Type w} {β : Type w} {γ : Type w} [Iterator α m β] [IteratorLoop α m n]
     [MonadLiftT m n]
     (f : γ → β → n γ) (init : γ) (it : IterM (α := α) m β) : n γ :=
   ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
@@ -325,31 +281,40 @@ The accumulated value is combined with the each element of the list in order, us
 The monadic effects of `f` are interleaved with potential effects caused by the iterator's step
 function. Therefore, it may *not* be equivalent to `it.toList.foldlM`.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.foldM` instead.
+This function is deprecated. Instead of `it.allowNontermination.foldM`, use `it.foldM`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, deprecated IterM.foldM (since := "2025-12-04")]
 def IterM.Partial.foldM {m : Type w → Type w'} {n : Type w → Type w'} [Monad n]
-    {α : Type w} {β : Type w} {γ : Type w} [Iterator α m β] [IteratorLoopPartial α m n]
-    [MonadLiftT m n]
+    {α : Type w} {β : Type w} {γ : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n]
     (f : γ → β → n γ) (init : γ) (it : IterM.Partial (α := α) m β) : n γ :=
   ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
 
+/--
+Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+The monadic effects of `f` are interleaved with potential effects caused by the iterator's step
+function. Therefore, it may *not* be equivalent to `it.toList.foldlM`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `IterM.foldM`.
+-/
+@[always_inline, inline]
+def IterM.Total.foldM {m : Type w → Type w'} {n : Type w → Type w'} [Monad n]
+    {α : Type w} {β : Type w} {γ : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n]
+    [Finite α m] (f : γ → β → n γ) (init : γ) (it : IterM.Total (α := α) m β) : n γ :=
+  it.it.foldM (init := init) f
+
 /--
 Folds a function over an iterator from the left, accumulating a value starting with `init`.
 The accumulated value is combined with the each element of the list in order, using `f`.
 
 It is equivalent to `it.toList.foldl`.
-
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.fold` instead of `it.fold`. However, it is not possible to formally
-verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
 def IterM.fold {m : Type w → Type w'} {α : Type w} {β : Type w} {γ : Type w} [Monad m]
-    [Iterator α m β] [Finite α m] [IteratorLoop α m m]
-    (f : γ → β → γ) (init : γ) (it : IterM (α := α) m β) : m γ :=
+    [Iterator α m β] [IteratorLoop α m m] (f : γ → β → γ) (init : γ) (it : IterM (α := α) m β) :
+    m γ :=
   ForIn.forIn (m := m) it init (fun x acc => pure (ForInStep.yield (f acc x)))
 
 /--
@@ -358,27 +323,36 @@ The accumulated value is combined with the each element of the list in order, us
 
 It is equivalent to `it.toList.foldl`.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.fold` instead.
+This function is deprecated. Instead of `it.allowNontermination.fold`, use `it.fold`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, deprecated IterM.Partial.fold (since := "2025-12-04")]
 def IterM.Partial.fold {m : Type w → Type w'} {α : Type w} {β : Type w} {γ : Type w}
-    [Monad m] [Iterator α m β] [IteratorLoopPartial α m m]
-    (f : γ → β → γ) (init : γ) (it : IterM.Partial (α := α) m β) : m γ :=
+    [Monad m] [Iterator α m β] [IteratorLoop α m m] (f : γ → β → γ) (init : γ)
+    (it : IterM.Partial (α := α) m β) : m γ :=
   ForIn.forIn (m := m) it init (fun x acc => pure (ForInStep.yield (f acc x)))
 
+/--
+Folds a function over an iterator from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+It is equivalent to `it.toList.foldl`.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `IterM.fold`.
+-/
+@[always_inline, inline]
+def IterM.Total.fold {m : Type w → Type w'} {α : Type w} {β : Type w} {γ : Type w}
+    [Monad m] [Iterator α m β] [IteratorLoop α m m] [Finite α m] (f : γ → β → γ) (init : γ)
+    (it : IterM.Total (α := α) m β) : m γ :=
+  it.it.fold (init := init) f
+
 /--
 Iterates over the whole iterator, applying the monadic effects of each step, discarding all
 emitted values.
-
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.drain` instead of `it.drain`. However, it is not possible to formally
-verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
 def IterM.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] [Finite α m] (it : IterM (α := α) m β) [IteratorLoop α m m] :
+    [Iterator α m β] (it : IterM (α := α) m β) [IteratorLoop α m m] :
     m PUnit :=
   it.fold (γ := PUnit) (fun _ _ => .unit) .unit
 
@@ -386,31 +360,36 @@ def IterM.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
 Iterates over the whole iterator, applying the monadic effects of each step, discarding all
 emitted values.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.drain` instead.
+This function is deprecated. Instead of `it.allowNontermination.drain`, use `it.drain`.
+-/
+@[always_inline, inline, deprecated IterM.drain (since := "2025-12-04")]
+def IterM.Partial.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorLoop α m m] : m PUnit :=
+  it.it.fold (γ := PUnit) (fun _ _ => .unit) .unit
+
+/--
+Iterates over the whole iterator, applying the monadic effects of each step, discarding all
+emitted values.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `IterM.drain`.
 -/
 @[always_inline, inline]
-def IterM.Partial.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorLoopPartial α m m] :
-    m PUnit :=
-  it.fold (γ := PUnit) (fun _ _ => .unit) .unit
+def IterM.Total.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] [Finite α m] (it : IterM.Total (α := α) m β) [IteratorLoop α m m] : m PUnit :=
+  it.it.drain
 
 set_option doc.verso true in
 /--
 Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
 any element emitted by the iterator {name}`it`.
 
-{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+{lit}`O(|it|)`. Short-circuits upon encountering the first match. The outputs of {name}`it` are
 examined in order of iteration.
-
-This function requires a {name}`Finite` instance proving that the iterator will finish after a
-finite number of steps. If the iterator is not finite or such an instance is not available,
-consider using {lit}`it.allowNontermination.anyM` instead of {lean}`it.anyM`. However, it is not
-possible to formally verify the behavior of the partial variant.
 -/
 @[specialize]
 def IterM.anyM {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [IteratorLoop α m m] [Finite α m]
+    [Iterator α m β] [IteratorLoop α m m]
     (p : β → m (ULift Bool)) (it : IterM (α := α) m β) : m (ULift Bool) :=
   ForIn.forIn it (ULift.up false) (fun x _ => do
     if (← p x).down then
@@ -423,39 +402,45 @@ set_option doc.verso true in
 Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
 any element emitted by the iterator {name}`it`.
 
-{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+{lit}`O(|it|)`. Short-circuits upon encountering the first match. The outputs of {name}`it` are
 examined in order of iteration.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.anyM`
-instead.
+This function is deprecated. Instead of {lit}`it.allowNontermination.anyM`, use {lit}`it.anyM`.
 -/
-@[specialize]
+@[always_inline, inline, deprecated IterM.anyM (since := "2025-12-04")]
 def IterM.Partial.anyM {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [IteratorLoopPartial α m m]
-    (p : β → m (ULift Bool)) (it : IterM.Partial (α := α) m β) : m (ULift Bool) :=
-  ForIn.forIn it (ULift.up false) (fun x _ => do
-    if (← p x).down then
-      return .done (.up true)
-    else
-      return .yield (.up false))
+    [Iterator α m β] [IteratorLoop α m m] (p : β → m (ULift Bool))
+    (it : IterM.Partial (α := α) m β) : m (ULift Bool) :=
+  it.it.anyM p
+
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
+any element emitted by the iterator {name}`it`.
+
+{lit}`O(|it|)`. Short-circuits upon encountering the first match. The outputs of {name}`it` are
+examined in order of iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`IterM.anyM`.
+-/
+@[always_inline, inline]
+def IterM.Total.anyM {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [IteratorLoop α m m] [Finite α m] (p : β → m (ULift Bool))
+    (it : IterM.Total (α := α) m β) : m (ULift Bool) :=
+  it.it.anyM p
 
 set_option doc.verso true in
 /--
 Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
 any element emitted by the iterator {name}`it`.
 
-{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+{lit}`O(|it|)`. Short-circuits upon encountering the first match. The outputs of {name}`it` are
 examined in order of iteration.
-
-This function requires a {name}`Finite` instance proving that the iterator will finish after a
-finite number of steps. If the iterator is not finite or such an instance is not available,
-consider using {lit}`it.allowNontermination.any` instead of {lean}`it.any`. However, it is not
-possible to formally verify the behavior of the partial variant.
 -/
 @[inline]
 def IterM.any {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [IteratorLoop α m m] [Finite α m]
+    [Iterator α m β] [IteratorLoop α m m]
     (p : β → Bool) (it : IterM (α := α) m β) : m (ULift Bool) := do
   it.anyM (fun x => pure (.up (p x)))
 
@@ -464,79 +449,96 @@ set_option doc.verso true in
 Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
 any element emitted by the iterator {name}`it`.
 
-{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
+{lit}`O(|it|)`. Short-circuits upon encountering the first match. The outputs of {name}`it` are
 examined in order of iteration.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.any`
-instead.
+This function is deprecated. Instead of {lit}`it.allowNontermination.any`, use {lit}`it.any`.
+-/
+@[inline, deprecated IterM.any (since := "2025-12-04")]
+def IterM.Partial.any {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] (p : β → Bool) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
+  it.it.any p
+
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
+any element emitted by the iterator {name}`it`.
+
+{lit}`O(|it|)`. Short-circuits upon encountering the first match. The outputs of {name}`it` are
+examined in order of iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`IterM.any`.
 -/
 @[inline]
-def IterM.Partial.any {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [IteratorLoopPartial α m m]
-    (p : β → Bool) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
-  it.anyM (fun x => pure (.up (p x)))
+def IterM.Total.any {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (p : β → Bool) (it : IterM.Total (α := α) m β) :
+    m (ULift Bool) := do
+  it.it.any p
 
 set_option doc.verso true in
 /--
 Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
 all elements emitted by the iterator {name}`it`.
 
-{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+{lit}`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of {name}`it` are
 examined in order of iteration.
-
-This function requires a {name}`Finite` instance proving that the iterator will finish after a
-finite number of steps. If the iterator is not finite or such an instance is not available,
-consider using {lit}`it.allowNontermination.allM` instead of {lean}`it.allM`. However, it is not
-possible to formally verify the behavior of the partial variant.
 -/
 @[specialize]
-def IterM.allM {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [IteratorLoop α m m] [Finite α m]
+def IterM.allM {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m]
     (p : β → m (ULift Bool)) (it : IterM (α := α) m β) : m (ULift Bool) := do
   ForIn.forIn it (ULift.up true) (fun x _ => do
     if (← p x).down then
       return .yield (.up true)
     else
       return .done (.up false))
+
 set_option doc.verso true in
 /--
 Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
 all elements emitted by the iterator {name}`it`.
 
-{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+{lit}`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of {name}`it` are
 examined in order of iteration.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.allM`
-instead.
+This function is deprecated. Instead of {lit}`it.allowNontermination.allM`, use {lit}`it.allM`.
 -/
-@[specialize]
-def IterM.Partial.allM {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [IteratorLoopPartial α m m]
-    (p : β → m (ULift Bool)) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
-  ForIn.forIn it (ULift.up true) (fun x _ => do
-    if (← p x).down then
-      return .yield (.up true)
-    else
-      return .done (.up false))
+@[always_inline, inline, deprecated IterM.allM (since := "2025-12-04")]
+def IterM.Partial.allM {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] (p : β → m (ULift Bool)) (it : IterM.Partial (α := α) m β) :
+    m (ULift Bool) := do
+  it.it.allM p
+
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the monadic predicate {name}`p` returns {lean}`ULift.up true` for
+all elements emitted by the iterator {name}`it`.
+
+{lit}`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of {name}`it` are
+examined in order of iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`IterM.allM`.
+-/
+@[always_inline, inline]
+def IterM.Total.allM {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (p : β → m (ULift Bool)) (it : IterM.Total (α := α) m β) :
+    m (ULift Bool) := do
+  it.it.allM p
 
 set_option doc.verso true in
 /--
 Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
 all elements emitted by the iterator {name}`it`.
 
-{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+{lit}`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of {name}`it` are
 examined in order of iteration.
 
-This function requires a {name}`Finite` instance proving that the iterator will finish after a
-finite number of steps. If the iterator is not finite or such an instance is not available,
-consider using {lit}`it.allowNontermination.all` instead of {lean}`it.all`. However, it is not
-possible to formally verify the behavior of the partial variant.
+If the iterator is not finite, this function might run forever. The variant
+{lit}`it.ensureTermination.toListRev` always terminates after finitely many steps.
 -/
 @[inline]
-def IterM.all {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [IteratorLoop α m m] [Finite α m]
+def IterM.all {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m]
     (p : β → Bool) (it : IterM (α := α) m β) : m (ULift Bool) := do
   it.allM (fun x => pure (.up (p x)))
 
@@ -545,72 +547,349 @@ set_option doc.verso true in
 Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
 all elements emitted by the iterator {name}`it`.
 
-{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
+{lit}`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of {name}`it` are
 examined in order of iteration.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a {name}`Finite` instance, consider using {name}`IterM.all`
-instead.
+This function is deprecated. Instead of {lit}`it.allowNontermination.allM`, use {lit}`it.allM`.
+-/
+@[inline, deprecated IterM.all (since := "2025-12-04")]
+def IterM.Partial.all {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] (p : β → Bool) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
+  it.it.all p
+
+set_option doc.verso true in
+/--
+Returns {lean}`ULift.up true` if the pure predicate {name}`p` returns {lean}`true` for
+all elements emitted by the iterator {name}`it`.
+
+{lit}`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of {name}`it` are
+examined in order of iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using {name}`IterM.all`.
 -/
 @[inline]
-def IterM.Partial.all {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [IteratorLoopPartial α m m]
-    (p : β → Bool) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
-  it.allM (fun x => pure (.up (p x)))
+def IterM.Total.all {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (p : β → Bool) (it : IterM.Total (α := α) m β) :
+    m (ULift Bool) := do
+  it.it.all p
 
+/--
+Returns the first non-`none` result of applying the monadic function `f` to each output
+of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
+examined in order of iteration.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.findSomeM?` always terminates after finitely many steps.
+
+Example:
+```lean example
+#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findSomeM? fun i => do
+  if i < 5 then
+    return some (i * 10)
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return none
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 10
+```
+-/
 @[inline]
 def IterM.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
-    [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → m (Option γ)) :
+    [IteratorLoop α m m] (it : IterM (α := α) m β) (f : β → m (Option γ)) :
     m (Option γ) :=
   ForIn.forIn it none (fun x _ => do
     match ← f x with
     | none => return .yield none
     | some fx => return .done (some fx))
 
-@[inline]
+/--
+Returns the first non-`none` result of applying the monadic function `f` to each output
+of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
+examined in order of iteration.
+
+This function is deprecated. Instead of `it.allowNontermination.findSomeM?`, use `it.findSomeM?`.
+
+Example:
+```lean example
+#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findSomeM? fun i => do
+  if i < 5 then
+    return some (i * 10)
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return none
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 10
+```
+-/
+@[inline, deprecated IterM.findSomeM? (since := "2025-12-04")]
 def IterM.Partial.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
-    [IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → m (Option γ)) :
+    [IteratorLoop α m m] (it : IterM.Partial (α := α) m β) (f : β → m (Option γ)) :
     m (Option γ) :=
-  ForIn.forIn it none (fun x _ => do
-    match ← f x with
-    | none => return .yield none
-    | some fx => return .done (some fx))
+  it.it.findSomeM? f
 
+/--
+Returns the first non-`none` result of applying the monadic function `f` to each output
+of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
+examined in order of iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `IterM.findSomeM?`.
+
+Example:
+```lean example
+#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findSomeM? fun i => do
+  if i < 5 then
+    return some (i * 10)
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return none
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 10
+```
+-/
+@[inline]
+def IterM.Total.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (it : IterM.Total (α := α) m β) (f : β → m (Option γ)) :
+    m (Option γ) :=
+  it.it.findSomeM? f
+
+/--
+Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
+Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
+iteration.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.findSome?` always terminates after finitely many steps.
+
+Examples:
+ * `([7, 6, 5, 8, 1, 2, 6].iterM Id).findSome? (fun x => if x < 5 then some (10 * x) else none) = pure (some 10)`
+ * `([7, 6, 5, 8, 1, 2, 6].iterM Id).findSome? (fun x => if x < 1 then some (10 * x) else none) = pure none`
+-/
 @[inline]
 def IterM.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
-    [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → Option γ) :
+    [IteratorLoop α m m] (it : IterM (α := α) m β) (f : β → Option γ) :
     m (Option γ) :=
   it.findSomeM? (pure <| f ·)
 
-@[inline]
+/--
+Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
+Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
+iteration.
+
+This function is deprecated. Instead of `it.allowNontermination.findSome?`, use `it.findSome?`.
+
+Examples:
+ * `([7, 6, 5, 8, 1, 2, 6].iterM Id).allowNontermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = pure (some 10)`
+ * `([7, 6, 5, 8, 1, 2, 6].iterM Id).allowNontermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = pure none`
+-/
+@[inline, deprecated IterM.findSome? (since := "2025-12-04")]
 def IterM.Partial.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
-    [IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → Option γ) :
+    [IteratorLoop α m m] (it : IterM.Partial (α := α) m β) (f : β → Option γ) :
     m (Option γ) :=
-  it.findSomeM? (pure <| f ·)
+  it.it.findSome? f
 
+/--
+Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
+Returns `none` if `f` returns `none` for all outputs.
+
+`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
+iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `IterM.findSome?`.
+
+Examples:
+ * `([7, 6, 5, 8, 1, 2, 6].iterM Id).ensureTermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = pure (some 10)`
+ * `([7, 6, 5, 8, 1, 2, 6].iterM Id).ensureTermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = pure none`
+-/
+@[inline]
+def IterM.Total.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (it : IterM.Partial (α := α) m β) (f : β → Option γ) :
+    m (Option γ) :=
+  it.it.findSome? f
+
+/--
+Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
+`none` if no such element is found.
+
+`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
+iteration.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.findM?` always terminates after finitely many steps.
+
+Example:
+```lean example
+#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findM? fun i => do
+  if i < 5 then
+    return true
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return false
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 1
+```
+-/
 @[inline]
 def IterM.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
-    [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → m (ULift Bool)) :
+    [IteratorLoop α m m] (it : IterM (α := α) m β) (f : β → m (ULift Bool)) :
     m (Option β) :=
   it.findSomeM? (fun x => return if (← f x).down then some x else none)
 
-@[inline]
+/--
+Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
+`none` if no such element is found.
+
+`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
+iteration.
+
+This function is deprecated. Instead of `it.allowNontermination.findM?`, use `it.findM?`.
+
+Example:
+```lean example
+#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findM? fun i => do
+  if i < 5 then
+    return true
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return false
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 1
+```
+-/
+@[inline, deprecated IterM.findM? (since := "2025-12-04")]
 def IterM.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
-    [IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → m (ULift Bool)) :
+    [IteratorLoop α m m] (it : IterM.Partial (α := α) m β) (f : β → m (ULift Bool)) :
     m (Option β) :=
-  it.findSomeM? (fun x => return if (← f x).down then some x else none)
+  it.it.findM? f
 
+/--
+Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
+`none` if no such element is found.
+
+`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
+iteration.
+
+This variant requires terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `IterM.findM?`.
+
+Example:
+```lean example
+#eval ([7, 6, 5, 8, 1, 2, 6].iterM IO).findM? fun i => do
+  if i < 5 then
+    return true
+  if i ≤ 6 then
+    IO.println s!"Almost! {i}"
+  return false
+```
+```output
+Almost! 6
+Almost! 5
+```
+```output
+some 1
+```
+-/
+@[inline]
+def IterM.Total.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (it : IterM.Total (α := α) m β) (f : β → m (ULift Bool)) :
+    m (Option β) :=
+  it.it.findM? f
+
+/--
+Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
+no such output is found.
+
+`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
+order of iteration.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.find?` always terminates after finitely many steps.
+
+Examples:
+* `([7, 6, 5, 8, 1, 2, 6].iterM Id).find? (· < 5) = pure (some 1)`
+* `([7, 6, 5, 8, 1, 2, 6].iterM Id).find? (· < 1) = pure none`
+-/
 @[inline]
 def IterM.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
-    [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → Bool) :
+    [IteratorLoop α m m] (it : IterM (α := α) m β) (f : β → Bool) :
     m (Option β) :=
   it.findM? (pure <| .up <| f ·)
 
-@[inline]
+/--
+Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
+no such output is found.
+
+`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
+order of iteration.
+
+This function is deprecated. Instead of `it.allowNontermination.find?`, use `it.find?`.
+
+Examples:
+* `([7, 6, 5, 8, 1, 2, 6].iterM Id).allowNontermination.find? (· < 5) = pure (some 1)`
+* `([7, 6, 5, 8, 1, 2, 6].iterM Id).allowNontermination.find? (· < 1) = pure none`
+-/
+@[inline, deprecated IterM.find? (since := "2025-12-04")]
 def IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
-    [IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → Bool) :
+    [IteratorLoop α m m] (it : IterM.Partial (α := α) m β) (f : β → Bool) :
     m (Option β) :=
-  it.findM? (pure <| .up <| f ·)
+  it.it.find? f
+
+/--
+Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
+no such output is found.
+
+`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
+order of iteration.
+
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `IterM.find?`.
+
+Examples:
+* `([7, 6, 5, 8, 1, 2, 6].iterM Id).find? (· < 5) = pure (some 1)`
+* `([7, 6, 5, 8, 1, 2, 6].iterM Id).find? (· < 1) = pure none`
+-/
+@[inline]
+def IterM.Total.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (it : IterM.Total (α := α) m β) (f : β → Bool) :
+    m (Option β) :=
+  it.it.find? f
 
 section Count
 
@@ -622,9 +901,8 @@ Steps through the whole iterator, counting the number of outputs emitted.
 This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline]
-def IterM.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m]
-    [IteratorLoop α m m]
-    [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
+def IterM.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    [IteratorLoop α m m] [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
   it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
 
 /--
@@ -635,9 +913,8 @@ Steps through the whole iterator, counting the number of outputs emitted.
 This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline, deprecated IterM.count (since := "2025-10-29")]
-def IterM.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m]
-    [IteratorLoop α m m]
-    [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
+def IterM.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    [IteratorLoop α m m] [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
   it.count
 
 /--
@@ -647,10 +924,10 @@ Steps through the whole iterator, counting the number of outputs emitted.
 
 This function's runtime is linear in the number of steps taken by the iterator.
 -/
-@[always_inline, inline]
+@[always_inline, inline, deprecated IterM.count (since := "2025-12-04")]
 def IterM.Partial.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
-  it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
+    [IteratorLoop α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
+  it.it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
 
 /--
 Steps through the whole iterator, counting the number of outputs emitted.
@@ -661,8 +938,8 @@ This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline, deprecated IterM.Partial.count (since := "2025-10-29")]
 def IterM.Partial.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
-  it.count
+    [IteratorLoop α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
+  it.it.count
 
 end Count
 
diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Total.lean b/src/Init/Data/Iterators/Consumers/Monadic/Total.lean
new file mode 100644
index 0000000000..862d3e38f2
--- /dev/null
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Total.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Basic
+
+set_option doc.verso true
+
+public section
+
+namespace Std.Iterators
+
+structure IterM.Total {α : Type w} (m : Type w → Type w') (β : Type w) where
+  it : IterM (α := α) m β
+
+/--
+For an iterator {name}`it`, {lean}`it.ensureTermination` provides variants of consumers that always
+terminate.
+-/
+@[always_inline, inline]
+def IterM.ensureTermination {α : Type w} {β : Type w} {m : Type w → Type w'}
+    (it : IterM (α := α) m β) :
+  IterM.Total (α := α) m β :=
+  ⟨it⟩
+
+/--
+A wrapper around an iterator that provides strictly terminating consumers. See
+{name}`IterM.ensureTermination`.
+-/
+add_decl_doc IterM.Total
+
+end Std.Iterators
diff --git a/src/Init/Data/Iterators/Consumers/Total.lean b/src/Init/Data/Iterators/Consumers/Total.lean
new file mode 100644
index 0000000000..907058adb3
--- /dev/null
+++ b/src/Init/Data/Iterators/Consumers/Total.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Iterators.Basic
+
+set_option doc.verso true
+
+public section
+
+namespace Std.Iterators
+
+structure Iter.Total {α : Type w} (β : Type w) where
+  it : Iter (α := α) β
+
+/--
+For an iterator {name}`it`, {lean}`it.ensureTermination` provides variants of consumers that always
+terminate.
+-/
+@[always_inline, inline]
+def Iter.ensureTermination {α : Type w} {β : Type w}
+    (it : Iter (α := α) β) :
+  Iter.Total (α := α) β :=
+  ⟨it⟩
+
+/--
+A wrapper around an iterator that provides strictly terminating consumers. See
+{name}`Iter.ensureTermination`.
+-/
+add_decl_doc Iter.Total
+
+end Std.Iterators
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index ff49d9257b..f885855b6d 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -247,9 +247,8 @@ instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     have : it = IterM.mapWithPostcondition _ it.internalState.inner := by rfl
     generalize it.internalState.inner = it at *
     cases this
-    simp only [LawfulIteratorCollect.toArrayMapped_eq]
     simp only [IteratorCollect.toArrayMapped]
-    rw [LawfulIteratorCollect.toArrayMapped_eq]
+    simp only [LawfulIteratorCollect.toArrayMapped_eq]
     induction it using IterM.inductSteps with | step it ih_yield ih_skip
     rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
     rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
@@ -487,13 +486,8 @@ theorem IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m]
   · simp [instIteratorMap, inferInstanceAs]
     congr
     simp
-  · refine heq_of_eqRec_eq ?_ rfl
-    congr
+  · congr
     simp only [Map, PostconditionT.map_pure, Function.comp_apply]
-    simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
-    congr
-    simp
-  · simp [Map]
   · simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
     congr
     simp
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
index 283bff26b1..b613eca24f 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
@@ -11,6 +11,8 @@ public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 public import Init.Data.Iterators.Consumers.Access
 import all Init.Data.Iterators.Consumers.Access
 import all Init.Data.Iterators.Consumers.Collect
+import all Init.Data.Iterators.Consumers.Total
+import all Init.Data.Iterators.Consumers.Monadic.Total
 
 public section
 
@@ -31,6 +33,23 @@ theorem Iter.toListRev_eq_toListRev_toIterM {α β} [Iterator α Id β] [Finite
     it.toListRev = it.toIterM.toListRev.run :=
   (rfl)
 
+@[simp]
+theorem Iter.toArray_ensureTermination {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
+    [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
+    it.ensureTermination.toArray = it.toArray :=
+  (rfl)
+
+@[simp]
+theorem Iter.toList_ensureTermination {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
+    [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
+    it.ensureTermination.toList = it.toList :=
+  (rfl)
+
+@[simp]
+theorem Iter.toListRev_ensureTermination_eq_toListRev {α β} [Iterator α Id β] [Finite α Id]
+    {it : Iter (α := α) β} : it.ensureTermination.toListRev = it.toListRev :=
+  (rfl)
+
 @[simp]
 theorem IterM.toList_toIter {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     {it : IterM (α := α) Id β} :
@@ -49,12 +68,22 @@ theorem Iter.toList_toArray {α β} [Iterator α Id β] [Finite α Id] [Iterator
     it.toArray.toList = it.toList := by
   simp [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray]
 
+theorem Iter.toList_toArray_ensureTermination {α β} [Iterator α Id β] [Finite α Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
+    it.ensureTermination.toArray.toList = it.toList := by
+  simp
+
 @[simp]
 theorem Iter.toArray_toList {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.toList.toArray = it.toArray := by
   simp [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toArray_toList]
 
+theorem Iter.toArray_toList_ensureTermination {α β} [Iterator α Id β] [Finite α Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
+    it.ensureTermination.toList.toArray = it.toArray := by
+  simp
+
 @[simp]
 theorem Iter.reverse_toListRev [Iterator α Id β] [Finite α Id]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
@@ -62,11 +91,21 @@ theorem Iter.reverse_toListRev [Iterator α Id β] [Finite α Id]
     it.toListRev.reverse = it.toList := by
   simp [toListRev_eq_toListRev_toIterM, toList_eq_toList_toIterM, ← IterM.reverse_toListRev]
 
+theorem Iter.reverse_toListRev_ensureTermination [Iterator α Id β] [Finite α Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
+    it.ensureTermination.toListRev.reverse = it.toList := by
+  simp
+
 theorem Iter.toListRev_eq {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.toListRev = it.toList.reverse := by
   simp [Iter.toListRev_eq_toListRev_toIterM, Iter.toList_eq_toList_toIterM, IterM.toListRev_eq]
 
+theorem Iter.toListRev_ensureTermination {α β} [Iterator α Id β] [Finite α Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
+    it.ensureTermination.toListRev = it.toList.reverse := by
+  simp [toListRev_eq]
+
 theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.toArray = match it.step.val with
@@ -78,6 +117,14 @@ theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [I
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn <;> simp
 
+theorem Iter.toArray_ensureTermination_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
+    [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
+    it.ensureTermination.toArray = match it.step.val with
+      | .yield it' out => #[out] ++ it'.toArray
+      | .skip it' => it'.toArray
+      | .done => #[] := by
+  rw [toArray_ensureTermination, toArray_eq_match_step]
+
 theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.toList = match it.step.val with
@@ -87,6 +134,14 @@ theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [It
   rw [← Iter.toList_toArray, Iter.toArray_eq_match_step]
   split <;> simp [Iter.toList_toArray]
 
+theorem Iter.toList_ensureTermination_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
+    [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
+    it.ensureTermination.toList = match it.step.val with
+      | .yield it' out => out :: it'.toList
+      | .skip it' => it'.toList
+      | .done => [] := by
+  rw [toList_ensureTermination, toList_eq_match_step]
+
 theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
     it.toListRev = match it.step.val with
       | .yield it' out => it'.toListRev ++ [out]
@@ -96,6 +151,13 @@ theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id]
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn <;> simp
 
+theorem Iter.toListRev_ensureTermination_eq_match_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
+    it.ensureTermination.toListRev = match it.step.val with
+      | .yield it' out => it'.toListRev ++ [out]
+      | .skip it' => it'.toListRev
+      | .done => [] := by
+  rw [toListRev_ensureTermination_eq_toListRev, toListRev_eq_match_step]
+
 theorem Iter.getElem?_toList_eq_atIdxSlow? {α β}
     [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
     {it : Iter (α := α) β} {k : Nat} :
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
index bd180bedb3..e8ca77ee62 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -23,22 +23,22 @@ theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
     {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → m (ForInStep γ)} :
     letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
     ForIn'.forIn' it init f =
-      IterM.DefaultConsumers.forIn' (fun _ _ f x => f x.run) γ (fun _ _ _ => True)
-        IteratorLoop.wellFounded_of_finite it.toIterM init _ (fun _ => id)
-          (fun out h acc => (⟨·, .intro⟩) <$>
-            f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
-  simp [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn', hl.lawful (fun γ δ f x => f x.run),
-    IteratorLoop.defaultImplementation]
+      IterM.DefaultConsumers.forIn' (n := m) (fun _ _ f x => f x.run) γ (fun _ _ _ => True)
+        it.toIterM init _ (fun _ => id)
+          (fun out h acc => return ⟨← f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc, trivial⟩) := by
+  simp only [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn']
+  have : ∀ a b c, f a b c = (Subtype.val <$> (⟨·, trivial⟩) <$> f a b c) := by simp
+  simp +singlePass only [this]
+  rw [hl.lawful (fun _ _ f x => f x.run) (wf := IteratorLoop.wellFounded_of_finite)]
+  simp [IteratorLoop.defaultImplementation]
 
 theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
     {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
     [hl : LawfulIteratorLoop α Id m] {γ : Type x} {it : Iter (α := α) β} {init : γ}
     {f : (b : β) → γ → m (ForInStep γ)} :
     ForIn.forIn it init f =
-      IterM.DefaultConsumers.forIn' (fun _ _ f c => f c.run) γ (fun _ _ _ => True)
-        IteratorLoop.wellFounded_of_finite it.toIterM init _ (fun _ => id)
-          (fun out _ acc => (⟨·, .intro⟩) <$>
-            f out acc) := by
+      IterM.DefaultConsumers.forIn' (n := m) (fun _ _ f c => f c.run) γ (fun _ _ _ => True)
+        it.toIterM init _ (fun _ => id) (fun out _ acc => return ⟨← f out acc, trivial⟩) := by
   simp [ForIn.forIn, forIn'_eq, -forIn'_eq_forIn]
 
 @[congr] theorem Iter.forIn'_congr {α β : Type w} {m : Type w → Type w'} [Monad m]
@@ -106,20 +106,24 @@ theorem Iter.forIn'_eq_match_step {α β : Type w} [Iterator α Id β]
             fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
       | .done _ => return init) := by
   simp only [forIn'_eq]
-  rw [IterM.DefaultConsumers.forIn'_eq_match_step]
-  simp only [bind_map_left, Iter.step]
+  rw [IterM.DefaultConsumers.forIn'_eq_match_step (fun _ _ _ => True)
+    IteratorLoop.wellFounded_of_finite]
+  simp only [Iter.step]
   cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn
-  · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
+  · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter,
+      bind_assoc]
     apply bind_congr
     intro forInStep
     cases forInStep
     · simp
-    · simp only
-      apply IterM.DefaultConsumers.forIn'_eq_forIn'
-      intros; congr
+    · simp only [pure_bind]
+      apply IterM.DefaultConsumers.forIn'_eq_forIn' (fun _ _ _ => True)
+        IteratorLoop.wellFounded_of_finite
+      · simp
   · simp only
-    apply IterM.DefaultConsumers.forIn'_eq_forIn'
-    intros; congr
+    apply IterM.DefaultConsumers.forIn'_eq_forIn' (fun _ _ _ => True)
+      IteratorLoop.wellFounded_of_finite
+    · simp
   · simp
 
 theorem Iter.forIn_eq_match_step {α β : Type w} [Iterator α Id β]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
index 5b333ae73d..10ab51f308 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
@@ -10,29 +10,49 @@ public import Init.Data.Array.Lemmas
 public import Init.Data.Iterators.Lemmas.Monadic.Basic
 public import Init.Data.Iterators.Consumers.Monadic.Collect
 import all Init.Data.Iterators.Consumers.Monadic.Collect
+import all Init.Data.Iterators.Consumers.Monadic.Total
+import all Init.WFExtrinsicFix
 
 public section
 
 namespace Std.Iterators
+open Std.Internal
 
 variable {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
   {lift : ⦃δ : Type w⦄ → m δ → n δ} {f : β → n γ} {it : IterM (α := α) m β}
 
-theorem IterM.DefaultConsumers.toArrayMapped.go.aux₁ [Monad n] [LawfulMonad n] [Iterator α m β]
-    [Finite α m] {b : γ} {bs : Array γ} :
+private theorem IterM.DefaultConsumers.toArrayMapped.go_eq [Monad n]
+    [Iterator α m β] [LawfulMonad n] [Finite α m] {acc : Array γ} :
+    letI : MonadLift m n := ⟨lift (δ := _)⟩
+    go lift f it acc (m := m) = (do
+      match (← it.step).inflate.val with
+      | .yield it' out => go lift f it' (acc.push (← f out))
+      | .skip it' => go lift f it' acc
+      | .done => return acc) := by
+  letI : MonadLift m n := ⟨lift (δ := _)⟩
+  rw [toArrayMapped.go, WellFounded.extrinsicFix₂_eq_apply]
+  · simp only
+    apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn
+    · apply bind_congr; intro fx
+      simp [go]
+    · simp [go]
+    · simp
+  · simp only [show (IterM.finitelyManySteps! = IterM.finitelyManySteps) by rfl]
+    apply InvImage.wf
+    exact WellFoundedRelation.wf
+
+private theorem IterM.DefaultConsumers.toArrayMapped.go.aux₁ [Monad n] [LawfulMonad n]
+    [Iterator α m β] [Finite α m] {b : γ} {bs : Array γ} :
     IterM.DefaultConsumers.toArrayMapped.go lift f it (#[b] ++ bs) (m := m) =
       (#[b] ++ ·) <$> IterM.DefaultConsumers.toArrayMapped.go lift f it bs (m := m) := by
-  induction it, bs using IterM.DefaultConsumers.toArrayMapped.go.induct with | _ it bs ih₁ ih₂
-  rw [go, map_eq_pure_bind, go, bind_assoc]
-  apply bind_congr
-  intro step
-  split
-  · simp [ih₁ _ _ ‹_›]
-  · simp [ih₂ _ ‹_›]
-  · simp
+  induction it using IterM.inductSteps generalizing bs with | step it ihy ihs
+  rw [go_eq, map_eq_pure_bind, go_eq, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn <;> simp (discharger := assumption) [ihy, ihs]
 
-theorem IterM.DefaultConsumers.toArrayMapped.go.aux₂ [Monad n] [LawfulMonad n] [Iterator α m β]
-    [Finite α m] {acc : Array γ} :
+private theorem IterM.DefaultConsumers.toArrayMapped.go.aux₂ [Monad n] [LawfulMonad n]
+    [Iterator α m β] [Finite α m] {acc : Array γ} :
     IterM.DefaultConsumers.toArrayMapped.go lift f it acc (m := m) =
       (acc ++ ·) <$> IterM.DefaultConsumers.toArrayMapped lift f it (m := m) := by
   rw [← Array.toArray_toList (xs := acc)]
@@ -51,12 +71,18 @@ theorem IterM.DefaultConsumers.toArrayMapped_eq_match_step [Monad n] [LawfulMona
         return #[← f out] ++ (← IterM.DefaultConsumers.toArrayMapped lift f it' (m := m))
       | .skip it' => IterM.DefaultConsumers.toArrayMapped lift f it' (m := m)
       | .done => return #[]) := by
-  rw [IterM.DefaultConsumers.toArrayMapped, IterM.DefaultConsumers.toArrayMapped.go]
+  rw [IterM.DefaultConsumers.toArrayMapped, IterM.DefaultConsumers.toArrayMapped.go_eq]
   apply bind_congr
   intro step
   cases step.inflate using PlausibleIterStep.casesOn <;>
     simp [IterM.DefaultConsumers.toArrayMapped.go.aux₂]
 
+@[simp]
+theorem IterM.toArray_ensureTermination [Monad m] [Iterator α m β] [Finite α m]
+    [IteratorCollect α m m] {it : IterM (α := α) m β} :
+    it.ensureTermination.toArray = it.toArray :=
+  (rfl)
+
 theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m] :
     it.toArray = (do
@@ -68,18 +94,43 @@ theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
   rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
   simp [bind_pure_comp, pure_bind]
 
+theorem IterM.toArray_ensureTermination_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
+    [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] :
+    it.ensureTermination.toArray = (do
+      match (← it.step).inflate.val with
+      | .yield it' out => return #[out] ++ (← it'.toArray)
+      | .skip it' => it'.toArray
+      | .done => return #[]) := by
+  rw [toArray_ensureTermination, toArray_eq_match_step]
+
+@[simp]
+theorem IterM.toList_ensureTermination [Monad m] [Iterator α m β] [Finite α m]
+    [IteratorCollect α m m] {it : IterM (α := α) m β} :
+    it.ensureTermination.toList = it.toList :=
+  (rfl)
+
 @[simp]
 theorem IterM.toList_toArray [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m]
     {it : IterM (α := α) m β} :
     Array.toList <$> it.toArray = it.toList := by
   simp [IterM.toList]
 
+theorem IterM.toList_toArray_ensureTermination [Monad m] [Iterator α m β] [Finite α m]
+    [IteratorCollect α m m] {it : IterM (α := α) m β} :
+    Array.toList <$> it.ensureTermination.toArray = it.toList := by
+  simp
+
 @[simp]
 theorem IterM.toArray_toList [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] {it : IterM (α := α) m β} :
     List.toArray <$> it.toList = it.toArray := by
   simp [IterM.toList, -toList_toArray]
 
+theorem IterM.toArray_toList_ensureTermination [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+    [IteratorCollect α m m] {it : IterM (α := α) m β} :
+    List.toArray <$> it.ensureTermination.toList = it.toArray := by
+  rw [toList_ensureTermination, toArray_toList]
+
 theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM (α := α) m β} :
     it.toList = (do
@@ -93,17 +144,49 @@ theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
   intro step
   split <;> simp
 
-theorem IterM.toListRev.go.aux₁ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+theorem IterM.toList_ensureTermination_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
+    [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM (α := α) m β} :
+    it.ensureTermination.toList = (do
+      match (← it.step).inflate.val with
+      | .yield it' out => return out :: (← it'.toList)
+      | .skip it' => it'.toList
+      | .done => return []) := by
+  rw [toList_ensureTermination, toList_eq_match_step]
+
+@[simp]
+theorem IterM.toListRev_ensureTermination_eq_toListRev [Monad m] [Iterator α m β] [Finite α m]
+    {it : IterM (α := α) m β} :
+    it.ensureTermination.toListRev = it.toListRev :=
+  (rfl)
+
+private theorem IterM.toListRev.go_eq [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+    {it : IterM (α := α) m β} {bs : List β} :
+    go it bs = (do
+      match (← it.step).inflate.val with
+      | .yield it' out => go it' (out :: bs)
+      | .skip it' => go it' bs
+      | .done => return bs) := by
+  rw [go, WellFounded.extrinsicFix₂_eq_apply]
+  · apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn <;> simp [go]
+  · simp only [show (IterM.finitelyManySteps! = IterM.finitelyManySteps) by rfl]
+    apply InvImage.wf
+    exact WellFoundedRelation.wf
+
+private theorem IterM.toListRev.go.aux₁ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     {it : IterM (α := α) m β} {b : β} {bs : List β} :
     IterM.toListRev.go it (bs ++ [b]) = (· ++ [b]) <$> IterM.toListRev.go it bs:= by
-  induction it, bs using IterM.toListRev.go.induct with | _ it bs ih₁ ih₂
-  rw [go, go, map_eq_pure_bind, bind_assoc]
+  induction it using IterM.inductSteps generalizing bs with | step it ihy ihs
+  rw [go_eq, go_eq, map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
-  simp only [List.cons_append] at ih₁
-  split <;> simp [*]
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simpa using ihy ‹_› (bs := _ :: bs)
+  · simpa using ihs ‹_›
+  · simp
 
-theorem IterM.toListRev.go.aux₂ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+
+private theorem IterM.toListRev.go.aux₂ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     {it : IterM (α := α) m β} {acc : List β} :
     IterM.toListRev.go it acc = (· ++ acc) <$> it.toListRev := by
   rw [← List.reverse_reverse (as := acc)]
@@ -120,11 +203,21 @@ theorem IterM.toListRev_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m 
       | .skip it' => it'.toListRev
       | .done => return []) := by
   simp [IterM.toListRev]
-  rw [toListRev.go]
+  rw [toListRev.go_eq]
   apply bind_congr
   intro step
   cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.toListRev.go.aux₂]
 
+theorem IterM.toListRev_ensureTermination_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
+    [Finite α m] {it : IterM (α := α) m β} :
+    it.ensureTermination.toListRev = (do
+      match (← it.step).inflate.val with
+      | .yield it' out => return (← it'.toListRev) ++ [out]
+      | .skip it' => it'.toListRev
+      | .done => return []) := by
+  rw [toListRev_ensureTermination_eq_toListRev, toListRev_eq_match_step]
+
+@[simp]
 theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m]
     {it : IterM (α := α) m β} :
@@ -137,19 +230,31 @@ theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β] [Fi
   intro step
   cases step.inflate using PlausibleIterStep.casesOn <;> simp (discharger := assumption) [ihy, ihs]
 
+@[simp]
+theorem IterM.reverse_toListRev_ensureTermination [Monad m] [LawfulMonad m] [Iterator α m β]
+    [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {it : IterM (α := α) m β} :
+    List.reverse <$> it.ensureTermination.toListRev = it.toList := by
+  rw [toListRev_ensureTermination_eq_toListRev, reverse_toListRev]
+
 theorem IterM.toListRev_eq [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m]
     {it : IterM (α := α) m β} :
     it.toListRev = List.reverse <$> it.toList := by
-  rw [← IterM.reverse_toListRev]
-  simp
+  simp [← IterM.reverse_toListRev]
+
+theorem IterM.toListRev_ensureTermination [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+    [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {it : IterM (α := α) m β} :
+    it.ensureTermination.toListRev = List.reverse <$> it.toList := by
+  simp [← IterM.reverse_toListRev]
 
 theorem LawfulIteratorCollect.toArray_eq {α β : Type w} {m : Type w → Type w'}
     [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m]
     [hl : LawfulIteratorCollect α m m]
     {it : IterM (α := α) m β} :
     it.toArray = (letI : IteratorCollect α m m := .defaultImplementation; it.toArray) := by
-  simp only [IterM.toArray, toArrayMapped_eq]
+  simp [IterM.toArray, toArrayMapped_eq, IteratorCollect.defaultImplementation]
 
 theorem LawfulIteratorCollect.toList_eq {α β : Type w} {m : Type w → Type w'}
     [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
index 959dd93ada..2fca7ebfbd 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
@@ -15,29 +15,75 @@ public section
 namespace Std.Iterators
 
 theorem IterM.DefaultConsumers.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'}
-    [Iterator α m β]
-    {n : Type x → Type x'} [Monad n]
+    [Iterator α m β] {n : Type x → Type x'} [Monad n] [LawfulMonad n]
     {lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
-    {plausible_forInStep : β → γ → ForInStep γ → Prop}
-    {wf : IteratorLoop.WellFounded α m plausible_forInStep}
     {it : IterM (α := α) m β} {init : γ}
-    {P hP} {f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))} :
-    IterM.DefaultConsumers.forIn' lift γ plausible_forInStep wf it init P hP f =
+    {P hP}
+    (PlausibleForInStep : β → γ → ForInStep γ → Prop)
+    {f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))}
+    (wf : IteratorLoop.WellFounded α m PlausibleForInStep) :
+    IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep it init P hP f =
       (lift _ _ · it.step) (fun s =>
           match s.inflate with
           | .yield it' out h => do
             match ← f out (hP _ <| .direct ⟨_, h⟩) init with
             | ⟨.yield c, _⟩ =>
-              IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' c P
+              IterM.DefaultConsumers.forIn' lift _ PlausibleForInStep it' c P
                 (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
             | ⟨.done c, _⟩ => return c
           | .skip it' h =>
-            IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' init P
+            IterM.DefaultConsumers.forIn' lift _ PlausibleForInStep it' init P
               (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
           | .done _ => return init) := by
-  rw [forIn']
-  congr; ext step
-  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
+  haveI : Nonempty γ := ⟨init⟩
+  rw [forIn', WellFounded.extrinsicFix₃_eq_apply]
+  · congr; ext step
+    cases step.inflate using PlausibleIterStep.casesOn
+    · simp only
+      apply bind_congr; intro step
+      split <;> simp [forIn']
+    · simp [forIn']
+    · simp
+  · apply InvImage.wf
+    exact wf
+
+theorem IterM.DefaultConsumers.forIn'_eq_wf {m : Type w → Type w'} {α : Type w} {β : Type w}
+    [Iterator α m β]
+    {n : Type x → Type x'} [Monad n] [LawfulMonad n]
+    {lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
+    (Pl : β → γ → ForInStep γ → Prop)
+    (wf : IteratorLoop.WellFounded α m Pl)
+    {it : IterM (α := α) m β} {init : γ}
+    {P : β → Prop} {hP : ∀ b, it.IsPlausibleIndirectOutput b → P b}
+    (f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))) :
+    forIn' lift γ Pl it init P hP f =
+      forIn'.wf lift γ Pl wf it init P hP f := by
+  haveI : Nonempty γ := ⟨init⟩
+  rw [forIn', WellFounded.extrinsicFix₃_eq_fix]; rotate_left
+  · apply InvImage.wf
+    exact wf
+  · fun_induction forIn'.wf lift γ Pl wf it init P hP f
+    rename_i ihy ihs
+    rw [WellFounded.fix_eq]
+    congr 1; ext step
+    cases step.inflate using PlausibleIterStep.casesOn
+    · apply bind_congr; intro forInStep
+      match forInStep with
+      | ⟨.yield c, h⟩ => simp (discharger := assumption) [ihy]
+      | ⟨.done c, h⟩ => simp
+    · simp (discharger := assumption) [ihs]
+    · simp
+
+theorem IterM.DefaultConsumers.forIn'_eq_wf_of_finite {m : Type w → Type w'} {α : Type w}
+    {β : Type w} [Iterator α m β] [Finite α m]
+    {n : Type x → Type x'} [Monad n] [LawfulMonad n]
+    {lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
+    {it : IterM (α := α) m β} {init : γ}
+    {P : β → Prop} {hP : ∀ b, it.IsPlausibleIndirectOutput b → P b}
+    (f : (b : β) → P b → (c : γ) → n (Subtype (fun _ => True))) :
+    forIn' lift γ (fun _ _ _ => True) it init P hP f =
+      forIn'.wf lift γ (fun _ _ _ => True) IteratorLoop.wellFounded_of_finite it init P hP f := by
+  apply forIn'_eq_wf
 
 theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n]
@@ -45,11 +91,12 @@ theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
     [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
     {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)} :
     letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
-    ForIn'.forIn' it init f = IterM.DefaultConsumers.forIn' (n := n)
-        (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True)
-        IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) ((⟨·, .intro⟩) <$> f · · ·) := by
-  simp [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn',
-    hl.lawful (fun _ _ f x => monadLift x >>= f), IteratorLoop.defaultImplementation]
+    ForIn'.forIn' (α := β) (m := n) it init f = IterM.DefaultConsumers.forIn' (n := n)
+        (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) it init _ (fun _ => id) (return ⟨← f · · ·, trivial⟩) := by
+  simp only [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn']
+  have : f = (Subtype.val <$> (⟨·, trivial⟩) <$> f · · ·) := by simp
+  rw [this, hl.lawful (fun _ _ f x => monadLift x >>= f) (wf := IteratorLoop.wellFounded_of_finite)]
+  simp [IteratorLoop.defaultImplementation]
 
 theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n]
@@ -57,13 +104,13 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
     [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
     {f : β → γ → n (ForInStep γ)} :
     ForIn.forIn it init f = IterM.DefaultConsumers.forIn' (n := n)
-        (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True)
-        IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by
+        (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) it init _ (fun _ => id)
+        (fun out _ acc => return ⟨← f out acc, trivial⟩) := by
   simp only [ForIn.forIn, forIn'_eq]
 
 @[congr] theorem IterM.forIn'_congr {α β : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Monad m]
-    [Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n]
+    [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n]
     {ita itb : IterM (α := α) m β} (w : ita = itb)
     {b b' : γ} (hb : b = b')
     {f : (a' : β) → _ → γ → n (ForInStep γ)}
@@ -78,7 +125,7 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
 
 @[congr] theorem IterM.forIn_congr {α β : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Monad m]
-    [Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n]
+    [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n]
     {ita itb : IterM (α := α) m β} (w : ita = itb)
     {b b' : γ} (hb : b = b')
     {f : (a' : β) → γ → n (ForInStep γ)}
@@ -89,6 +136,36 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
   simp only [← funext_iff] at h
   rw [← h]
 
+theorem IterM.DefaultConsumers.forIn'_eq_forIn' {m : Type w → Type w'} {α : Type w} {β : Type w}
+    [Iterator α m β]
+    {n : Type x → Type x'} [Monad n] [LawfulMonad n]
+    {lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
+    {it : IterM (α := α) m β} {init : γ}
+    {P : β → Prop} {hP : ∀ b, it.IsPlausibleIndirectOutput b → P b}
+    {Q : β → Prop} {hQ : ∀ b, it.IsPlausibleIndirectOutput b → Q b}
+    (Pl : β → γ → ForInStep γ → Prop)
+    {f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))}
+    {g : (b : β) → Q b → (c : γ) → n (Subtype (Pl b c))}
+    (wf : IteratorLoop.WellFounded α m Pl)
+    (hfg : ∀ b c, (hPb : P b) → (hQb : Q b) → f b hPb c = g b hQb c) :
+    IterM.DefaultConsumers.forIn' lift γ Pl it init P hP f =
+      IterM.DefaultConsumers.forIn' lift γ Pl it init Q hQ g := by
+  rw [forIn'_eq_match_step Pl wf, forIn'_eq_match_step Pl wf]
+  congr; ext step
+  split
+  · congr
+    · apply hfg
+    · ext forInStep
+      match forInStep with
+      | ⟨.yield _, h⟩ => apply IterM.DefaultConsumers.forIn'_eq_forIn' <;> assumption
+      | ⟨.done _, h⟩ => rfl
+  · apply IterM.DefaultConsumers.forIn'_eq_forIn' <;> assumption
+  · rfl
+termination_by IteratorLoop.WithWF.mk it init (hwf := wf)
+decreasing_by
+  · exact Or.inl ⟨_, ‹_›, ‹_›⟩
+  · exact Or.inr ⟨‹_›, rfl⟩
+
 theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n]
     [IteratorLoop α m n] [LawfulIteratorLoop α m n]
@@ -108,21 +185,21 @@ theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [It
           fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
       | .done _ => return init) := by
   rw [IterM.forIn'_eq, DefaultConsumers.forIn'_eq_match_step]
-  apply bind_congr
-  intro step
-  cases step.inflate using PlausibleIterStep.casesOn
-  · simp only [map_eq_pure_bind, bind_assoc]
-    apply bind_congr
-    intro forInStep
-    cases forInStep
+  · apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn
+    · simp only [bind_assoc]
+      apply bind_congr
+      intro forInStep
+      cases forInStep
+      · simp
+      · simp only [forIn'_eq, pure_bind]
+        exact DefaultConsumers.forIn'_eq_forIn' (α := α) (m := m) (n := n) _
+          IteratorLoop.wellFounded_of_finite (by simp)
+    · simp only [forIn'_eq]
+      exact DefaultConsumers.forIn'_eq_forIn' (α := α) (m := m) (n := n) _
+          IteratorLoop.wellFounded_of_finite (by simp)
     · simp
-    · simp only [bind_pure_comp, pure_bind, forIn'_eq]
-      apply DefaultConsumers.forIn'_eq_forIn'
-      intros; congr
-  · simp only [forIn'_eq]
-    apply DefaultConsumers.forIn'_eq_forIn'
-    intros; congr
-  · simp
+  · exact IteratorLoop.wellFounded_of_finite
 
 theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n]
diff --git a/src/Init/Data/Iterators/Producers/Monadic/List.lean b/src/Init/Data/Iterators/Producers/Monadic/List.lean
index 9221db28af..bc4491e23f 100644
--- a/src/Init/Data/Iterators/Producers/Monadic/List.lean
+++ b/src/Init/Data/Iterators/Producers/Monadic/List.lean
@@ -72,19 +72,9 @@ instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
     IteratorCollect (ListIterator α) m n :=
   .defaultImplementation
 
-@[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
-    IteratorCollectPartial (ListIterator α) m n :=
-  .defaultImplementation
-
 @[always_inline, inline]
 instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
     IteratorLoop (ListIterator α) m n :=
   .defaultImplementation
 
-@[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
-    IteratorLoopPartial (ListIterator α) m n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
index 5eb6ccb4d0..df07fbf492 100644
--- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean
+++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
@@ -8,8 +8,10 @@ module
 prelude
 public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Access
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 public import Init.Data.Range.Polymorphic.PRange
 public import Init.Data.List.Sublist
+public import Init.WFExtrinsicFix
 
 set_option doc.verso true
 
@@ -121,10 +123,6 @@ instance Iterator.instIteratorCollect [UpwardEnumerable α] [LE α] [DecidableLE
     {n : Type u → Type w} [Monad n] : IteratorCollect (Rxc.Iterator α) Id n :=
   .defaultImplementation
 
-instance Iterator.instIteratorCollectPartial [UpwardEnumerable α] [LE α] [DecidableLE α]
-    {n : Type u → Type w} [Monad n] : IteratorCollectPartial (Rxc.Iterator α) Id n :=
-  .defaultImplementation
-
 theorem Iterator.Monadic.isPlausibleOutput_next {a}
     [UpwardEnumerable α] [LE α] [DecidableLE α]
     {it : IterM (α := Rxc.Iterator α) Id α} (h : it.internalState.next = some a)
@@ -448,161 +446,168 @@ instance Iterator.instIteratorLoop [UpwardEnumerable α] [LE α] [DecidableLE α
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     {n : Type u → Type w} [Monad n] :
     IteratorLoop (Rxc.Iterator α) Id n where
-  forIn _ γ Pl wf it init f :=
+  forIn _ γ Pl it init f :=
     match it with
     | ⟨⟨some next, upperBound⟩⟩ =>
-      if hu : next ≤ upperBound then
-        loop γ Pl wf upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu
-      else
-        return init
+      loop γ Pl (next ≤ ·) (fun a b hab hna => ?hle) upperBound init next ?hle'' (fun a ha₁ ha₂ c => f a ?hf c)
     | ⟨⟨none, _⟩⟩ => return init
   where
-    @[specialize]
-    loop γ Pl wf (upperBound : α) least acc
-        (f : (out : α) → UpwardEnumerable.LE least out → out ≤ upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s)))
-        (next : α) (hl : UpwardEnumerable.LE least next) (hu : next ≤ upperBound) : n γ := do
-      match ← f next hl hu acc with
-      | ⟨.yield acc', _⟩ =>
-        match hs : UpwardEnumerable.succ? next with
-        | some next' =>
-          if hu : next' ≤ upperBound then
-            loop γ Pl wf upperBound least acc' f next' ?hle' hu
+    @[always_inline, inline]
+    loop γ (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop) (hl : ∀ a b : α, a ≤ b → LargeEnough a → LargeEnough b)
+        (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
+        (f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (Pl out c))) : n γ :=
+      haveI : Nonempty γ := ⟨acc⟩
+      WellFounded.extrinsicFix₃ (C₃ := fun _ _ _ => n γ) (InvImage (IteratorLoop.rel _ Id Pl) (fun x => (⟨Rxc.Iterator.mk (some x.1) upperBound⟩, x.2.1)))
+        (fun next acc (h : LargeEnough next) G => do
+          if hu : next ≤ upperBound then
+            match ← f next h hu acc with
+            | ⟨.yield acc', h'⟩ =>
+              match hs : UpwardEnumerable.succ? next with
+              | some next' => G next' acc' (hl _ _ ?hle' h) ?decreasing
+              | none => return acc'
+            | ⟨.done acc', _⟩ => return acc'
           else
-            return acc'
-        | none => return acc'
-      | ⟨.done acc', _⟩ => return acc'
-    termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
-    decreasing_by
-      simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff,
-        Monadic.step, *]
+            return acc) next acc h
   finally
     case hf =>
       rw [Monadic.isPlausibleIndirectOutput_iff]
+      simp only [UpwardEnumerable.le_iff] at ha₁
       obtain ⟨n, hn⟩ := ha₁
       exact ⟨n, hn, ha₂⟩
     case hle =>
-      exact UpwardEnumerable.le_refl _
+      simp only [UpwardEnumerable.le_iff] at hna hab ⊢
+      exact UpwardEnumerable.le_trans hna hab
     case hle' =>
-      refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
-      simp [succMany?_one, hs]
+      simp only [UpwardEnumerable.le_iff]
+      refine ⟨1, ?_⟩
+      simpa [succMany?_one] using hs
+    case hle'' =>
+      exact UpwardEnumerable.le_iff.mpr (UpwardEnumerable.le_refl _)
+    case decreasing =>
+      simp_wf
+      simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
-/--
-An efficient {name}`IteratorLoop` instance:
-As long as the compiler cannot optimize away the {name}`Option` in the internal state, we use a special
-loop implementation.
--/
-partial instance Iterator.instIteratorLoopPartial [UpwardEnumerable α] [LE α] [DecidableLE α]
+private noncomputable def Iterator.instIteratorLoop.loop.wf [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    {n : Type u → Type w} [Monad n] : IteratorLoopPartial (Rxc.Iterator α) Id n where
-  forInPartial _ γ it init f :=
-    match it with
-    | ⟨⟨some next, upperBound⟩⟩ =>
+    {n : Type u → Type w} [Monad n] (γ : Type u)
+    (Pl : α → γ → ForInStep γ → Prop)
+    (wf : IteratorLoop.WellFounded (Rxc.Iterator α) Id Pl)
+    (LargeEnough : α → Prop) (hl : ∀ a b : α, a ≤ b → LargeEnough a → LargeEnough b)
+    (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
+    (f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
+    n γ := do
+  if hu : next ≤ upperBound then
+    match ← f next h hu acc with
+    | ⟨.yield acc', _⟩ =>
+      match hs : UpwardEnumerable.succ? next with
+      | some next' =>
+        loop.wf γ Pl wf LargeEnough hl upperBound acc' next' (hl _ _ ?hle h) f
+      | none => return acc'
+    | ⟨.done acc', _⟩ => return acc'
+  else
+    return acc
+termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
+decreasing_by
+  simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
+where finally
+  case hle =>
+    simp only [UpwardEnumerable.le_iff]
+    refine ⟨1, ?_⟩
+    simpa [succMany?_one] using hs
+
+private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LE α] [DecidableLE α]
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Monad n] [LawfulMonad n]
+    {γ LargeEnough hl upperBound} {next hn} {acc} (Pl wf f) :
+    loop γ Pl LargeEnough hl upperBound acc next hn f =
+      loop.wf (α := α) (n := n) γ Pl wf LargeEnough hl upperBound acc next hn f := by
+  haveI : Nonempty γ := ⟨acc⟩
+  rw [loop, WellFounded.extrinsicFix₃_eq_fix]; rotate_left
+  · exact InvImage.wf _ wf
+  · fun_induction loop.wf γ Pl wf LargeEnough hl upperBound acc  next hn f
+    · rw [WellFounded.fix_eq]
+      simp only [↓reduceDIte, *]
+      apply bind_congr; intro forInStep
+      split
+      · simp only
+        split
+        · simp_all
+        · simp
+      · simp
+    · rw [WellFounded.fix_eq]
+      simp_all
+
+private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LE α] [DecidableLE α]
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
+    {n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
+    {lift} [instLawfulMonadLiftFunction : Std.Internal.LawfulMonadLiftBindFunction (m := Id) (n := n) lift]
+    (Pl : α → γ → ForInStep γ → Prop)
+    (wf : IteratorLoop.WellFounded (Rxc.Iterator α) Id Pl)
+    (LargeEnough : α → Prop) (hl : ∀ a b : α, a ≤ b → LargeEnough a → LargeEnough b)
+    (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
+    (f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
+    loop.wf γ Pl wf LargeEnough hl upperBound acc next h f = (do
       if hu : next ≤ upperBound then
-        loop γ upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu
-      else
-        return init
-    | ⟨⟨none, _⟩⟩ => return init
-  where
-    @[specialize]
-    loop γ (upperBound : α) least acc
-        (f : (out : α) → UpwardEnumerable.LE least out → out ≤ upperBound → (c : γ) → n (ForInStep γ))
-        (next : α) (hl : UpwardEnumerable.LE least next) (hu : next ≤ upperBound) : n γ := do
-      match ← f next hl hu acc with
-      | .yield acc' =>
-        match hs : succ? next with
-        | some next' =>
-          if hu : next' ≤ upperBound then
-            loop γ upperBound least acc' f next' ?hle' hu
-          else
-            return acc'
-        | none => return acc'
-      | .done acc' => return acc'
-  finally
-    case hf =>
-      rw [Monadic.isPlausibleIndirectOutput_iff]
-      obtain ⟨n, hn⟩ := ha₁
-      exact ⟨n, hn, ha₂⟩
-    case hle =>
-      exact UpwardEnumerable.le_refl _
-    case hle' =>
-      refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
-      simp [succMany?_one, hs]
-
-theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α] [LE α] [DecidableLE α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
-    {n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u}
-    {lift} [Internal.LawfulMonadLiftBindFunction lift]
-    {PlausibleForInStep} {upperBound} {next} {hl} {hu} {f} {acc} {wf} :
-    loop (α := α) (n := n) γ PlausibleForInStep wf upperBound least acc f next hl hu =
-      (do
-        match ← f next hl hu acc with
-        | ⟨.yield c, _⟩ =>
+        match ← f next h hu acc with
+        | ⟨.yield acc', _⟩ =>
           letI it' : IterM (α := Rxc.Iterator α) Id α := ⟨⟨succ? next, upperBound⟩⟩
-          IterM.DefaultConsumers.forIn' (m := Id) lift γ
-            PlausibleForInStep wf it' c it'.IsPlausibleIndirectOutput (fun _ => id)
-            (fun b h c => f b
-                (by
-                  refine UpwardEnumerable.le_trans hl ?_
-                  simp only [Monadic.isPlausibleIndirectOutput_iff, it',
-                    ← succMany?_add_one_eq_succ?_bind_succMany?] at h
-                  exact ⟨h.choose + 1, h.choose_spec.1⟩)
-                (by
-                  simp only [Monadic.isPlausibleIndirectOutput_iff, it'] at h
-                  exact h.choose_spec.2) c)
-        | ⟨.done c, _⟩ => return c) := by
-  rw [loop]
-  apply bind_congr
-  intro step
+          IterM.DefaultConsumers.forIn' (m := Id) (n := n) lift γ Pl it' acc'
+            it'.IsPlausibleIndirectOutput (fun _ => id)
+            fun next' h acc' => f next'
+              (by
+                refine hl next next' ?_ ‹_›
+                simp only [it', Monadic.isPlausibleIndirectOutput_iff,
+                  ← succMany?_add_one_eq_succ?_bind_succMany?] at h
+                exact UpwardEnumerable.le_iff.mpr ⟨h.choose + 1, h.choose_spec.1⟩)
+              (by
+                simp only [it', Monadic.isPlausibleIndirectOutput_iff] at h
+                exact h.choose_spec.2)
+              acc'
+        | ⟨.done acc', _⟩ => return acc'
+      else return acc) := by
+  haveI : Nonempty γ := ⟨acc⟩
+  rw [loop.wf]
+  congr 1; ext hu
+  apply bind_congr; intro forInStep
   split
   · split
-    · split
-      · simp only [*]
-        rw [IterM.DefaultConsumers.forIn']
-        simp only [Monadic.step_eq_step, Monadic.step, ↓reduceIte, *,
-          Internal.LawfulMonadLiftBindFunction.liftBind_pure]
-        rw [loop_eq (lift := lift), Shrink.inflate_deflate]
-        apply bind_congr
-        intro step
+    · rw [loopWf_eq (lift := lift) _ Pl wf]
+      rw [IterM.DefaultConsumers.forIn'_eq_match_step (lift := lift) Pl wf]; rotate_left
+      · simp only [Monadic.step_eq_step, Monadic.step,
+          Shrink.inflate_deflate, instLawfulMonadLiftFunction.liftBind_pure, *]
         split
-        · apply IterM.DefaultConsumers.forIn'_eq_forIn'
-          intros; rfl
+        · apply bind_congr; intro forInStep
+          split
+          · apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> (intros; rfl)
+          · simp
         · simp
-      · simp only [*]
-        rw [IterM.DefaultConsumers.forIn']
-        simp [Monadic.step_eq_step, Monadic.step, *,
-          Internal.LawfulMonadLiftBindFunction.liftBind_pure]
-    · simp only [*]
-      rw [IterM.DefaultConsumers.forIn']
-      simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
+    · rw [IterM.DefaultConsumers.forIn'_eq_match_step Pl wf]
+      simp [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure, *]
   · simp
 termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
 decreasing_by
-      simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
+  simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
 instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] :
     LawfulIteratorLoop (Rxc.Iterator α) Id n where
   lawful := by
-    intro lift instLawfulMonadLiftFunction
-    ext γ PlausibleForInStep hwf it init f
-    simp only [IteratorLoop.forIn, IteratorLoop.defaultImplementation]
-    rw [IterM.DefaultConsumers.forIn']
-    simp only [Monadic.step_eq_step, Monadic.step]
-    simp only [Internal.LawfulMonadLiftBindFunction.liftBind_pure]
+    intro lift instLawfulMonadLiftFunction γ it init Pl wf f
+    simp only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
+      IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    rw [IterM.DefaultConsumers.forIn'.wf]
+    split; rotate_left
+    · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
+    rename_i next _
+    rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
+    simp only [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure,
+      Shrink.inflate_deflate]
     split
-    · rename_i it f next upperBound f'
-      simp
+    · apply bind_congr; intro forInStep
       split
       · simp only
-        rw [instIteratorLoop.loop_eq (lift := lift)]
-        apply bind_congr
-        intro step
-        split
-        · apply IterM.DefaultConsumers.forIn'_eq_forIn'
-          intro b c hPb hQb
-          congr
-        · simp
+        rw [← IterM.DefaultConsumers.forIn'_eq_wf Pl wf _]
+        apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> all_goals (intros; rfl)
       · simp
     · simp
 
@@ -698,10 +703,6 @@ instance Iterator.instIteratorCollect [UpwardEnumerable α] [LT α] [DecidableLT
     {n : Type u → Type w} [Monad n] : IteratorCollect (Rxo.Iterator α) Id n :=
   .defaultImplementation
 
-instance Iterator.instIteratorCollectPartial [UpwardEnumerable α] [LT α] [DecidableLT α]
-    {n : Type u → Type w} [Monad n] : IteratorCollectPartial (Rxo.Iterator α) Id n :=
-  .defaultImplementation
-
 theorem Iterator.Monadic.isPlausibleOutput_next {a}
     [UpwardEnumerable α] [LT α] [DecidableLT α]
     {it : IterM (α := Rxo.Iterator α) Id α} (h : it.internalState.next = some a)
@@ -1025,161 +1026,164 @@ instance Iterator.instIteratorLoop [UpwardEnumerable α] [LT α] [DecidableLT α
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     {n : Type u → Type w} [Monad n] :
     IteratorLoop (Rxo.Iterator α) Id n where
-  forIn _ γ Pl wf it init f :=
+  forIn _ γ Pl it init f :=
     match it with
     | ⟨⟨some next, upperBound⟩⟩ =>
-      if hu : next < upperBound then
-        loop γ Pl wf upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu
-      else
-        return init
+      loop γ Pl (UpwardEnumerable.LE next ·) (fun a b hab hna => ?hle) upperBound init next ?hle'' (fun a ha₁ ha₂ c => f a ?hf c)
     | ⟨⟨none, _⟩⟩ => return init
   where
-    @[specialize]
-    loop γ Pl wf (upperBound : α) least acc
-        (f : (out : α) → UpwardEnumerable.LE least out → out < upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s)))
-        (next : α) (hl : UpwardEnumerable.LE least next) (hu : next < upperBound) : n γ := do
-      match ← f next hl hu acc with
-      | ⟨.yield acc', _⟩ =>
-        match hs : UpwardEnumerable.succ? next with
-        | some next' =>
-          if hu : next' < upperBound then
-            loop γ Pl wf upperBound least acc' f next' ?hle' hu
+    @[always_inline, inline]
+    loop γ (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop)
+        (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
+        (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
+        (f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (Pl out c))) : n γ :=
+      haveI : Nonempty γ := ⟨acc⟩
+      WellFounded.extrinsicFix₃ (C₃ := fun _ _ _ => n γ) (InvImage (IteratorLoop.rel _ Id Pl) (fun x => (⟨Rxo.Iterator.mk (some x.1) upperBound⟩, x.2.1)))
+        (fun next acc (h : LargeEnough next) G => do
+          if hu : next < upperBound then
+            match ← f next h hu acc with
+            | ⟨.yield acc', h'⟩ =>
+              match hs : UpwardEnumerable.succ? next with
+              | some next' => G next' acc' (hl _ _ ?hle' h) ?decreasing
+              | none => return acc'
+            | ⟨.done acc', _⟩ => return acc'
           else
-            return acc'
-        | none => return acc'
-      | ⟨.done acc', _⟩ => return acc'
-    termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
-    decreasing_by
-      simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff,
-        Monadic.step, *]
+            return acc) next acc h
   finally
     case hf =>
       rw [Monadic.isPlausibleIndirectOutput_iff]
       obtain ⟨n, hn⟩ := ha₁
       exact ⟨n, hn, ha₂⟩
     case hle =>
-      exact UpwardEnumerable.le_refl _
+      exact UpwardEnumerable.le_trans hna hab
     case hle' =>
-      refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
-      simp [succMany?_one, hs]
+      refine ⟨1, ?_⟩
+      simpa [succMany?_one] using hs
+    case hle'' =>
+      exact UpwardEnumerable.le_refl _
+    case decreasing =>
+      simp_wf; simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
-/--
-An efficient {name}`IteratorLoopPartial` instance:
-As long as the compiler cannot optimize away the {name}`Option` in the internal state, we use a special
-loop implementation.
--/
-partial instance Iterator.instIteratorLoopPartial [UpwardEnumerable α] [LT α] [DecidableLT α]
+private noncomputable def Iterator.instIteratorLoop.loop.wf [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    {n : Type u → Type w} [Monad n] : IteratorLoopPartial (Rxo.Iterator α) Id n where
-  forInPartial _ γ it init f :=
-    match it with
-    | ⟨⟨some next, upperBound⟩⟩ =>
+    {n : Type u → Type w} [Monad n] (γ : Type u)
+    (Pl : α → γ → ForInStep γ → Prop)
+    (wf : IteratorLoop.WellFounded (Rxo.Iterator α) Id Pl)
+    (LargeEnough : α → Prop) (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
+    (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
+    (f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
+    n γ := do
+  if hu : next < upperBound then
+    match ← f next h hu acc with
+    | ⟨.yield acc', _⟩ =>
+      match hs : UpwardEnumerable.succ? next with
+      | some next' =>
+        loop.wf γ Pl wf LargeEnough hl upperBound acc' next' (hl _ _ ?hle h) f
+      | none => return acc'
+    | ⟨.done acc', _⟩ => return acc'
+  else
+    return acc
+termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
+decreasing_by
+  simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
+where finally
+  case hle =>
+    refine ⟨1, ?_⟩
+    simpa [succMany?_one] using hs
+
+private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LT α] [DecidableLT α]
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Monad n] [LawfulMonad n]
+    {γ LargeEnough hl upperBound} {next hn} {acc} (Pl wf f) :
+    loop γ Pl LargeEnough hl upperBound acc next hn f =
+      loop.wf (α := α) (n := n) γ Pl wf LargeEnough hl upperBound acc next hn f := by
+  haveI : Nonempty γ := ⟨acc⟩
+  rw [loop, WellFounded.extrinsicFix₃_eq_fix]; rotate_left
+  · exact InvImage.wf _ wf
+  · fun_induction loop.wf γ Pl wf LargeEnough hl upperBound acc  next hn f
+    · rw [WellFounded.fix_eq]
+      simp only [↓reduceDIte, *]
+      apply bind_congr; intro forInStep
+      split
+      · simp only
+        split
+        · simp_all
+        · simp
+      · simp
+    · rw [WellFounded.fix_eq]
+      simp_all
+
+private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LT α] [DecidableLT α]
+    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
+    {n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
+    {lift} [instLawfulMonadLiftFunction : Std.Internal.LawfulMonadLiftBindFunction (m := Id) (n := n) lift]
+    (Pl : α → γ → ForInStep γ → Prop)
+    (wf : IteratorLoop.WellFounded (Rxo.Iterator α) Id Pl)
+    (LargeEnough : α → Prop) (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
+    (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
+    (f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
+    loop.wf γ Pl wf LargeEnough hl upperBound acc next h f = (do
       if hu : next < upperBound then
-        loop γ upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu
-      else
-        return init
-    | ⟨⟨none, _⟩⟩ => return init
-  where
-    @[specialize]
-    loop γ (upperBound : α) least acc
-        (f : (out : α) → UpwardEnumerable.LE least out → out < upperBound → (c : γ) → n (ForInStep γ))
-        (next : α) (hl : UpwardEnumerable.LE least next) (hu : next < upperBound) : n γ := do
-      match ← f next hl hu acc with
-      | .yield acc' =>
-        match hs : succ? next with
-        | some next' =>
-          if hu : next' < upperBound then
-            loop γ upperBound least acc' f next' ?hle' hu
-          else
-            return acc'
-        | none => return acc'
-      | .done acc' => return acc'
-  finally
-    case hf =>
-      rw [Monadic.isPlausibleIndirectOutput_iff]
-      obtain ⟨n, hn⟩ := ha₁
-      exact ⟨n, hn, ha₂⟩
-    case hle =>
-      exact UpwardEnumerable.le_refl _
-    case hle' =>
-      refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
-      simp [succMany?_one, hs]
-
-theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α] [LT α] [DecidableLT α]
-    [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
-    {n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u}
-    {lift} [Internal.LawfulMonadLiftBindFunction lift]
-    {PlausibleForInStep} {upperBound} {next} {hl} {hu} {f} {acc} {wf} :
-    loop (α := α) (n := n) γ PlausibleForInStep wf upperBound least acc f next hl hu =
-      (do
-        match ← f next hl hu acc with
-        | ⟨.yield c, _⟩ =>
+        match ← f next h hu acc with
+        | ⟨.yield acc', _⟩ =>
           letI it' : IterM (α := Rxo.Iterator α) Id α := ⟨⟨succ? next, upperBound⟩⟩
-          IterM.DefaultConsumers.forIn' (m := Id) lift γ
-            PlausibleForInStep wf it' c it'.IsPlausibleIndirectOutput (fun _ => id)
-            (fun b h c => f b
-                (by
-                  refine UpwardEnumerable.le_trans hl ?_
-                  simp only [Monadic.isPlausibleIndirectOutput_iff, it',
-                    ← succMany?_add_one_eq_succ?_bind_succMany?] at h
-                  exact ⟨h.choose + 1, h.choose_spec.1⟩)
-                (by
-                  simp only [Monadic.isPlausibleIndirectOutput_iff, it'] at h
-                  exact h.choose_spec.2) c)
-        | ⟨.done c, _⟩ => return c) := by
-  rw [loop]
-  apply bind_congr
-  intro step
+          IterM.DefaultConsumers.forIn' (m := Id) (n := n) lift γ Pl it' acc'
+            it'.IsPlausibleIndirectOutput (fun _ => id)
+            fun next' h acc' => f next'
+              (by
+                refine hl next next' ?_ ‹_›
+                simp only [it', Monadic.isPlausibleIndirectOutput_iff,
+                  ← succMany?_add_one_eq_succ?_bind_succMany?] at h
+                exact ⟨h.choose + 1, h.choose_spec.1⟩)
+              (by
+                simp only [it', Monadic.isPlausibleIndirectOutput_iff] at h
+                exact h.choose_spec.2)
+              acc'
+        | ⟨.done acc', _⟩ => return acc'
+      else return acc) := by
+  haveI : Nonempty γ := ⟨acc⟩
+  rw [loop.wf]
+  congr 1; ext hu
+  apply bind_congr; intro forInStep
   split
   · split
-    · split
-      · simp only [*]
-        rw [IterM.DefaultConsumers.forIn']
-        simp only [Monadic.step_eq_step, Monadic.step, ↓reduceIte, *,
-          Internal.LawfulMonadLiftBindFunction.liftBind_pure]
-        rw [loop_eq (lift := lift), Shrink.inflate_deflate]
-        apply bind_congr
-        intro step
+    · rw [loopWf_eq (lift := lift) _ Pl wf]
+      rw [IterM.DefaultConsumers.forIn'_eq_match_step (lift := lift) Pl wf]; rotate_left
+      · simp only [Monadic.step_eq_step, Monadic.step,
+          Shrink.inflate_deflate, instLawfulMonadLiftFunction.liftBind_pure, *]
         split
-        · apply IterM.DefaultConsumers.forIn'_eq_forIn'
-          intros; rfl
+        · apply bind_congr; intro forInStep
+          split
+          · apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> (intros; rfl)
+          · simp
         · simp
-      · simp only [*]
-        rw [IterM.DefaultConsumers.forIn']
-        simp [Monadic.step_eq_step, Monadic.step, *,
-          Internal.LawfulMonadLiftBindFunction.liftBind_pure]
-    · simp only [*]
-      rw [IterM.DefaultConsumers.forIn']
-      simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
+    · rw [IterM.DefaultConsumers.forIn'_eq_match_step Pl wf]
+      simp [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure, *]
   · simp
 termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
 decreasing_by
-      simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
+  simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
 instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] :
     LawfulIteratorLoop (Rxo.Iterator α) Id n where
   lawful := by
-    intro lift instLawfulMonadLiftFunction
-    ext γ PlausibleForInStep hwf it init f
-    simp only [IteratorLoop.forIn, IteratorLoop.defaultImplementation]
-    rw [IterM.DefaultConsumers.forIn']
-    simp only [Monadic.step_eq_step, Monadic.step]
-    simp only [Internal.LawfulMonadLiftBindFunction.liftBind_pure]
+    intro lift instLawfulMonadLiftFunction γ it init Pl wf f
+    simp only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
+      IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    rw [IterM.DefaultConsumers.forIn'.wf]
+    split; rotate_left
+    · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
+    rename_i next _
+    rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
+    simp only [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure,
+      Shrink.inflate_deflate]
     split
-    · rename_i it f next upperBound f'
-      simp
+    · apply bind_congr; intro forInStep
       split
       · simp only
-        rw [instIteratorLoop.loop_eq (lift := lift)]
-        apply bind_congr
-        intro step
-        split
-        · apply IterM.DefaultConsumers.forIn'_eq_forIn'
-          intro b c hPb hQb
-          congr
-        · simp
+        rw [← IterM.DefaultConsumers.forIn'_eq_wf Pl wf _]
+        apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> all_goals (intros; rfl)
       · simp
     · simp
 
@@ -1265,10 +1269,6 @@ instance Iterator.instIteratorCollect [UpwardEnumerable α]
     {n : Type u → Type w} [Monad n] : IteratorCollect (Rxi.Iterator α) Id n :=
   .defaultImplementation
 
-instance Iterator.instIteratorCollectPartial [UpwardEnumerable α]
-    {n : Type u → Type w} [Monad n] : IteratorCollectPartial (Rxi.Iterator α) Id n :=
-  .defaultImplementation
-
 theorem Iterator.Monadic.isPlausibleOutput_next {a} [UpwardEnumerable α]
     {it : IterM (α := Rxi.Iterator α) Id α} (h : it.internalState.next = some a) :
     it.IsPlausibleOutput a := by
@@ -1508,148 +1508,151 @@ section IteratorLoop
 
 /--
 An efficient {name}`IteratorLoop` instance:
-As long as the compiler cannot optimize away the {name}`Option` in the internal state, we use a
-special loop implementation.
+As long as the compiler cannot optimize away the {name}`Option` in the internal state, we use a special
+loop implementation.
 -/
 @[always_inline, inline]
-instance Iterator.instIteratorLoop [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α]
+instance Iterator.instIteratorLoop [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     {n : Type u → Type w} [Monad n] :
     IteratorLoop (Rxi.Iterator α) Id n where
-  forIn _ γ Pl wf it init f :=
+  forIn _ γ Pl it init f :=
     match it with
     | ⟨⟨some next⟩⟩ =>
-        loop γ Pl wf next init (fun a ha c => f a ?hf c) next ?hle
+      loop γ Pl (UpwardEnumerable.LE next ·) (fun a b hab hna => ?hle) init next ?hle'' (fun a ha c => f a ?hf c)
     | ⟨⟨none⟩⟩ => return init
   where
-    @[specialize]
-    loop γ Pl wf least acc
-        (f : (out : α) → UpwardEnumerable.LE least out → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s)))
-        (next : α) (hl : UpwardEnumerable.LE least next) : n γ := do
-      match ← f next hl acc with
-      | ⟨.yield acc', _⟩ =>
-        match hs : UpwardEnumerable.succ? next with
-        | some next' =>
-            loop γ Pl wf least acc' f next' ?hle'
-        | none => return acc'
-      | ⟨.done acc', _⟩ => return acc'
-    termination_by IteratorLoop.WithWF.mk ⟨⟨some next⟩⟩ acc (hwf := wf)
-    decreasing_by
-      simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff,
-        Monadic.step, *]
+    @[always_inline, inline]
+    loop γ (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop) (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
+        (acc : γ) (next : α) (h : LargeEnough next)
+        (f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (Pl out c))) : n γ :=
+      haveI : Nonempty γ := ⟨acc⟩
+      WellFounded.extrinsicFix₃ (C₃ := fun _ _ _ => n γ) (InvImage (IteratorLoop.rel _ Id Pl) (fun x => (⟨Rxi.Iterator.mk (some x.1)⟩, x.2.1)))
+        (fun next acc (h : LargeEnough next) G => do
+          match ← f next h acc with
+          | ⟨.yield acc', h'⟩ =>
+            match hs : UpwardEnumerable.succ? next with
+            | some next' => G next' acc' (hl _ _ ?hle' h) ?decreasing
+            | none => return acc'
+          | ⟨.done acc', _⟩ => return acc') next acc h
   finally
     case hf =>
       rw [Monadic.isPlausibleIndirectOutput_iff]
       exact ha
     case hle =>
-      exact UpwardEnumerable.le_refl _
+      exact UpwardEnumerable.le_trans hna hab
     case hle' =>
-      refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
-      simp [succMany?_one, hs]
-
-/--
-An efficient {name}`IteratorLoopPartial` instance:
-As long as the compiler cannot optimize away the {name}`Option` in the internal state, we use a
-special loop implementation.
--/
-partial instance Iterator.instIteratorLoopPartial [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α]
-    {n : Type u → Type w} [Monad n] : IteratorLoopPartial (Rxi.Iterator α) Id n where
-  forInPartial _ γ it init f :=
-    match it with
-    | ⟨⟨some next⟩⟩ => loop γ next init (fun a ha c => f a ?hf c) next ?hle
-    | ⟨⟨none⟩⟩ => return init
-  where
-    @[specialize]
-    loop γ least acc
-        (f : (out : α) → UpwardEnumerable.LE least out → (c : γ) → n (ForInStep γ))
-        (next : α) (hl : UpwardEnumerable.LE least next) : n γ := do
-      match ← f next hl acc with
-      | .yield acc' =>
-        match hs : succ? next with
-        | some next' =>
-            loop γ least acc' f next' ?hle'
-        | none => return acc'
-      | .done acc' => return acc'
-  finally
-    case hf =>
-      rw [Monadic.isPlausibleIndirectOutput_iff]
-      exact ha
-    case hle =>
+      refine ⟨1, ?_⟩
+      simpa [succMany?_one] using hs
+    case hle'' =>
       exact UpwardEnumerable.le_refl _
-    case hle' =>
-      refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
-      simp [succMany?_one, hs]
+    case decreasing =>
+      simp_wf; simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
-theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α]
+private noncomputable def Iterator.instIteratorLoop.loop.wf [UpwardEnumerable α]
     [LawfulUpwardEnumerable α]
-    {n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u}
-    {lift} [Internal.LawfulMonadLiftBindFunction lift]
-    {PlausibleForInStep next hl f acc wf} :
-    loop (α := α) (n := n) γ PlausibleForInStep wf least acc f next hl =
-      (do
-        match ← f next hl acc with
-        | ⟨.yield c, _⟩ =>
+    {n : Type u → Type w} [Monad n] (γ : Type u)
+    (Pl : α → γ → ForInStep γ → Prop)
+    (wf : IteratorLoop.WellFounded (Rxi.Iterator α) Id Pl)
+    (LargeEnough : α → Prop) (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
+    (acc : γ) (next : α) (h : LargeEnough next)
+    (f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
+    n γ := do
+    match ← f next h acc with
+    | ⟨.yield acc', _⟩ =>
+      match hs : UpwardEnumerable.succ? next with
+      | some next' =>
+        loop.wf γ Pl wf LargeEnough hl acc' next' (hl _ _ ?hle h) f
+      | none => return acc'
+    | ⟨.done acc', _⟩ => return acc'
+termination_by IteratorLoop.WithWF.mk ⟨⟨some next⟩⟩ acc (hwf := wf)
+decreasing_by
+  simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
+where finally
+  case hle =>
+    refine ⟨1, ?_⟩
+    simpa [succMany?_one] using hs
+
+private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α]
+    [LawfulUpwardEnumerable α] [Monad n] [LawfulMonad n]
+    {γ LargeEnough hl} {next hn} {acc} (Pl wf f) :
+    loop γ Pl LargeEnough hl acc next hn f =
+      loop.wf (α := α) (n := n) γ Pl wf LargeEnough hl acc next hn f := by
+  haveI : Nonempty γ := ⟨acc⟩
+  rw [loop, WellFounded.extrinsicFix₃_eq_fix]; rotate_left
+  · exact InvImage.wf _ wf
+  · fun_induction loop.wf γ Pl wf LargeEnough hl acc  next hn f
+    · rw [WellFounded.fix_eq]
+      apply bind_congr; intro forInStep
+      split
+      · simp only
+        split
+        · simp_all
+        · simp
+      · simp
+
+private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α]
+    [LawfulUpwardEnumerable α]
+    {n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
+    {lift} [instLawfulMonadLiftFunction : Std.Internal.LawfulMonadLiftBindFunction (m := Id) (n := n) lift]
+    (Pl : α → γ → ForInStep γ → Prop)
+    (wf : IteratorLoop.WellFounded (Rxi.Iterator α) Id Pl)
+    (LargeEnough : α → Prop) (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
+    (acc : γ) (next : α) (h : LargeEnough next)
+    (f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
+    loop.wf γ Pl wf LargeEnough hl acc next h f = (do
+        match ← f next h acc with
+        | ⟨.yield acc', _⟩ =>
           letI it' : IterM (α := Rxi.Iterator α) Id α := ⟨⟨succ? next⟩⟩
-          IterM.DefaultConsumers.forIn' (m := Id) lift γ
-            PlausibleForInStep wf it' c it'.IsPlausibleIndirectOutput (fun _ => id)
-            (fun b h c => f b
-                (by
-                  refine UpwardEnumerable.le_trans hl ?_
-                  simp only [Monadic.isPlausibleIndirectOutput_iff, it',
-                    ← succMany?_add_one_eq_succ?_bind_succMany?] at h
-                  exact ⟨h.choose + 1, h.choose_spec⟩)
-                c)
-        | ⟨.done c, _⟩ => return c) := by
-  rw [loop]
-  apply bind_congr
-  intro step
+          IterM.DefaultConsumers.forIn' (m := Id) (n := n) lift γ Pl it' acc'
+            it'.IsPlausibleIndirectOutput (fun _ => id)
+            fun next' h acc' => f next'
+              (by
+                refine hl next next' ?_ ‹_›
+                simp only [it', Monadic.isPlausibleIndirectOutput_iff,
+                  ← succMany?_add_one_eq_succ?_bind_succMany?] at h
+                exact ⟨h.choose + 1, h.choose_spec⟩)
+              acc'
+        | ⟨.done acc', _⟩ => return acc') := by
+  haveI : Nonempty γ := ⟨acc⟩
+  rw [loop.wf]
+  apply bind_congr; intro forInStep
   split
   · split
-    · split
-      · rename_i heq
-        cases heq
-        simp only [*]
-        rw [IterM.DefaultConsumers.forIn']
-        simp only [Monadic.step_eq_step, Monadic.step, *,
-          Internal.LawfulMonadLiftBindFunction.liftBind_pure]
-        rw [loop_eq (lift := lift), Shrink.inflate_deflate]
-        apply bind_congr
-        intro step
+    · rw [loopWf_eq (lift := lift) _ Pl wf]
+      rw [IterM.DefaultConsumers.forIn'_eq_match_step (lift := lift) Pl wf]; rotate_left
+      · simp only [Monadic.step_eq_step, Monadic.step,
+          Shrink.inflate_deflate, instLawfulMonadLiftFunction.liftBind_pure, *]
+        apply bind_congr; intro forInStep
         split
-        · apply IterM.DefaultConsumers.forIn'_eq_forIn'
-          intros; rfl
+        · apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> (intros; rfl)
         · simp
-      · rename_i heq
-        cases heq
-    · simp only [*]
-      rw [IterM.DefaultConsumers.forIn']
-      simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
+    · rw [IterM.DefaultConsumers.forIn'_eq_match_step Pl wf]
+      simp [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure, *]
   · simp
 termination_by IteratorLoop.WithWF.mk ⟨⟨some next⟩⟩ acc (hwf := wf)
 decreasing_by
-      simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
+  simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
 instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α]
-    [LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] [LawfulMonad n] :
+    [LawfulUpwardEnumerable α]
+    {n : Type u → Type w} [Monad n] [LawfulMonad n] :
     LawfulIteratorLoop (Rxi.Iterator α) Id n where
   lawful := by
-    intro lift instLawfulMonadLiftFunction
-    ext γ PlausibleForInStep hwf it init f
-    simp only [IteratorLoop.forIn, IteratorLoop.defaultImplementation]
-    rw [IterM.DefaultConsumers.forIn']
-    simp only [Monadic.step_eq_step, Monadic.step]
-    simp only [Internal.LawfulMonadLiftBindFunction.liftBind_pure]
+    intro lift instLawfulMonadLiftFunction γ it init Pl wf f
+    simp only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
+      IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    rw [IterM.DefaultConsumers.forIn'.wf]
+    split; rotate_left
+    · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
+    rename_i next _
+    rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
+    simp only [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure,
+      Shrink.inflate_deflate]
+    apply bind_congr; intro forInStep
     split
-    · rename_i it f next upperBound f'
-      rw [instIteratorLoop.loop_eq (lift := lift), Shrink.inflate_deflate]
-      apply bind_congr
-      intro step
-      split
-      · apply IterM.DefaultConsumers.forIn'_eq_forIn'
-        intro b c hPb hQb
-        congr
-      · simp
+    · simp only
+      rw [← IterM.DefaultConsumers.forIn'_eq_wf Pl wf _]
+      apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> all_goals (intros; rfl)
     · simp
 
 end IteratorLoop
diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean
index e742d7d67c..d71ed68217 100644
--- a/src/Init/Data/Slice/Array/Iterator.lean
+++ b/src/Init/Data/Slice/Array/Iterator.lean
@@ -60,9 +60,7 @@ instance SubarrayIterator.instFinite : Finite (SubarrayIterator α) Id :=
   .of_finitenessRelation instFinitelessRelation
 
 instance [Monad m] : IteratorCollect (SubarrayIterator α) Id m := .defaultImplementation
-instance [Monad m] : IteratorCollectPartial (SubarrayIterator α) Id m := .defaultImplementation
 instance [Monad m] : IteratorLoop (SubarrayIterator α) Id m := .defaultImplementation
-instance [Monad m] : IteratorLoopPartial (SubarrayIterator α) Id m := .defaultImplementation
 
 @[inline, expose]
 def Subarray.instToIterator :=
diff --git a/src/Init/Data/String/Lemmas/Search.lean b/src/Init/Data/String/Lemmas/Search.lean
index 47afce552e..262f28ccc1 100644
--- a/src/Init/Data/String/Lemmas/Search.lean
+++ b/src/Init/Data/String/Lemmas/Search.lean
@@ -16,7 +16,6 @@ open String.Slice Pattern
 
 variable {ρ : Type} {σ : Slice → Type}
 variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
-variable [∀ s, Std.Iterators.Finite (σ s) Id]
 variable [∀ s, Std.Iterators.IteratorLoop (σ s) Id Id]
 
 @[simp]
diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean
index e3a5f80870..e206284b6b 100644
--- a/src/Init/Data/String/Slice.lean
+++ b/src/Init/Data/String/Slice.lean
@@ -188,15 +188,9 @@ instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitIterator
 instance [Monad n] : Std.Iterators.IteratorCollect (SplitIterator pat s) Id n :=
   .defaultImplementation
 
-instance [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator pat s) Id n :=
-  .defaultImplementation
-
 instance [Monad n] : Std.Iterators.IteratorLoop (SplitIterator pat s) Id n :=
   .defaultImplementation
 
-instance [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator pat s) Id n :=
-  .defaultImplementation
-
 end SplitIterator
 
 /--
@@ -290,18 +284,10 @@ instance [Monad n] {s} :
     Std.Iterators.IteratorCollect (SplitInclusiveIterator pat s) Id n :=
   .defaultImplementation
 
-instance [Monad n] {s} :
-    Std.Iterators.IteratorCollectPartial (SplitInclusiveIterator pat s) Id n :=
-  .defaultImplementation
-
 instance [Monad n] {s} :
     Std.Iterators.IteratorLoop (SplitInclusiveIterator pat s) Id n :=
   .defaultImplementation
 
-instance [Monad n] {s} :
-    Std.Iterators.IteratorLoopPartial (SplitInclusiveIterator pat s) Id n :=
-  .defaultImplementation
-
 end SplitInclusiveIterator
 
 /--
@@ -640,16 +626,9 @@ instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (RevSplitIterat
 instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] :
-    Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ s) m n :=
-  .defaultImplementation
-
 instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ s) m n :=
-  .defaultImplementation
-
 end RevSplitIterator
 
 /--
@@ -921,15 +900,9 @@ instance [Pure m] : Std.Iterators.Finite (PosIterator s) m :=
 instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (PosIterator s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial (PosIterator s) m n :=
-  .defaultImplementation
-
 instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (PosIterator s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (PosIterator s) m n :=
-  .defaultImplementation
-
 docs_to_verso positions
 
 end PosIterator
@@ -1011,16 +984,9 @@ instance [Pure m] : Std.Iterators.Finite (RevPosIterator s) m :=
 instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevPosIterator s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] :
-    Std.Iterators.IteratorCollectPartial (RevPosIterator s) m n :=
-  .defaultImplementation
-
 instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevPosIterator s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevPosIterator s) m n :=
-  .defaultImplementation
-
 docs_to_verso revPositions
 
 end RevPosIterator
@@ -1098,15 +1064,9 @@ instance [Pure m] : Std.Iterators.Finite ByteIterator m :=
 instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect ByteIterator m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial ByteIterator m n :=
-  .defaultImplementation
-
 instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop ByteIterator m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial ByteIterator m n :=
-  .defaultImplementation
-
 docs_to_verso bytes
 
 end ByteIterator
@@ -1185,15 +1145,9 @@ instance [Pure m] : Std.Iterators.Finite RevByteIterator m :=
 instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect RevByteIterator m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial RevByteIterator m n :=
-  .defaultImplementation
-
 instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop RevByteIterator m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial RevByteIterator m n :=
-  .defaultImplementation
-
 docs_to_verso revBytes
 
 end RevByteIterator
diff --git a/src/Init/WFExtrinsicFix.lean b/src/Init/WFExtrinsicFix.lean
new file mode 100644
index 0000000000..d74948612d
--- /dev/null
+++ b/src/Init/WFExtrinsicFix.lean
@@ -0,0 +1,245 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.WF
+import Init.Classical
+import Init.Ext
+import Init.NotationExtra
+
+set_option doc.verso true
+set_option linter.missingDocs true
+
+/-!
+This module provides a fixpoint combinator that combines advantages of `partial` and well-founded
+recursion.
+
+The combinator is similar to {lean}`WellFounded.fix`, but does
+not require a well-foundedness proof. Therefore, it can be used in situations in which
+a proof of termination is impossible or inconvenient. Given a well-foundedness proof, there is a
+theorem guaranteeing that it is equal to {lean}`WellFounded.fix`.
+-/
+
+variable {α : Sort _} {β : α → Sort _} {γ : (a : α) → β a → Sort _}
+  {C : α → Sort _} {C₂ : (a : α) → β a → Sort _} {C₃ : (a : α) → (b : β a) → γ a b → Sort _}
+
+set_option doc.verso true
+
+namespace WellFounded
+
+/--
+The function implemented as the loop {lean}`opaqueFix R F a = F a (fun a _ => opaqueFix R F a)`.
+{lean}`opaqueFix R F` is the fixpoint of the functional {name}`F`, as long as the loop is
+well-founded.
+
+The loop might run forever depending on {name}`F`. It is opaque, i.e., it is impossible to prove
+nontrivial properties about it.
+-/
+@[specialize]
+partial def opaqueFix [∀ a, Nonempty (C a)] (R : α → α → Prop)
+    (F : ∀ a, (∀ a', R a' a → C a') → C a) (a : α) : C a :=
+  F a (fun a _ => opaqueFix R F a)
+
+/-
+SAFE assuming that the code generated by iteration over `F` is equivalent to the well-founded
+fixpoint of `F` if `R` is well-founded.
+-/
+/--
+A fixpoint combinator that can be used to construct recursive functions with an *extrinsic* proof
+of termination.
+
+Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
+to {name}`R`, {lean}`extrinsicFix R F` is the recursive function obtained by having {name}`F` call
+itself recursively.
+
+If {name}`R` is not well-founded, {lean}`extrinsicFix R F` might run forever. In this case,
+nothing interesting can be proved about the recursive function; it is opaque.
+
+If {name}`R` _is_ well-founded, {lean}`extrinsicFix R F` is equivalent to
+{lean}`WellFounded.fix _ F`, logically and regarding its termination behavior.
+-/
+@[implemented_by opaqueFix]
+public def extrinsicFix [∀ a, Nonempty (C a)] (R : α → α → Prop)
+    (F : ∀ a, (∀ a', R a' a → C a') → C a) (a : α) : C a :=
+  open scoped Classical in
+  if h : WellFounded R then
+    h.fix F a
+  else
+    -- Return `opaqueFix R F a` so that `implemented_by opaqueFix` is sound.
+    -- In effect, `extrinsicFix` is opaque if `WellFounded R` is false.
+    opaqueFix R F a
+
+public theorem extrinsicFix_eq_fix [∀ a, Nonempty (C a)] {R : α → α → Prop}
+    {F : ∀ a, (∀ a', R a' a → C a') → C a}
+    (wf : WellFounded R) {a : α} :
+    extrinsicFix R F a = wf.fix F a := by
+  simp only [extrinsicFix, dif_pos wf]
+
+public theorem extrinsicFix_eq_apply [∀ a, Nonempty (C a)] {R : α → α → Prop}
+    {F : ∀ a, (∀ a', R a' a → C a') → C a} (h : WellFounded R) {a : α} :
+    extrinsicFix R F a = F a (fun a _ => extrinsicFix R F a) := by
+  simp only [extrinsicFix, dif_pos h]
+  rw [WellFounded.fix_eq]
+
+/--
+A fixpoint combinator that allows for deferred proofs of termination.
+
+{lean}`extrinsicFix R F` is function implemented as the loop
+{lean}`extrinsicFix R F a = F a (fun a _ => extrinsicFix R F a)`.
+
+If the loop can be shown to be well-founded, {name}`extrinsicFix_eq_apply` proves that it satisfies the
+fixpoint equation. Otherwise, {lean}`extrinsicFix R F` is opaque, i.e., it is impossible to prove
+nontrivial properties about it.
+-/
+add_decl_doc extrinsicFix
+
+/--
+The function implemented as the loop
+{lean}`opaqueFix₂ R F a b = F a b (fun a' b' _ => opaqueFix₂ R F a' b')`.
+{lean}`opaqueFix₂ R F` is the fixpoint of the functional {name}`F`, as long as the loop is
+well-founded.
+
+The loop might run forever depending on {name}`F`. It is opaque, i.e., it is impossible to prove
+nontrivial properties about it.
+-/
+@[specialize]
+partial def opaqueFix₂ [∀ a b, Nonempty (C₂ a b)]
+    (R : (a : α) ×' β a → (a : α) ×' β a → Prop)
+    (F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b)
+    (a : α) (b : β a) :
+    C₂ a b :=
+  F a b (fun a' b' _ => opaqueFix₂ R F a' b')
+
+/-
+SAFE assuming that the code generated by iteration over `F` is equivalent to the well-founded
+fixpoint of `F` if `R` is well-founded.
+-/
+/--
+A fixpoint combinator that can be used to construct recursive functions of arity two with an
+*extrinsic* proof of termination.
+
+Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
+to {name}`R`, {lean}`extrinsicFix₂ R F` is the recursive function obtained by having {name}`F` call
+itself recursively.
+
+If {name}`R` is not well-founded, {lean}`extrinsicFix₂ R F` might run forever. In this case,
+nothing interesting can be proved about the recursive function; it is opaque.
+
+If {name}`R` _is_ well-founded, {lean}`extrinsicFix₂ R F` is equivalent to a well-founded recursive
+function, logically and regarding its termination behavior.
+-/
+@[implemented_by opaqueFix₂]
+public def extrinsicFix₂ [∀ a b, Nonempty (C₂ a b)]
+    (R : (a : α) ×' β a → (a : α) ×' β a → Prop)
+    (F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b)
+    (a : α) (b : β a) :
+    C₂ a b :=
+  let F' (x : PSigma β) (G : (y : PSigma β) → R y x → C₂ y.1 y.2) : C₂ x.1 x.2 :=
+    F x.1 x.2 (fun a b => G ⟨a, b⟩)
+  extrinsicFix (C := fun x : PSigma β => C₂ x.1 x.2) R F' ⟨a, b⟩
+
+public theorem extrinsicFix₂_eq_fix [∀ a b, Nonempty (C₂ a b)]
+    {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
+    {F : ∀ a b, (∀ a' b', R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b}
+    (wf : WellFounded R) {a b} :
+    extrinsicFix₂ R F a b = wf.fix (fun x G => F x.1 x.2 (fun a b h => G ⟨a, b⟩ h)) ⟨a, b⟩ := by
+  rw [extrinsicFix₂, extrinsicFix_eq_fix wf]
+
+public theorem extrinsicFix₂_eq_apply [∀ a b, Nonempty (C₂ a b)]
+    {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
+    {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b}
+    (wf : WellFounded R) {a : α} {b : β a} :
+    extrinsicFix₂ R F a b = F a b (fun a' b' _ => extrinsicFix₂ R F a' b') := by
+  rw [extrinsicFix₂, extrinsicFix_eq_apply wf]
+  rfl
+
+/--
+A fixpoint combinator that allows for deferred proofs of termination.
+
+{lean}`extrinsicFix₂ R F` is function implemented as the loop
+{lean}`extrinsicFix₂ R F a b = F a b (fun a' b' _ => extrinsicFix₂ R F a' b')`.
+
+If the loop can be shown to be well-founded, {name}`extrinsicFix₂_eq_apply` proves that it satisfies the
+fixpoint equation. Otherwise, {lean}`extrinsicFix₂ R F` is opaque, i.e., it is impossible to prove
+nontrivial properties about it.
+-/
+add_decl_doc extrinsicFix₂
+
+/--
+The function implemented as the loop
+{lean}`opaqueFix₃ R F a b c = F a b c (fun a' b' c' _ => opaqueFix₃ R F a' b' c')`.
+{lean}`opaqueFix₃ R F` is the fixpoint of the functional {name}`F`, as long as the loop is
+well-founded.
+
+The loop might run forever depending on {name}`F`. It is opaque, i.e., it is impossible to prove
+nontrivial properties about it.
+-/
+@[specialize]
+public partial def opaqueFix₃ [∀ a b c, Nonempty (C₃ a b c)]
+    (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop)
+    (F : ∀ (a b c), (∀ (a' b' c'), R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c)
+    (a : α) (b : β a) (c : γ a b) :
+    C₃ a b c :=
+  F a b c (fun a b c _ => opaqueFix₃ R F a b c)
+
+/-
+SAFE assuming that the code generated by iteration over `F` is equivalent to the well-founded
+fixpoint of `F` if `R` is well-founded.
+-/
+/--
+A fixpoint combinator that can be used to construct recursive functions of arity three with an
+*extrinsic* proof of termination.
+
+Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
+to {name}`R`, {lean}`extrinsicFix₃ R F` is the recursive function obtained by having {name}`F` call
+itself recursively.
+
+If {name}`R` is not well-founded, {lean}`extrinsicFix₃ R F` might run forever. In this case,
+nothing interesting can be proved about the recursive function; it is opaque.
+
+If {name}`R` _is_ well-founded, {lean}`extrinsicFix₃ R F` is equivalent to a well-founded recursive
+function, logically and regarding its termination behavior.
+-/
+@[implemented_by opaqueFix₃]
+public def extrinsicFix₃ [∀ a b c, Nonempty (C₃ a b c)]
+    (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop)
+    (F : ∀ (a b c), (∀ (a' b' c'), R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c)
+    (a : α) (b : β a) (c : γ a b) :
+    C₃ a b c :=
+  let F' (x : (a : α) ×' (b : β a) ×' γ a b) (G : (y : (a : α) ×' (b : β a) ×' γ a b) → R y x → C₃ y.1 y.2.1 y.2.2) :
+      C₃ x.1 x.2.1 x.2.2 :=
+    F x.1 x.2.1 x.2.2 (fun a b c => G ⟨a, b, c⟩)
+  extrinsicFix (C := fun x : (a : α) ×' (b : β a) ×' γ a b => C₃ x.1 x.2.1 x.2.2) R F' ⟨a, b, c⟩
+
+public theorem extrinsicFix₃_eq_fix [∀ a b c, Nonempty (C₃ a b c)]
+    {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
+    {F : ∀ a b c, (∀ a' b' c', R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c}
+    (wf : WellFounded R) {a b c} :
+    extrinsicFix₃ R F a b c = wf.fix (fun x G => F x.1 x.2.1 x.2.2 (fun a b c h => G ⟨a, b, c⟩ h)) ⟨a, b, c⟩ := by
+  rw [extrinsicFix₃, extrinsicFix_eq_fix wf]
+
+public theorem extrinsicFix₃_eq_apply [∀ a b c, Nonempty (C₃ a b c)]
+    {R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
+    {F : ∀ (a b c), (∀ (a' b' c'), R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c}
+    (wf : WellFounded R) {a : α} {b : β a} {c : γ a b} :
+    extrinsicFix₃ R F a b c = F a b c (fun a b c _ => extrinsicFix₃ R F a b c) := by
+  rw [extrinsicFix₃, extrinsicFix_eq_apply wf]
+  rfl
+
+/--
+A fixpoint combinator that allows for deferred proofs of termination.
+
+{lean}`extrinsicFix₃ R F` is function implemented as the loop
+{lean}`extrinsicFix₃ R F a b c = F a b c (fun a b c _ => extrinsicFix₃ R F a b c)`.
+
+If the loop can be shown to be well-founded, {name}`extrinsicFix₃_eq_apply` proves that it satisfies the
+fixpoint equation. Otherwise, {lean}`extrinsicFix₃ R F` is opaque, i.e., it is impossible to prove
+nontrivial properties about it.
+-/
+add_decl_doc extrinsicFix₃
+
+end WellFounded
diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
index 32580e1532..7d793910d6 100644
--- a/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
+++ b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
@@ -51,18 +51,10 @@ public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type
     IteratorCollect (AssocListIterator α β) Id m :=
   .defaultImplementation
 
-public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] :
-    IteratorCollectPartial (AssocListIterator α β) Id m :=
-  .defaultImplementation
-
 public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] :
     IteratorLoop (AssocListIterator α β) Id m :=
   .defaultImplementation
 
-public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] :
-    IteratorLoopPartial (AssocListIterator α β) Id m :=
-  .defaultImplementation
-
 /--
 Internal implementation detail of the hash map. Returns a finite iterator on an associative list.
 -/
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
index 71ecfcd7fe..eec1837b6a 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
@@ -156,16 +156,8 @@ instance Drop.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [
     IteratorCollect (Drop α m β) m n :=
   .defaultImplementation
 
-instance Drop.instIteratorCollectPartial {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorCollectPartial (Drop α m β) m n :=
-  .defaultImplementation
-
 instance Drop.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoop (Drop α m β) m n :=
   .defaultImplementation
 
-instance Drop.instIteratorLoopPartial {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorLoopPartial (Drop α m β) m n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
index 895348846b..e56dbf7b7f 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
@@ -275,17 +275,8 @@ instance DropWhile.instIteratorCollect [Monad m] [Monad n] [Iterator α m β] [P
     IteratorCollect (DropWhile α m β P) m n :=
   .defaultImplementation
 
-instance DropWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m β] {P} :
-    IteratorCollectPartial (DropWhile α m β P) m n :=
-  .defaultImplementation
-
 instance DropWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β] :
     IteratorLoop (DropWhile α m β P) m n :=
   .defaultImplementation
 
-instance DropWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
-    [IteratorLoopPartial α m n] [MonadLiftT m n] {P} :
-    IteratorLoopPartial (DropWhile α m β P) m n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
index 7e0534b0d1..43234e9eb7 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
@@ -139,19 +139,9 @@ instance Types.StepSizeIterator.instIteratorCollect {m n} [Iterator α m β]
     IteratorCollect (Types.StepSizeIterator α m β) m n :=
   .defaultImplementation
 
-instance Types.StepSizeIterator.instIteratorCollectPartial {m n} [Iterator α m β]
-    [IteratorAccess α m] [Monad m] [Monad n] :
-    IteratorCollectPartial (Types.StepSizeIterator α m β) m n :=
-  .defaultImplementation
-
 instance Types.StepSizeIterator.instIteratorLoop {m n} [Iterator α m β]
     [IteratorAccess α m] [Monad m] [Monad n] :
     IteratorLoop (Types.StepSizeIterator α m β) m n :=
   .defaultImplementation
 
-instance Types.StepSizeIterator.instIteratorLoopPartial {m n} [Iterator α m β]
-    [IteratorAccess α m] [Monad m] [Monad n] :
-    IteratorLoopPartial (Types.StepSizeIterator α m β) m n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
index ee3eb6a442..8881662af2 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
@@ -230,18 +230,9 @@ instance TakeWhile.instIteratorCollect [Monad m] [Monad n] [Iterator α m β] [P
     IteratorCollect (TakeWhile α m β P) m n :=
   .defaultImplementation
 
-instance TakeWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m β] {P} :
-    IteratorCollectPartial (TakeWhile α m β P) m n :=
-  .defaultImplementation
-
 instance TakeWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
     [IteratorLoop α m n] :
     IteratorLoop (TakeWhile α m β P) m n :=
   .defaultImplementation
 
-instance TakeWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
-    [IteratorLoopPartial α m n] {P} :
-    IteratorLoopPartial (TakeWhile α m β P) m n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean b/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean
index 515d1a5363..694da4bc76 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean
@@ -315,16 +315,8 @@ instance Zip.instIteratorCollect [Monad m] [Monad n] :
     IteratorCollect (Zip α₁ m α₂ β₂) m n :=
   .defaultImplementation
 
-instance Zip.instIteratorCollectPartial [Monad m] [Monad n] :
-    IteratorCollectPartial (Zip α₁ m α₂ β₂) m n :=
-  .defaultImplementation
-
 instance Zip.instIteratorLoop [Monad m] [Monad n] :
     IteratorLoop (Zip α₁ m α₂ β₂) m n :=
   .defaultImplementation
 
-instance Zip.instIteratorLoopPartial [Monad m] [Monad n] :
-    IteratorLoopPartial (Zip α₁ m α₂ β₂) m n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
index 428be6b623..a438818e99 100644
--- a/src/Std/Data/Iterators/Producers/Monadic/Array.lean
+++ b/src/Std/Data/Iterators/Producers/Monadic/Array.lean
@@ -116,19 +116,9 @@ instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
     IteratorCollect (ArrayIterator α) m n :=
   .defaultImplementation
 
-@[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
-    IteratorCollectPartial (ArrayIterator α) m n :=
-  .defaultImplementation
-
 @[always_inline, inline]
 instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
     IteratorLoop (ArrayIterator α) m n :=
   .defaultImplementation
 
-@[always_inline, inline]
-instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
-    IteratorLoopPartial (ArrayIterator α) m n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Producers/Monadic/Empty.lean b/src/Std/Data/Iterators/Producers/Monadic/Empty.lean
index 0382454a57..6e1a915999 100644
--- a/src/Std/Data/Iterators/Producers/Monadic/Empty.lean
+++ b/src/Std/Data/Iterators/Producers/Monadic/Empty.lean
@@ -61,16 +61,8 @@ instance Empty.instIteratorCollect {n : Type w → Type w''} [Monad m] [Monad n]
     IteratorCollect (Empty m β) m n :=
   .defaultImplementation
 
-instance Empty.instIteratorCollectPartial {n : Type w → Type w''} [Monad m] [Monad n] :
-    IteratorCollectPartial (Empty m β) m n :=
-  .defaultImplementation
-
 instance Empty.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] :
     IteratorLoop (Empty m β) m n :=
   .defaultImplementation
 
-instance Empty.instIteratorLoopPartial {n : Type x → Type x'} [Monad m] [Monad n] :
-    IteratorLoopPartial (Empty m β) m n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/src/Std/Data/Iterators/Producers/Repeat.lean b/src/Std/Data/Iterators/Producers/Repeat.lean
index 913a0ee7d1..2edfb7739d 100644
--- a/src/Std/Data/Iterators/Producers/Repeat.lean
+++ b/src/Std/Data/Iterators/Producers/Repeat.lean
@@ -72,16 +72,8 @@ instance RepeatIterator.instIteratorLoop {α : Type w} {f : α → α} {n : Type
     IteratorLoop (RepeatIterator α f) Id n :=
   .defaultImplementation
 
-instance RepeatIterator.instIteratorLoopPartial {α : Type w} {f : α → α} {n : Type w → Type w'}
-    [Monad n] : IteratorLoopPartial (RepeatIterator α f) Id n :=
-  .defaultImplementation
-
 instance RepeatIterator.instIteratorCollect {α : Type w} {f : α → α} {n : Type w → Type w'}
     [Monad n] : IteratorCollect (RepeatIterator α f) Id n :=
   .defaultImplementation
 
-instance RepeatIterator.instIteratorCollectPartial {α : Type w} {f : α → α} {n : Type w → Type w'}
-    [Monad n] : IteratorCollectPartial (RepeatIterator α f) Id n :=
-  .defaultImplementation
-
 end Std.Iterators
diff --git a/tests/bench/hashmap.lean b/tests/bench/hashmap.lean
index db2d8d8809..588588f328 100644
--- a/tests/bench/hashmap.lean
+++ b/tests/bench/hashmap.lean
@@ -33,9 +33,6 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
   step := fun ⟨it⟩ =>
     pure (.deflate ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩)
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
-  .defaultImplementation
-
 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
diff --git a/tests/bench/phashmap.lean b/tests/bench/phashmap.lean
index 62c7c5696a..d2443d643e 100644
--- a/tests/bench/phashmap.lean
+++ b/tests/bench/phashmap.lean
@@ -31,9 +31,6 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
   step := fun ⟨it⟩ =>
     pure (.deflate ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩)
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
-  .defaultImplementation
-
 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
diff --git a/tests/bench/sigmaIterator.lean b/tests/bench/sigmaIterator.lean
index 659acfd692..df27e5de02 100644
--- a/tests/bench/sigmaIterator.lean
+++ b/tests/bench/sigmaIterator.lean
@@ -110,21 +110,11 @@ instance SigmaIterator.instIteratorCollect {γ : Type w} {α : γ → Type w}
     IteratorCollect (SigmaIterator γ α) m n :=
   .defaultImplementation
 
-instance SigmaIterator.instIteratorCollectPartial {γ : Type w} {α : γ → Type w}
-    [∀ x : γ, Iterator (α x) m β] [Monad m] [Monad n] :
-    IteratorCollectPartial (SigmaIterator γ α) m n :=
-  .defaultImplementation
-
 instance SigmaIterator.instIteratorLoop {γ : Type w} {α : γ → Type w}
     [∀ x : γ, Iterator (α x) m β] [Monad m] [Monad n] :
     IteratorLoop (SigmaIterator γ α) m n :=
   .defaultImplementation
 
-instance SigmaIterator.instIteratorLoopPartial {γ : Type w} {α : γ → Type w}
-    [∀ x : γ, Iterator (α x) m β] [Monad m] [Monad n] :
-    IteratorLoopPartial (SigmaIterator γ α) m n :=
-  .defaultImplementation
-
 end Types
 
 /--
diff --git a/tests/bench/treemap.lean b/tests/bench/treemap.lean
index cc29bbc71d..07246ea510 100644
--- a/tests/bench/treemap.lean
+++ b/tests/bench/treemap.lean
@@ -28,9 +28,6 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
   step := fun ⟨it⟩ =>
     pure (.deflate ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩)
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
-  .defaultImplementation
-
 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
diff --git a/tests/lean/run/iterators.lean b/tests/lean/run/iterators.lean
index 66e7af9eb2..9925652767 100644
--- a/tests/lean/run/iterators.lean
+++ b/tests/lean/run/iterators.lean
@@ -14,13 +14,25 @@ section ListIteratorBasic
 #guard_msgs in
 #eval [1, 2, 3].iter.toList
 
+/-- info: [1, 2, 3] -/
+#guard_msgs in
+#eval [1, 2, 3].iter.ensureTermination.toList
+
+/-- info: [3, 2, 1] -/
+#guard_msgs in
+#eval [1, 2, 3].iter.toListRev
+
+/-- info: [3, 2, 1] -/
+#guard_msgs in
+#eval [1, 2, 3].iter.ensureTermination.toListRev
+
 /-- info: #[1, 2, 3] -/
 #guard_msgs in
 #eval [1, 2, 3].iter.toArray
 
-/-- info: [1, 2, 3] -/
+/-- info: #[1, 2, 3] -/
 #guard_msgs in
-#eval [1, 2, 3].iter |>.allowNontermination.toList
+#eval [1, 2, 3].iter.ensureTermination.toArray
 
 /-- info: ([1, 2, 3].iterM IO).toList : IO (List Nat) -/
 #guard_msgs in
@@ -342,3 +354,38 @@ example : (Std.Iterators.Iter.empty Nat).toList = [] := by
   simp
 
 end Empty
+
+section Termination
+
+example := positives.toList
+example := positives.toListRev
+example := positives.toArray
+
+/--
+error: failed to synthesize instance of type class
+  Std.Iterators.Finite (Std.Iterators.RepeatIterator Nat fun x => x + 1) Id
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+-/
+#guard_msgs in
+example := positives.ensureTermination.toList
+
+/--
+error: failed to synthesize instance of type class
+  Std.Iterators.Finite (Std.Iterators.RepeatIterator Nat fun x => x + 1) Id
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+-/
+#guard_msgs in
+example := positives.ensureTermination.toListRev
+
+/--
+error: failed to synthesize instance of type class
+  Std.Iterators.Finite (Std.Iterators.RepeatIterator Nat fun x => x + 1) Id
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+-/
+#guard_msgs in
+example := positives.ensureTermination.toArray
+
+end Termination