clean up the fixpoint combinator

Author: datokrat

src/Init/Data/Iterators/Basic.lean

@@ -703,18 +703,6 @@ def IterM.TerminationMeasures.Finite.Rel
     TerminationMeasures.Finite α m → TerminationMeasures.Finite α m → Prop :=
   Relation.TransGen <| InvImage IterM.IsPlausibleSuccessorOf IterM.TerminationMeasures.Finite.it
 
-/--
-The relation of plausible successors on `IterM.TerminationMeasures.Finite`. It is well-founded
-if there is a `Finite` instance.
--/
-@[expose]
-def IterM.TerminationMeasures.Finite.RelExtrinsic
-    {α : Type w} {m : Type w → Type w'} {β : Type w}
-    (R : IterM (α := α) m β → IterM (α := α) m β → Prop)
-    [Iterator α m β] :
-    TerminationMeasures.Finite α m → TerminationMeasures.Finite α m → Prop :=
-  Relation.TransGen <| InvImage R IterM.TerminationMeasures.Finite.it
-
 instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [Finite α m] : WellFoundedRelation (IterM.TerminationMeasures.Finite α m) where
   rel := IterM.TerminationMeasures.Finite.Rel

src/Init/Data/Iterators/Consumers/Collect.lean

@@ -43,7 +43,7 @@ Traverses the given iterator and stores the emitted values in an array.
 
 This function is deprecated. Instead of `it.allowNontermination.toArray`, use `it.toArray`.
 -/
-@[always_inline, inline, deprecated Iter.toArray (since := "2025-10-23")]
+@[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
@@ -78,7 +78,7 @@ 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-10-23")]
+@[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.toListRev
@@ -113,7 +113,7 @@ 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-10-23")]
+@[always_inline, deprecated Iter.toList (since := "2025-12-04")]
 def Iter.Partial.toList {α : Type w} {β : Type w}
     [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : List β :=
   it.it.toList

src/Init/Data/Iterators/Consumers/Loop.lean

@@ -117,7 +117,7 @@ It is equivalent to `it.toList.foldlM`.
 
 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 β]
     [IteratorLoop α Id m] (f : γ → β → m γ)
@@ -160,7 +160,7 @@ It is equivalent to `it.toList.foldl`.
 
 This function is deprecated. Instead of `it.allowNontermination.fold`, use `it.fold`.
 -/
-@[always_inline, inline]
+@[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 (α := α) β) : γ :=
@@ -375,7 +375,7 @@ Almost! 5
 some 10
 ```
 -/
-@[inline, deprecated Iter.findSomeM? (since := "2025-10-21")]
+@[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 γ)) :
@@ -449,7 +449,7 @@ 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-10-21")]
+@[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 γ :=
@@ -534,7 +534,7 @@ Almost! 5
 some 1
 ```
 -/
-@[inline, deprecated Iter.findM? (since := "2025-10-21")]
+@[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 β) :=
@@ -605,7 +605,7 @@ 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-10-21")]
+@[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 β :=
   it.it.find? f

src/Init/Data/Iterators/Consumers/Monadic/Collect.lean

@@ -9,7 +9,7 @@ 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.Internal.ExtrinsicTermination
+public import Init.WFExtrinsicFix
 
 @[expose] public section
 
@@ -82,44 +82,14 @@ where
   @[always_inline]
   go it (acc : Array γ) : n (Array γ) :=
     letI : MonadLift m n := ⟨lift (α := _)⟩
-    extrinsicFix₂ (C₂ := fun _ _ => n (Array γ)) (InvImage TerminationMeasures.Finite.Rel (·.1.finitelyManySteps!))
+    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
 
--- @[always_inline, no_expose]
--- def IterM.DefaultConsumers.toArrayMapped {α β : Type w} {m : Type w → Type w'}
---     {n : Type w → Type w''} [Monad n] [MonadAttach 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
---   @[always_inline]
---   go it (acc : Array γ) : n (Array γ) :=
---     letI : MonadLift m n := ⟨lift (α := _)⟩
---     extrinsicFix₂ (C₂ := fun _ _ => n (Array γ))
---     (fun x' x => (∃ out, x.1.IsPlausibleStepE (.yield x'.1 out) ∧ ∃ fx, MonadAttach.CanReturn (f out) fx ∧ x'.2 = x.2.push fx) ∨ (∃ h, MonadAttach.CanReturn (m := n) x.1.step (.deflate <| .skip x'.1 h) ∧ x'.2 = x.2))
---     (fun (it : IterM (α := α) m β) acc recur => do
---       let ⟨step, hs⟩ ← MonadAttach.attach (m := n) it.step
---       match hs' : step.inflate with
---       | .yield it' out h =>
---         let fx ← MonadAttach.attach (f out)
---         recur it' (acc.push fx.val) (by
---           apply Or.inl
---           have : step = .deflate (.yield it' out h) := by simp [← hs']
---           rw [this] at hs
---           exact ⟨out, h, hs, fx.val, fx.property, rfl⟩)
---       | .skip it' h => recur it' acc (by
---           apply Or.inr
---           have : step = .deflate (.skip it' h) := by simp [← hs']
---           rw [this] at hs
---           exact ⟨h, hs, rfl⟩)
---       | .done h => return acc) it acc
-
 /--
 This is the default implementation of the `IteratorCollect` class.
 It simply iterates through the iterator using `IterM.step`, incrementally building up the desired
@@ -208,7 +178,7 @@ def IterM.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type
 where
   @[always_inline, inline]
   go (it : IterM m β) acc :=
-    extrinsicFix₂ (InvImage TerminationMeasures.Finite.Rel (·.1.finitelyManySteps!))
+    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)

src/Init/Data/Iterators/Consumers/Monadic/Loop.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Data.Iterators.Consumers.Monadic.Partial
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
-public import Init.Internal.ExtrinsicTermination
+public import Init.WFExtrinsicFix
 public import Init.Data.Iterators.Consumers.Monadic.Total
 
 public section
@@ -101,12 +101,12 @@ def IterM.DefaultConsumers.forIn' {m : Type w → Type w'} {α : Type w} {β : T
     [Iterator α m β]
     {n : Type x → Type x'} [Monad n]
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) (γ : Type x)
-    (plausible_forInStep : β → γ → ForInStep γ → Prop)
+    (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⟩
-  extrinsicFix₃ (C₃ := fun _ _ _ => n γ) (InvImage (IteratorLoop.rel α m plausible_forInStep) (fun x => (x.1, x.2.1)))
+  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 =>
@@ -121,25 +121,24 @@ This is the loop implementation of the default instance `IteratorLoop.defaultImp
 -/
 @[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]
+    [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)
+    (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 (plausible_forInStep b c))) : n γ :=
+    (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'.wf 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'.wf 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)
@@ -284,7 +283,7 @@ function. Therefore, it may *not* be equivalent to `it.toList.foldlM`.
 
 This function is deprecated. Instead of `it.allowNontermination.foldM`, use `it.foldM`.
 -/
-@[always_inline, inline, deprecated IterM.foldM (since := "2025-10-21")]
+@[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 β] [IteratorLoop α m n] [MonadLiftT m n]
     (f : γ → β → n γ) (init : γ) (it : IterM.Partial (α := α) m β) : n γ :=
@@ -326,7 +325,7 @@ It is equivalent to `it.toList.foldl`.
 
 This function is deprecated. Instead of `it.allowNontermination.fold`, use `it.fold`.
 -/
-@[always_inline, inline, deprecated IterM.Partial.fold (since := "2025-10-21")]
+@[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 β] [IteratorLoop α m m] (f : γ → β → γ) (init : γ)
     (it : IterM.Partial (α := α) m β) : m γ :=
@@ -363,7 +362,7 @@ emitted values.
 
 This function is deprecated. Instead of `it.allowNontermination.drain`, use `it.drain`.
 -/
-@[always_inline, inline, deprecated IterM.drain (since := "2025-10-21")]
+@[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
@@ -408,7 +407,7 @@ examined in order of iteration.
 
 This function is deprecated. Instead of {lit}`it.allowNontermination.anyM`, use {lit}`it.anyM`.
 -/
-@[always_inline, inline, deprecated IterM.anyM (since := "2025-10-21")]
+@[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 β] [IteratorLoop α m m] (p : β → m (ULift Bool))
     (it : IterM.Partial (α := α) m β) : m (ULift Bool) :=
@@ -455,7 +454,7 @@ examined in order of iteration.
 
 This function is deprecated. Instead of {lit}`it.allowNontermination.any`, use {lit}`it.any`.
 -/
-@[inline, deprecated IterM.any (since := "2025-10-21")]
+@[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
@@ -504,7 +503,7 @@ examined in order of iteration.
 
 This function is deprecated. Instead of {lit}`it.allowNontermination.allM`, use {lit}`it.allM`.
 -/
-@[always_inline, inline, deprecated IterM.allM (since := "2025-10-21")]
+@[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
@@ -553,7 +552,7 @@ examined in order of iteration.
 
 This function is deprecated. Instead of {lit}`it.allowNontermination.allM`, use {lit}`it.allM`.
 -/
-@[inline, deprecated IterM.all (since := "2025-10-21")]
+@[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
@@ -637,7 +636,7 @@ Almost! 5
 some 10
 ```
 -/
-@[inline, deprecated IterM.findSomeM? (since := "2025-10-21")]
+@[inline, deprecated IterM.findSomeM? (since := "2025-12-04")]
 def IterM.Partial.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
     [IteratorLoop α m m] (it : IterM.Partial (α := α) m β) (f : β → m (Option γ)) :
     m (Option γ) :=
@@ -709,7 +708,7 @@ 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-10-21")]
+@[inline, deprecated IterM.findSome? (since := "2025-12-04")]
 def IterM.Partial.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
     [IteratorLoop α m m] (it : IterM.Partial (α := α) m β) (f : β → Option γ) :
     m (Option γ) :=
@@ -794,7 +793,7 @@ Almost! 5
 some 1
 ```
 -/
-@[inline, deprecated IterM.findM? (since := "2025-10-21")]
+@[inline, deprecated IterM.findM? (since := "2025-12-04")]
 def IterM.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
     [IteratorLoop α m m] (it : IterM.Partial (α := α) m β) (f : β → m (ULift Bool)) :
     m (Option β) :=
@@ -866,7 +865,7 @@ 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-10-21")]
+@[inline, deprecated IterM.find? (since := "2025-12-04")]
 def IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
     [IteratorLoop α m m] (it : IterM.Partial (α := α) m β) (f : β → Bool) :
     m (Option β) :=

src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean

@@ -11,7 +11,7 @@ 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.Internal.ExtrinsicTermination
+import all Init.WFExtrinsicFix
 
 public section
 
@@ -30,7 +30,7 @@ private theorem IterM.DefaultConsumers.toArrayMapped.go_eq [Monad n]
       | .skip it' => go lift f it' acc
       | .done => return acc) := by
   letI : MonadLift m n := ⟨lift (δ := _)⟩
-  rw [toArrayMapped.go, extrinsicFix₂_eq]
+  rw [toArrayMapped.go, WellFounded.extrinsicFix₂_eq_apply]
   · simp only
     apply bind_congr; intro step
     cases step.inflate using PlausibleIterStep.casesOn
@@ -42,35 +42,6 @@ private theorem IterM.DefaultConsumers.toArrayMapped.go_eq [Monad n]
     apply InvImage.wf
     exact WellFoundedRelation.wf
 
--- private theorem IterM.DefaultConsumers.toArrayMapped.go_eq [Monad n] [MonadAttach 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, extrinsicFix₂_eq]
---   · simp only
---     simp only [← MonadAttach.map_val_attach (x := liftM it.step), map_eq_pure_bind, bind_assoc]
---     apply bind_congr; rintro ⟨step, hs⟩
---     simp only [pure_bind]
---     cases step.inflate using PlausibleIterStep.casesOn
---     · simp only [← MonadAttach.map_val_attach (x := f _), map_eq_pure_bind, bind_assoc]
---       apply bind_congr; intro fx
---       simp [go]
---     · simp [go]
---     · simp
---   · apply Subrelation.wf (r := InvImage WellFoundedRelation.rel (·.1.finitelyManySteps))
---     · intro x' x h
---       apply Relation.TransGen.single
---       match h with
---       | Or.inl ⟨out, h, h'⟩ => exact ⟨_, rfl, h⟩
---       | Or.inr ⟨h, h'⟩ => exact ⟨_, rfl, h⟩
---     · 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) =
@@ -195,7 +166,7 @@ private theorem IterM.toListRev.go_eq [Monad m] [LawfulMonad m] [Iterator α m 
       | .yield it' out => go it' (out :: bs)
       | .skip it' => go it' bs
       | .done => return bs) := by
-  rw [go, extrinsicFix₂_eq]
+  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]