From 22cd34c341200986cbcbdbb8d1d40c24db595bf5 Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wojciech@lean-fro.org>
Date: Mon, 23 Jun 2025 17:41:22 +0200
Subject: [PATCH] chore: rename keywords for (co)inductive predicates and the
 names of the associated (co)induction principles

---
 .../Iterators/Lemmas/Combinators/Monadic/FilterMap.lean     | 6 +++---
 src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean        | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index 6d16885081..8ca14e1b20 100644
--- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -131,7 +131,7 @@ theorem IterM.step_filterM {f : β → n (ULift Bool)}
   intro step
   match step with
   | .yield it' out h =>
-    simp only [PostconditionT.lift, 
+    simp only [PostconditionT.lift,
       PostconditionT.operation_map, Functor.map_map, PlausibleIterStep.skip,
       PlausibleIterStep.yield, bind_map_left]
     apply bind_congr
@@ -156,7 +156,7 @@ theorem IterM.step_mapM {γ : Type w} {f : β → n γ}
   match step with
   | .yield it' out h =>
     simp only [bind_pure_comp]
-    simp only [PostconditionT.lift, Functor.map, 
+    simp only [PostconditionT.lift, Functor.map,
       ]
     simp only [PostconditionT.operation_map, Functor.map_map, PlausibleIterStep.skip,
       PlausibleIterStep.yield, bind_map_left, bind_pure_comp]
@@ -483,7 +483,7 @@ theorem IterM.Equiv.filterMapWithPostcondition {α₁ α₂ β γ : Type w}
     (h : IterM.Equiv ita itb) :
     IterM.Equiv (ita.filterMapWithPostcondition f) (itb.filterMapWithPostcondition f) := by
   rw [IterM.Equiv]
-  refine BundledIterM.Equiv.fixpoint_induct n γ ?R ?implies (.ofIterM _) (.ofIterM _) ?hR
+  refine BundledIterM.Equiv.coinduct n γ ?R ?implies (.ofIterM _) (.ofIterM _) ?hR
   case R =>
     intro ita' itb'
     exact ∃ (ita : IterM (α := α₁) m β) (itb : IterM (α := α₂) m β),
diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean
index 4528a69dfa..63f6a00b44 100644
--- a/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean
+++ b/src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean
@@ -83,7 +83,7 @@ def BundledIterM.Equiv (m : Type w → Type w') (β : Type w) [Monad m] [LawfulM
     (ita itb : BundledIterM m β) : Prop :=
   (BundledIterM.step ita).map (IterStep.mapIterator (Quot.mk (BundledIterM.Equiv m β))) =
   (BundledIterM.step itb).map (IterStep.mapIterator (Quot.mk (BundledIterM.Equiv m β)))
-greatest_fixpoint monotonicity by
+coinductive_fixpoint monotonicity by
   intro R S hRS ita itb h
   simp only [BundledIterM.step] at ⊢ h
   simp only [quotMk_eq_quotOfQuot_comp hRS, IterStep.mapIterator_comp, HetT.comp_map, h]
@@ -130,7 +130,7 @@ protected theorem BundledIterM.Equiv.exact {m : Type w → Type w'} {β : Type w
     [LawfulMonad m] (ita itb : BundledIterM m β) :
     Quot.mk (BundledIterM.Equiv m β) ita =
       Quot.mk (BundledIterM.Equiv m β) itb → BundledIterM.Equiv m β ita itb := by
-  refine BundledIterM.Equiv.fixpoint_induct m β
+  refine BundledIterM.Equiv.coinduct m β
     (fun ita' itb' => Quot.mk _ ita' = Quot.mk _ itb') ?_ ita itb
   intro ita' itb' h
   replace h := congrArg (BundledIterM.stepOnQuotient) h
@@ -240,7 +240,7 @@ theorem IterM.Equiv.of_morphism {α₁ α₂} {m : Type w → Type w'} [Monad m]
     (f : IterM (α := α₁) m β → IterM (α := α₂) m β)
     (h : ∀ it, IterM.stepAsHetT (f it) = IterStep.mapIterator f <$> IterM.stepAsHetT it) :
     IterM.Equiv ita (f ita) := by
-  refine BundledIterM.Equiv.fixpoint_induct m β ?R ?implies (.ofIterM ita) (.ofIterM (f ita)) ?hf
+  refine BundledIterM.Equiv.coinduct m β ?R ?implies (.ofIterM ita) (.ofIterM (f ita)) ?hf
   case R =>
     intro ita itb
     exact ∃ it, ita = .ofIterM it ∧ itb = .ofIterM (f it)