From b5c4880f9315caebc3be5fd44db0eb177a291dea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Wed, 23 Oct 2024 15:50:54 +0200
Subject: [PATCH 01/28] feat(CategoryTheory/SmallObject): very basic API for
 the iteration of functors

---
 Mathlib.lean                                  |  1 +
 .../{Iteration.lean => Iteration/Basic.lean}  | 69 +++++++++++++++++++
 2 files changed, 70 insertions(+)
 rename Mathlib/CategoryTheory/SmallObject/{Iteration.lean => Iteration/Basic.lean} (73%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 6986c912408c1..acca8d71d8e0d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1955,6 +1955,7 @@ import Mathlib.CategoryTheory.Sites.Whiskering
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.SmallObject.Construction
 import Mathlib.CategoryTheory.SmallObject.Iteration
+import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 import Mathlib.CategoryTheory.Square
 import Mathlib.CategoryTheory.Subobject.Basic
 import Mathlib.CategoryTheory.Subobject.Comma
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
similarity index 73%
rename from Mathlib/CategoryTheory/SmallObject/Iteration.lean
rename to Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index a9470418b418d..838f31a96e998 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -76,6 +76,19 @@ def coconeOfLE : Cocone (restrictionLT F hi) where
       naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ _ => by
         simp [comp_id, ← Functor.map_comp, homOfLE_comp] }
 
+/-- The functor `{ k // k ≤ i } ⥤ C` obtained by "restriction" of `F : { i // i ≤ j } ⥤ C`
+when `i ≤ j`. -/
+def restrictionLE : { k | k ≤ i } ⥤ C :=
+  (monotone_inclusion_le_le_of_le hi).functor ⋙ F
+
+@[simp]
+lemma restrictionLE_obj (k : J) (hk : k ≤ i) :
+    (restrictionLE F hi).obj ⟨k, hk⟩ = F.obj ⟨k, hk.trans hi⟩ := rfl
+
+@[simp]
+lemma restrictionLE_map {k₁ k₂ : { k | k ≤ i }} (φ : k₁ ⟶ k₂) :
+    (restrictionLE F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl
+
 end Iteration
 
 variable [IsWellOrder J (· < ·)] [OrderBot J]
@@ -186,6 +199,62 @@ instance : Subsingleton (iter₁ ⟶ iter₂) where
 
 end Hom
 
+@[simp]
+lemma natTrans_id : Hom.natTrans (𝟙 iter₁) = 𝟙 _ := rfl
+
+variable {iter₁ iter₂}
+
+@[simp, reassoc]
+lemma natTrans_comp {iter₃ : Iteration ε j} (φ : iter₁ ⟶ iter₂) (ψ : iter₂ ⟶ iter₃) :
+    (φ ≫ ψ).natTrans = φ.natTrans ≫ ψ.natTrans := rfl
+
+@[reassoc]
+lemma natTrans_naturality (φ : iter₁ ⟶ iter₂) (i₁ i₂ : J) (h : i₁ ≤ i₂) (h' : i₂ ≤ j) :
+    iter₁.F.map (by exact homOfLE h) ≫ φ.natTrans.app ⟨i₂, h'⟩ =
+      φ.natTrans.app ⟨i₁, h.trans h'⟩ ≫ iter₂.F.map (by exact homOfLE h) := by
+  apply φ.natTrans.naturality
+
+variable (ε) in
+/-- The evaluation functor `Iteration ε j ⥤ C ⥤ C` at `i : J` when `i ≤ j`. -/
+@[simps]
+def eval {i : J} (hi : i ≤ j) : Iteration ε j ⥤ C ⥤ C where
+  obj iter := iter.F.obj ⟨i, hi⟩
+  map φ := φ.natTrans.app _
+
+/-- Given `iter : Iteration ε j` and `i : J` such that `i ≤ j`, this is the
+induced element in `Iteration ε i`. -/
+@[simps F isoZero isoSucc]
+def trunc (iter : Iteration ε j) {i : J} (hi : i ≤ j) : Iteration ε i where
+  F := restrictionLE (iter.F) hi
+  isoZero := iter.isoZero
+  isoSucc k hk := iter.isoSucc k (lt_of_lt_of_le hk hi)
+  mapSucc'_eq k hk := iter.mapSucc'_eq k (lt_of_lt_of_le hk hi)
+  isColimit k _ hk := iter.isColimit k (hk.trans hi)
+
+variable (ε) in
+/-- The truncation functor `Iteration ε j ⥤ Iteration ε i` when `i ≤ j`. -/
+@[simps obj]
+def truncFunctor {i : J} (hi : i ≤ j) : Iteration ε j ⥤ Iteration ε i where
+  obj iter := iter.trunc hi
+  map {iter₁ iter₂} φ :=
+    { natTrans := whiskerLeft _ φ.natTrans
+      natTrans_app_succ := fun k hk => φ.natTrans_app_succ k (lt_of_lt_of_le hk hi) }
+
+@[simp]
+lemma truncFunctor_map_natTrans_app
+    (φ : iter₁ ⟶ iter₂) {i : J} (hi : i ≤ j) (k : J) (hk : k ≤ i) :
+    ((truncFunctor ε hi).map φ).natTrans.app ⟨k, hk⟩ =
+      φ.natTrans.app ⟨k, hk.trans hi⟩ := rfl
+
+namespace Hom
+
+lemma congr_app (φ φ' : iter₁ ⟶ iter₂) (i : J) (hi : i ≤ j) :
+    φ.natTrans.app ⟨i, hi⟩ = φ'.natTrans.app ⟨i, hi⟩ := by
+  obtain rfl := Subsingleton.elim φ φ'
+  rfl
+
+end Hom
+
 end Iteration
 
 end Functor

From 73f351792ea008a8bd492310fab8bf21650313bb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Wed, 23 Oct 2024 16:35:40 +0200
Subject: [PATCH 02/28] feat(CategoryTheory/SmallObject): construction of a
 morphism between iterations of functors in two cases

---
 Mathlib.lean                                  |   1 +
 .../SmallObject/Iteration/Basic.lean          |   6 +-
 .../SmallObject/Iteration/UniqueHom.lean      | 141 ++++++++++++++++++
 3 files changed, 145 insertions(+), 3 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index acca8d71d8e0d..fc81b47eee87b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1956,6 +1956,7 @@ import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.SmallObject.Construction
 import Mathlib.CategoryTheory.SmallObject.Iteration
 import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
+import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 import Mathlib.CategoryTheory.Square
 import Mathlib.CategoryTheory.Subobject.Basic
 import Mathlib.CategoryTheory.Subobject.Comma
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index 838f31a96e998..ecd3045676137 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -18,8 +18,8 @@ a functor `F : { i // i ≤ j } ⥤ C ⥤ C` equipped with the data
 which makes it the `i`th-iteration of `Φ` for all `i` such that `i ≤ j`.
 Under suitable assumptions on `C`, we shall show that this category
 `Iteration ε j` is equivalent to the punctual category (TODO).
-We shall study morphisms in this category, showing first that
-there is at most one morphism between two morphisms (done), and secondly,
+In this file, we show that the there is at most one morphism between
+two objects. In `SmallObject.Iteration.UniqueHom`, we shall show
 that there does always exist a unique morphism between
 two objects (TODO). Then, we shall show the existence of
 an object (TODO). In these proofs, which are all done using
@@ -173,7 +173,7 @@ lemma ext' {f g : Hom iter₁ iter₂} (h : f.natTrans = g.natTrans) : f = g :=
 
 attribute [local ext] ext'
 
-/-- The composition of morphisms in the category `Φ.Iteration ε j`. -/
+/-- The composition of morphisms in the category `Iteration ε j`. -/
 @[simps]
 def comp {iter₃ : Iteration ε j} (f : Hom iter₁ iter₂) (g : Hom iter₂ iter₃) :
     Hom iter₁ iter₃ where
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
new file mode 100644
index 0000000000000..76df8a73ea5a3
--- /dev/null
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
@@ -0,0 +1,141 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
+
+/-!
+# Uniqueness of morphisms in the category of iterations of functors
+
+Given a functor `Φ : C ⥤ C` and a natural transformation `ε : 𝟭 C ⟶ Φ`,
+we shall show in this file that there exists a unique morphism (TODO)
+between two arbitrary objects in the category `Functor.Iteration ε j`
+when `j : J` and `J` is a well orderered set.
+
+-/
+
+universe u
+
+namespace CategoryTheory
+
+open Category Limits
+
+variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ}
+  {J : Type u} [LinearOrder J]
+
+namespace Functor
+
+namespace Iteration
+
+namespace Hom
+
+variable [IsWellOrder J (· < ·)] [OrderBot J] (j : J)
+
+/-- The (unique) morphism between two objects in `Iteration ε ⊥` -/
+def mkOfBot (iter₁ iter₂ : Iteration ε (⊥ : J)) : iter₁ ⟶ iter₂ where
+  natTrans :=
+    { app := fun ⟨i, hi⟩ => eqToHom (by congr; simpa using hi) ≫ iter₁.isoZero.hom ≫
+        iter₂.isoZero.inv ≫ eqToHom (by congr; symm; simpa using hi)
+      naturality := fun ⟨i, hi⟩ ⟨k, hk⟩ φ => by
+        obtain rfl : i = ⊥ := by simpa using hi
+        obtain rfl : k = ⊥ := by simpa using hk
+        obtain rfl : φ = 𝟙 _ := rfl
+        simp }
+  natTrans_app_succ i hi := by simp at hi
+
+section
+
+variable {i : J} {iter₁ iter₂ : Iteration ε (wellOrderSucc i)}
+  (hi : i < wellOrderSucc i) (φ : iter₁.trunc hi.le ⟶ iter₂.trunc hi.le)
+
+/-- Auxiliary definition for `mkOfSucc`. -/
+noncomputable def mkOfSuccNatTransApp (k : J) (hk : k ≤ wellOrderSucc i) :
+    iter₁.F.obj ⟨k, hk⟩ ⟶ iter₂.F.obj ⟨k, hk⟩ :=
+  if hk' : k = wellOrderSucc i then
+    eqToHom (by subst hk'; rfl) ≫ (iter₁.isoSucc i hi).hom ≫
+      whiskerRight (φ.natTrans.app ⟨i, by rfl⟩) _ ≫ (iter₂.isoSucc i hi).inv ≫
+      eqToHom (by subst hk'; rfl)
+  else
+    φ.natTrans.app ⟨k, le_of_lt_wellOrderSucc (by
+      obtain hk|rfl := hk.lt_or_eq
+      · exact hk
+      · tauto)⟩
+
+lemma mkOfSuccNatTransApp_eq_of_le (k : J) (hk : k ≤ i) :
+    mkOfSuccNatTransApp hi φ k (hk.trans (self_le_wellOrderSucc i)) =
+      φ.natTrans.app ⟨k, hk⟩ :=
+  dif_neg (by rintro rfl; simpa using lt_of_le_of_lt hk hi)
+
+@[simp]
+lemma mkOfSuccNatTransApp_wellOrderSucc_eq :
+    mkOfSuccNatTransApp hi φ (wellOrderSucc i) (by rfl) =
+      (iter₁.isoSucc i hi).hom ≫ whiskerRight (φ.natTrans.app ⟨i, by rfl⟩) _ ≫
+        (iter₂.isoSucc i hi).inv := by
+  dsimp [mkOfSuccNatTransApp]
+  rw [dif_pos rfl, comp_id, id_comp]
+
+/-- Auxiliary definition for `mkOfSucc`. -/
+@[simps]
+noncomputable def mkOfSuccNatTrans :
+    iter₁.F ⟶ iter₂.F where
+  app := fun ⟨k, hk⟩ => mkOfSuccNatTransApp hi φ k hk
+  naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by
+    dsimp
+    have hk : k₁ ≤ k₂ := leOfHom f
+    obtain h₂ | rfl := hk₂.lt_or_eq
+    · replace h₂ : k₂ ≤ i := le_of_lt_wellOrderSucc h₂
+      rw [mkOfSuccNatTransApp_eq_of_le hi φ k₂ h₂,
+        mkOfSuccNatTransApp_eq_of_le hi φ k₁ (hk.trans h₂)]
+      exact natTrans_naturality φ k₁ k₂ hk h₂
+    · obtain h₁ | rfl := hk.lt_or_eq
+      · have h₂ : k₁ ≤ i := le_of_lt_wellOrderSucc h₁
+        let f₁ : (⟨k₁, hk⟩ : { l | l ≤ wellOrderSucc i}) ⟶
+          ⟨i, self_le_wellOrderSucc i⟩ := homOfLE h₂
+        let f₂ : (⟨i, self_le_wellOrderSucc i⟩ : { l | l ≤ wellOrderSucc i}) ⟶
+          ⟨wellOrderSucc i, by dsimp; rfl⟩ := homOfLE (self_le_wellOrderSucc i)
+        obtain rfl : f = f₁ ≫ f₂ := rfl
+        rw [Functor.map_comp, Functor.map_comp, assoc,
+          mkOfSuccNatTransApp_eq_of_le hi φ k₁ h₂]
+        erw [← natTrans_naturality_assoc φ k₁ i h₂ (by rfl)]
+        rw [mkOfSuccNatTransApp_wellOrderSucc_eq]
+        dsimp
+        change _ ≫ iter₁.mapSucc i hi ≫ _ = _ ≫ _ ≫ iter₂.mapSucc i hi
+        rw [iter₁.mapSucc_eq i hi, iter₂.mapSucc_eq i hi, assoc,
+          Iso.inv_hom_id_assoc]
+        ext X
+        dsimp
+        rw [← ε.naturality_assoc]
+        rfl
+      · obtain rfl : f = 𝟙 _ := rfl
+        rw [Functor.map_id, Functor.map_id, id_comp, comp_id]
+
+end
+
+/-- The (unique) morphism between two objects in `Iteration ε (wellOrderSucc i)`,
+assuming we have a morphism between the truncations to `Iteration ε i`. -/
+noncomputable def mkOfSucc
+    {i : J} (iter₁ iter₂ : Iteration ε (wellOrderSucc i)) (hi : i < wellOrderSucc i)
+    (φ : iter₁.trunc hi.le ⟶ iter₂.trunc hi.le) :
+    iter₁ ⟶ iter₂ where
+  natTrans := mkOfSuccNatTrans hi φ
+  natTrans_app_zero := by
+    dsimp
+    rw [mkOfSuccNatTransApp_eq_of_le _ _ _ bot_le, φ.natTrans_app_zero]
+    rfl
+  natTrans_app_succ k hk := by
+    obtain hk' | rfl := (le_of_lt_wellOrderSucc hk).lt_or_eq
+    · dsimp
+      rw [mkOfSuccNatTransApp_eq_of_le hi φ k hk'.le,
+        mkOfSuccNatTransApp_eq_of_le hi φ (wellOrderSucc k) (wellOrderSucc_le hk'),
+        φ.natTrans_app_succ _ hk']
+      rfl
+    · simp [mkOfSuccNatTransApp_eq_of_le hi φ k (by rfl)]
+
+end Hom
+
+end Iteration
+
+end Functor
+
+end CategoryTheory

From 9a2e020895fa4247091aaf9dc78ba2bbf0ce3bdd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Wed, 23 Oct 2024 17:28:39 +0200
Subject: [PATCH 03/28] Update Mathlib.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index acca8d71d8e0d..27c1b91cd3f8b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1954,7 +1954,6 @@ import Mathlib.CategoryTheory.Sites.Types
 import Mathlib.CategoryTheory.Sites.Whiskering
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.SmallObject.Construction
-import Mathlib.CategoryTheory.SmallObject.Iteration
 import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 import Mathlib.CategoryTheory.Square
 import Mathlib.CategoryTheory.Subobject.Basic

From f497043c992d0ab5de5bf6346ce480053b25d758 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Wed, 23 Oct 2024 17:29:23 +0200
Subject: [PATCH 04/28] fix Mathlib.lean

---
 Mathlib.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index fc81b47eee87b..4ccf3cecf7c3e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1954,7 +1954,6 @@ import Mathlib.CategoryTheory.Sites.Types
 import Mathlib.CategoryTheory.Sites.Whiskering
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.SmallObject.Construction
-import Mathlib.CategoryTheory.SmallObject.Iteration
 import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 import Mathlib.CategoryTheory.Square

From 46bf440e085847b837aa0a51ee7aac614816fa90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Wed, 23 Oct 2024 18:44:27 +0200
Subject: [PATCH 05/28] feat(CategoryTheory/SmallObject/Iteration): the unique
 morphism (limit case)

---
 .../SmallObject/Iteration/UniqueHom.lean      | 106 +++++++++++++++++-
 1 file changed, 102 insertions(+), 4 deletions(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
index 76df8a73ea5a3..50a9595e16d28 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
@@ -9,7 +9,7 @@ import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 # Uniqueness of morphisms in the category of iterations of functors
 
 Given a functor `Φ : C ⥤ C` and a natural transformation `ε : 𝟭 C ⟶ Φ`,
-we shall show in this file that there exists a unique morphism (TODO)
+we show in this file that there exists a unique morphism
 between two arbitrary objects in the category `Functor.Iteration ε j`
 when `j : J` and `J` is a well orderered set.
 
@@ -22,7 +22,7 @@ namespace CategoryTheory
 open Category Limits
 
 variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ}
-  {J : Type u} [LinearOrder J]
+  {J : Type u} [LinearOrder J] [IsWellOrder J (· < ·)] [OrderBot J] (j : J)
 
 namespace Functor
 
@@ -30,8 +30,6 @@ namespace Iteration
 
 namespace Hom
 
-variable [IsWellOrder J (· < ·)] [OrderBot J] (j : J)
-
 /-- The (unique) morphism between two objects in `Iteration ε ⊥` -/
 def mkOfBot (iter₁ iter₂ : Iteration ε (⊥ : J)) : iter₁ ⟶ iter₂ where
   natTrans :=
@@ -132,8 +130,108 @@ noncomputable def mkOfSucc
       rfl
     · simp [mkOfSuccNatTransApp_eq_of_le hi φ k (by rfl)]
 
+variable {j} {iter₁ iter₂ : Iteration ε j}
+
+section
+
+variable [IsWellOrderLimitElement j]
+  (φ : ∀ (i : J) (hi : i < j), iter₁.trunc hi.le ⟶ iter₂.trunc hi.le)
+
+/-- Auxiliary definition for `mkOfLimit`. -/
+def mkOfLimitNatTransApp (i : J) (hi : i ≤ j) :
+    iter₁.F.obj ⟨i, hi⟩ ⟶ iter₂.F.obj ⟨i, hi⟩ :=
+  if h : i < j
+    then
+      (φ i h).natTrans.app ⟨i, by rfl⟩
+    else by
+      obtain rfl : i = j := by
+        obtain h' | rfl := hi.lt_or_eq
+        · exfalso
+          exact h h'
+        · rfl
+      exact (iter₁.isColimit i (show i ≤ i by rfl)).desc (Cocone.mk _
+        { app := fun ⟨k, hk⟩ => (φ k hk).natTrans.app ⟨k, by rfl⟩ ≫
+            iter₂.F.map (homOfLE (by exact hk.le))
+          naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by
+            have hf : k₁ ≤ k₂ := by simpa using leOfHom f
+            dsimp
+            rw [comp_id, congr_app (φ k₁ hk₁) ((truncFunctor ε hf).map (φ k₂ hk₂))]
+            erw [natTrans_naturality_assoc (φ k₂ hk₂) k₁ k₂ hf (by rfl)]
+            dsimp
+            rw [← Functor.map_comp, homOfLE_comp] })
+
+lemma mkOfLimitNatTransApp_eq_of_lt (i : J) (hi : i < j) :
+    mkOfLimitNatTransApp φ i hi.le = (φ i hi).natTrans.app ⟨i, by rfl⟩ :=
+  dif_pos hi
+
+lemma mkOfLimitNatTransApp_naturality_top (i : J) (hi : i < j) :
+    iter₁.F.map (homOfLE (by simpa using hi.le) : ⟨i, hi.le⟩ ⟶ ⟨j, by rfl⟩) ≫
+      mkOfLimitNatTransApp φ j (by rfl) =
+      mkOfLimitNatTransApp φ i hi.le ≫ iter₂.F.map (homOfLE (by simpa using hi.le)) := by
+  rw [mkOfLimitNatTransApp_eq_of_lt φ i hi, mkOfLimitNatTransApp, dif_neg (by simp)]
+  exact (iter₁.isColimit j (by rfl)).fac _ ⟨i, hi⟩
+
+/-- Auxiliary definition for `mkOfLimit`. -/
+@[simps]
+def mkOfLimitNatTrans : iter₁.F ⟶ iter₂.F where
+  app := fun ⟨k, hk⟩ => mkOfLimitNatTransApp φ k hk
+  naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by
+    have hk : k₁ ≤ k₂ := leOfHom f
+    obtain h₂ | rfl := hk₂.lt_or_eq
+    · dsimp
+      rw [mkOfLimitNatTransApp_eq_of_lt _ k₂ h₂,
+        mkOfLimitNatTransApp_eq_of_lt _ k₁ (lt_of_le_of_lt hk h₂),
+        congr_app (φ k₁ (lt_of_le_of_lt hk h₂)) ((truncFunctor ε hk).map (φ k₂ h₂))]
+      exact natTrans_naturality (φ k₂ h₂) k₁ k₂ hk (by rfl)
+    · obtain h₁ | rfl := hk₁.lt_or_eq
+      · exact mkOfLimitNatTransApp_naturality_top _ _ h₁
+      · obtain rfl : f = 𝟙 _ := rfl
+        simp only [map_id, id_comp, comp_id]
+
+/-- The (unique) morphism between two objects in `Iteration ε j` when `j` is a limit element,
+assuming we have a morphism between the truncations to `Iteration ε i` for all `i < j`. -/
+def mkOfLimit : iter₁ ⟶ iter₂ where
+  natTrans := mkOfLimitNatTrans φ
+  natTrans_app_zero := by simp [mkOfLimitNatTransApp_eq_of_lt φ ⊥
+    (IsWellOrderLimitElement.bot_lt j)]
+  natTrans_app_succ i h := by
+    dsimp
+    have h' := IsWellOrderLimitElement.wellOrderSucc_lt h
+    rw [mkOfLimitNatTransApp_eq_of_lt φ _ h',
+      (φ _ h').natTrans_app_succ i (self_lt_wellOrderSucc h),
+      mkOfLimitNatTransApp_eq_of_lt φ _ h,
+      congr_app (φ i h) ((truncFunctor ε (self_le_wellOrderSucc i)).map (φ (wellOrderSucc i) h'))]
+    dsimp
+
+end
+
+instance : Nonempty (iter₁ ⟶ iter₂) := by
+  let P := fun (i : J) => ∀ (hi : i ≤ j),
+    Nonempty ((truncFunctor ε hi).obj iter₁ ⟶ (truncFunctor ε hi).obj iter₂)
+  suffices ∀ i, P i from this j (by rfl)
+  refine fun _ => WellFoundedLT.induction _ (fun i hi hi' => ?_)
+  obtain rfl | ⟨i, rfl, hi''⟩ | _ := eq_bot_or_eq_succ_or_isWellOrderLimitElement i
+  · exact ⟨Hom.mkOfBot _ _⟩
+  · exact ⟨Hom.mkOfSucc _ _ hi'' ((hi i hi'' (hi''.le.trans hi')).some)⟩
+  · exact ⟨Hom.mkOfLimit (fun k hk => (hi k hk (hk.le.trans hi')).some)⟩
+
+noncomputable instance : Unique (iter₁ ⟶ iter₂) :=
+  uniqueOfSubsingleton (Nonempty.some inferInstance)
+
 end Hom
 
+variable {j} (iter₁ iter₂ iter₃ : Iteration ε j)
+
+/-- The canonical isomorphism between two objects in the category `Iteration ε j`. -/
+noncomputable def iso : iter₁ ≅ iter₂ where
+  hom := default
+  inv := default
+
+@[simp]
+lemma iso_refl : iso iter₁ iter₁ = Iso.refl _ := by aesop_cat
+
+lemma iso_trans : iso iter₁ iter₃ = iso iter₁ iter₂ ≪≫ iso iter₂ iter₃ := by aesop_cat
+
 end Iteration
 
 end Functor

From 295d8dfd36eeeab2df30f24c50ba937a5e7a180e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 26 Oct 2024 12:04:26 +0200
Subject: [PATCH 06/28] fixes, using interval notation

---
 .../SmallObject/Iteration/Basic.lean          | 43 +++++++++++--------
 1 file changed, 24 insertions(+), 19 deletions(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index 1d311f0235677..9bcc16aca6810 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -15,7 +15,7 @@ In this file, given a functor `Φ : C ⥤ C` and a natural transformation
 
 Given `j : J` where `J` is a well ordered set, we first introduce
 a category `Iteration ε j`. An object in this category consists of
-a functor `F : { i // i ≤ j } ⥤ C ⥤ C` equipped with the data
+a functor `F : Set.Iic j ⥤ C ⥤ C` equipped with the data
 which makes it the `i`th-iteration of `Φ` for all `i` such that `i ≤ j`.
 Under suitable assumptions on `C`, we shall show that this category
 `Iteration ε j` is equivalent to the punctual category (TODO).
@@ -37,16 +37,15 @@ namespace CategoryTheory
 
 open Category Limits
 
-variable {C : Type*} [Category C] {Φ : C ⥤ C} (ε : 𝟭 C ⟶ Φ)
-  {J : Type u} [Preorder J]
+variable {C : Type*} [Category C] {Φ : C ⥤ C} (ε : 𝟭 C ⟶ Φ) {J : Type u}
 
 namespace Functor
 
 namespace Iteration
 
-variable {j : J} (F : { i // i ≤ j } ⥤ C)
+variable [Preorder J] {j : J} (F : Set.Iic j ⥤ C)
 
-/-- The map `F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩` when `F : { i // i ≤ j } ⥤ C`
+/-- The map `F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩` when `F : Set.Iic j ⥤ C`
 and `i : J` is such that `i < j`. -/
 noncomputable abbrev mapSucc' [SuccOrder J] (i : J) (hi : i < j) :
     F.obj ⟨i, hi.le⟩ ⟶ F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ :=
@@ -54,9 +53,9 @@ noncomputable abbrev mapSucc' [SuccOrder J] (i : J) (hi : i < j) :
 
 variable {i : J} (hi : i ≤ j)
 
-/-- The functor `{ k // k < i } ⥤ C` obtained by "restriction" of `F : { i // i ≤ j } ⥤ C`
+/-- The functor `Set.Iio i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C`
 when `i ≤ j`. -/
-def restrictionLT : { k // k < i } ⥤ C :=
+def restrictionLT : Set.Iio i ⥤ C :=
   (monotone_inclusion_lt_le_of_le hi).functor ⋙ F
 
 @[simp]
@@ -64,10 +63,10 @@ lemma restrictionLT_obj (k : J) (hk : k < i) :
     (restrictionLT F hi).obj ⟨k, hk⟩ = F.obj ⟨k, hk.le.trans hi⟩ := rfl
 
 @[simp]
-lemma restrictionLT_map {k₁ k₂ : { k // k < i }} (φ : k₁ ⟶ k₂) :
+lemma restrictionLT_map {k₁ k₂ : Set.Iio i} (φ : k₁ ⟶ k₂) :
     (restrictionLT F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl
 
-/-- Given `F : { i // i ≤ j } ⥤ C`, `i : J` such that `hi : i ≤ j`, this is the
+/-- Given `F : Set.Iic j ⥤ C`, `i : J` such that `hi : i ≤ j`, this is the
 cocone consisting of all maps `F.obj ⟨k, hk⟩ ⟶ F.obj ⟨i, hi⟩` for `k : J` such that `k < i`. -/
 @[simps]
 def coconeOfLE : Cocone (restrictionLT F hi) where
@@ -77,9 +76,9 @@ def coconeOfLE : Cocone (restrictionLT F hi) where
       naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ _ => by
         simp [comp_id, ← Functor.map_comp, homOfLE_comp] }
 
-/-- The functor `{ k // k ≤ i } ⥤ C` obtained by "restriction" of `F : { i // i ≤ j } ⥤ C`
+/-- The functor `Set.Iic i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C`
 when `i ≤ j`. -/
-def restrictionLE : { k | k ≤ i } ⥤ C :=
+def restrictionLE : Set.Iic i ⥤ C :=
   (monotone_inclusion_le_le_of_le hi).functor ⋙ F
 
 @[simp]
@@ -87,7 +86,7 @@ lemma restrictionLE_obj (k : J) (hk : k ≤ i) :
     (restrictionLE F hi).obj ⟨k, hk⟩ = F.obj ⟨k, hk.trans hi⟩ := rfl
 
 @[simp]
-lemma restrictionLE_map {k₁ k₂ : { k | k ≤ i }} (φ : k₁ ⟶ k₂) :
+lemma restrictionLE_map {k₁ k₂ : Set.Iic i} (φ : k₁ ⟶ k₂) :
     (restrictionLE F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl
 
 end Iteration
@@ -99,7 +98,7 @@ equipped with data and properties which characterizes the iterations up to a uni
 isomorphism for the three types of elements: `⊥`, successors, limit elements. -/
 structure Iteration [Preorder J] [OrderBot J] [SuccOrder J] (j : J) where
   /-- The data of all `i`th iterations for `i : J` such that `i ≤ j`. -/
-  F : { i // i ≤ j } ⥤ C ⥤ C
+  F : Set.Iic j ⥤ C ⥤ C
   /-- The zeroth iteration is the identity functor. -/
   isoZero : F.obj ⟨⊥, bot_le⟩ ≅ 𝟭 C
   /-- The iteration on a successor element is obtained by composition of
@@ -120,7 +119,7 @@ variable {j : J}
 
 section
 
-variable [OrderBot J] [SuccOrder J] (iter : Φ.Iteration ε j)
+variable [Preorder J] [OrderBot J] [SuccOrder J] (iter : Φ.Iteration ε j)
 
 /-- For `iter : Φ.Iteration.ε j`, this is the map
 `iter.F.obj ⟨i, _⟩ ⟶ iter.F.obj ⟨Order.succ i, _⟩` if `i : J` is such that `i < j`. -/
@@ -134,7 +133,9 @@ lemma mapSucc_eq (i : J) (hi : i < j) :
 
 end
 
-variable [OrderBot J] [SuccOrder J] (iter₁ iter₂ : Φ.Iteration ε j)
+section
+
+variable [Preorder J] [OrderBot J] [SuccOrder J] (iter₁ iter₂ : Φ.Iteration ε j)
 
 /-- A morphism between two objects `iter₁` and `iter₂` in the
 category `Φ.Iteration ε j` of `j`th iterations of a functor `Φ`
@@ -194,14 +195,13 @@ instance {J} {j : J} [PartialOrder J] [OrderBot J] [WellFoundedLT J] [SuccOrder
     intro i
     induction i using SuccOrder.limitRecOn with
     | hm j H =>
-      have := H.eq_bot
-      subst this
+      obtain rfl := H.eq_bot
       simp [natTrans_app_zero]
     | hs j H IH =>
       intro hj
       simp [Hom.natTrans_app_succ, IH, (Order.lt_succ_of_not_isMax H).trans_le hj]
     | hl j H IH =>
-      apply fun hj ↦ (iter₁.isColimit j H hj).hom_ext ?_
+      refine fun hj ↦ (iter₁.isColimit j H hj).hom_ext ?_
       rintro ⟨k, hk⟩
       simp [IH k hk]
 
@@ -237,7 +237,7 @@ def trunc (iter : Iteration ε j) {i : J} (hi : i ≤ j) : Iteration ε i where
   isoZero := iter.isoZero
   isoSucc k hk := iter.isoSucc k (lt_of_lt_of_le hk hi)
   mapSucc'_eq k hk := iter.mapSucc'_eq k (lt_of_lt_of_le hk hi)
-  isColimit k _ hk := iter.isColimit k (hk.trans hi)
+  isColimit k hk' hk := iter.isColimit k hk' (hk.trans hi)
 
 variable (ε) in
 /-- The truncation functor `Iteration ε j ⥤ Iteration ε i` when `i ≤ j`. -/
@@ -254,8 +254,13 @@ lemma truncFunctor_map_natTrans_app
     ((truncFunctor ε hi).map φ).natTrans.app ⟨k, hk⟩ =
       φ.natTrans.app ⟨k, hk.trans hi⟩ := rfl
 
+end
+
 namespace Hom
 
+variable [PartialOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J]
+  (iter₁ iter₂ : Φ.Iteration ε j)
+
 lemma congr_app (φ φ' : iter₁ ⟶ iter₂) (i : J) (hi : i ≤ j) :
     φ.natTrans.app ⟨i, hi⟩ = φ'.natTrans.app ⟨i, hi⟩ := by
   obtain rfl := Subsingleton.elim φ φ'

From 26405bdd6db4550a1b72ac127ce18010a17052a5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 26 Oct 2024 12:24:46 +0200
Subject: [PATCH 07/28] fix

---
 .../SmallObject/Iteration/UniqueHom.lean      | 66 ++++++++++---------
 1 file changed, 35 insertions(+), 31 deletions(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
index 76df8a73ea5a3..7cde80e52abe3 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
@@ -22,7 +22,7 @@ namespace CategoryTheory
 open Category Limits
 
 variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ}
-  {J : Type u} [LinearOrder J]
+  {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J]
 
 namespace Functor
 
@@ -30,7 +30,7 @@ namespace Iteration
 
 namespace Hom
 
-variable [IsWellOrder J (· < ·)] [OrderBot J] (j : J)
+variable (j : J)
 
 /-- The (unique) morphism between two objects in `Iteration ε ⊥` -/
 def mkOfBot (iter₁ iter₂ : Iteration ε (⊥ : J)) : iter₁ ⟶ iter₂ where
@@ -46,32 +46,35 @@ def mkOfBot (iter₁ iter₂ : Iteration ε (⊥ : J)) : iter₁ ⟶ iter₂ whe
 
 section
 
-variable {i : J} {iter₁ iter₂ : Iteration ε (wellOrderSucc i)}
-  (hi : i < wellOrderSucc i) (φ : iter₁.trunc hi.le ⟶ iter₂.trunc hi.le)
+variable {i : J} {iter₁ iter₂ : Iteration ε (Order.succ i)}
+  (hi : ¬IsMax i) (φ : iter₁.trunc (SuccOrder.le_succ i) ⟶ iter₂.trunc (SuccOrder.le_succ i))
 
 /-- Auxiliary definition for `mkOfSucc`. -/
-noncomputable def mkOfSuccNatTransApp (k : J) (hk : k ≤ wellOrderSucc i) :
-    iter₁.F.obj ⟨k, hk⟩ ⟶ iter₂.F.obj ⟨k, hk⟩ :=
-  if hk' : k = wellOrderSucc i then
-    eqToHom (by subst hk'; rfl) ≫ (iter₁.isoSucc i hi).hom ≫
-      whiskerRight (φ.natTrans.app ⟨i, by rfl⟩) _ ≫ (iter₂.isoSucc i hi).inv ≫
+noncomputable def mkOfSuccNatTransApp (k : J) (hk : k ≤ Order.succ i) :
+    iter₁.F.obj ⟨k, hk⟩ ⟶ iter₂.F.obj ⟨k, hk⟩ := by
+  classical
+  exact if hk' : k = Order.succ i then
+    eqToHom (by subst hk'; rfl) ≫ (iter₁.isoSucc i (Order.lt_succ_of_not_isMax hi)).hom ≫
+      whiskerRight (φ.natTrans.app ⟨i, by simp⟩) _ ≫
+      (iter₂.isoSucc i (Order.lt_succ_of_not_isMax hi)).inv ≫
       eqToHom (by subst hk'; rfl)
   else
-    φ.natTrans.app ⟨k, le_of_lt_wellOrderSucc (by
-      obtain hk|rfl := hk.lt_or_eq
+    φ.natTrans.app ⟨k, Order.le_of_lt_succ (by
+      obtain hk | rfl := hk.lt_or_eq
       · exact hk
       · tauto)⟩
 
 lemma mkOfSuccNatTransApp_eq_of_le (k : J) (hk : k ≤ i) :
-    mkOfSuccNatTransApp hi φ k (hk.trans (self_le_wellOrderSucc i)) =
+    mkOfSuccNatTransApp hi φ k (hk.trans (Order.le_succ i)) =
       φ.natTrans.app ⟨k, hk⟩ :=
-  dif_neg (by rintro rfl; simpa using lt_of_le_of_lt hk hi)
+  dif_neg (by rintro rfl; simpa using lt_of_le_of_lt hk (Order.lt_succ_of_not_isMax hi))
 
 @[simp]
-lemma mkOfSuccNatTransApp_wellOrderSucc_eq :
-    mkOfSuccNatTransApp hi φ (wellOrderSucc i) (by rfl) =
-      (iter₁.isoSucc i hi).hom ≫ whiskerRight (φ.natTrans.app ⟨i, by rfl⟩) _ ≫
-        (iter₂.isoSucc i hi).inv := by
+lemma mkOfSuccNatTransApp_succ_eq :
+    mkOfSuccNatTransApp hi φ (Order.succ i) (by rfl) =
+      (iter₁.isoSucc i (Order.lt_succ_of_not_isMax hi)).hom ≫
+        whiskerRight (φ.natTrans.app ⟨i, by simp⟩) _ ≫
+        (iter₂.isoSucc i (Order.lt_succ_of_not_isMax hi)).inv := by
   dsimp [mkOfSuccNatTransApp]
   rw [dif_pos rfl, comp_id, id_comp]
 
@@ -84,24 +87,25 @@ noncomputable def mkOfSuccNatTrans :
     dsimp
     have hk : k₁ ≤ k₂ := leOfHom f
     obtain h₂ | rfl := hk₂.lt_or_eq
-    · replace h₂ : k₂ ≤ i := le_of_lt_wellOrderSucc h₂
+    · replace h₂ : k₂ ≤ i := Order.le_of_lt_succ h₂
       rw [mkOfSuccNatTransApp_eq_of_le hi φ k₂ h₂,
         mkOfSuccNatTransApp_eq_of_le hi φ k₁ (hk.trans h₂)]
       exact natTrans_naturality φ k₁ k₂ hk h₂
     · obtain h₁ | rfl := hk.lt_or_eq
-      · have h₂ : k₁ ≤ i := le_of_lt_wellOrderSucc h₁
-        let f₁ : (⟨k₁, hk⟩ : { l | l ≤ wellOrderSucc i}) ⟶
-          ⟨i, self_le_wellOrderSucc i⟩ := homOfLE h₂
-        let f₂ : (⟨i, self_le_wellOrderSucc i⟩ : { l | l ≤ wellOrderSucc i}) ⟶
-          ⟨wellOrderSucc i, by dsimp; rfl⟩ := homOfLE (self_le_wellOrderSucc i)
+      · have h₂ : k₁ ≤ i := Order.le_of_lt_succ h₁
+        let f₁ : (⟨k₁, hk⟩ : { l | l ≤ Order.succ i}) ⟶
+          ⟨i, Order.le_succ i⟩ := homOfLE h₂
+        let f₂ : (⟨i, Order.le_succ i⟩ : Set.Iic (Order.succ i)) ⟶
+          ⟨Order.succ i, by simp⟩ := homOfLE (Order.le_succ i)
         obtain rfl : f = f₁ ≫ f₂ := rfl
         rw [Functor.map_comp, Functor.map_comp, assoc,
           mkOfSuccNatTransApp_eq_of_le hi φ k₁ h₂]
         erw [← natTrans_naturality_assoc φ k₁ i h₂ (by rfl)]
-        rw [mkOfSuccNatTransApp_wellOrderSucc_eq]
+        rw [mkOfSuccNatTransApp_succ_eq]
         dsimp
-        change _ ≫ iter₁.mapSucc i hi ≫ _ = _ ≫ _ ≫ iter₂.mapSucc i hi
-        rw [iter₁.mapSucc_eq i hi, iter₂.mapSucc_eq i hi, assoc,
+        change _ ≫ iter₁.mapSucc i (Order.lt_succ_of_not_isMax hi) ≫ _ =
+          _ ≫ _ ≫ iter₂.mapSucc i (Order.lt_succ_of_not_isMax hi)
+        rw [iter₁.mapSucc_eq i, iter₂.mapSucc_eq i, assoc,
           Iso.inv_hom_id_assoc]
         ext X
         dsimp
@@ -112,11 +116,11 @@ noncomputable def mkOfSuccNatTrans :
 
 end
 
-/-- The (unique) morphism between two objects in `Iteration ε (wellOrderSucc i)`,
+/-- The (unique) morphism between two objects in `Iteration ε (Order.succ i)`,
 assuming we have a morphism between the truncations to `Iteration ε i`. -/
 noncomputable def mkOfSucc
-    {i : J} (iter₁ iter₂ : Iteration ε (wellOrderSucc i)) (hi : i < wellOrderSucc i)
-    (φ : iter₁.trunc hi.le ⟶ iter₂.trunc hi.le) :
+    {i : J} (iter₁ iter₂ : Iteration ε (Order.succ i)) (hi : ¬IsMax i)
+    (φ : iter₁.trunc (SuccOrder.le_succ i) ⟶ iter₂.trunc (SuccOrder.le_succ i)) :
     iter₁ ⟶ iter₂ where
   natTrans := mkOfSuccNatTrans hi φ
   natTrans_app_zero := by
@@ -124,10 +128,10 @@ noncomputable def mkOfSucc
     rw [mkOfSuccNatTransApp_eq_of_le _ _ _ bot_le, φ.natTrans_app_zero]
     rfl
   natTrans_app_succ k hk := by
-    obtain hk' | rfl := (le_of_lt_wellOrderSucc hk).lt_or_eq
+    obtain hk' | rfl := (Order.le_of_lt_succ hk).lt_or_eq
     · dsimp
       rw [mkOfSuccNatTransApp_eq_of_le hi φ k hk'.le,
-        mkOfSuccNatTransApp_eq_of_le hi φ (wellOrderSucc k) (wellOrderSucc_le hk'),
+        mkOfSuccNatTransApp_eq_of_le hi φ (Order.succ k) (Order.succ_le_of_lt hk'),
         φ.natTrans_app_succ _ hk']
       rfl
     · simp [mkOfSuccNatTransApp_eq_of_le hi φ k (by rfl)]

From ecdbc603b0f0df74a9689c10d12258b176f6734a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Sun, 27 Oct 2024 22:38:22 +0100
Subject: [PATCH 08/28] Update
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
---
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index 88410b01649dd..d739917e114af 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -233,7 +233,7 @@ def eval {i : J} (hi : i ≤ j) : Iteration ε j ⥤ C ⥤ C where
 induced element in `Iteration ε i`. -/
 @[simps F isoZero isoSucc]
 def trunc (iter : Iteration ε j) {i : J} (hi : i ≤ j) : Iteration ε i where
-  F := restrictionLE (iter.F) hi
+  F := restrictionLE iter.F hi
   isoZero := iter.isoZero
   isoSucc k hk := iter.isoSucc k (lt_of_lt_of_le hk hi)
   mapSucc'_eq k hk := iter.mapSucc'_eq k (lt_of_lt_of_le hk hi)

From 64c0674e80e9c867d538bd7d9638f0e01a06a087 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 27 Oct 2024 22:58:54 +0100
Subject: [PATCH 09/28] fix

---
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean     | 2 +-
 Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean | 5 ++---
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index 05e609b4c2d32..73fbd53ce849c 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -233,7 +233,7 @@ def eval {i : J} (hi : i ≤ j) : Iteration ε j ⥤ C ⥤ C where
 induced element in `Iteration ε i`. -/
 @[simps F isoZero isoSucc]
 def trunc (iter : Iteration ε j) {i : J} (hi : i ≤ j) : Iteration ε i where
-  F := restrictionLE (iter.F) hi
+  F := restrictionLE iter.F hi
   isoZero := iter.isoZero
   isoSucc k hk := iter.isoSucc k (lt_of_lt_of_le hk hi)
   mapSucc'_eq k hk := iter.mapSucc'_eq k (lt_of_lt_of_le hk hi)
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
index 7cde80e52abe3..203752bd83237 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
@@ -51,9 +51,8 @@ variable {i : J} {iter₁ iter₂ : Iteration ε (Order.succ i)}
 
 /-- Auxiliary definition for `mkOfSucc`. -/
 noncomputable def mkOfSuccNatTransApp (k : J) (hk : k ≤ Order.succ i) :
-    iter₁.F.obj ⟨k, hk⟩ ⟶ iter₂.F.obj ⟨k, hk⟩ := by
-  classical
-  exact if hk' : k = Order.succ i then
+    iter₁.F.obj ⟨k, hk⟩ ⟶ iter₂.F.obj ⟨k, hk⟩ :=
+  if hk' : k = Order.succ i then
     eqToHom (by subst hk'; rfl) ≫ (iter₁.isoSucc i (Order.lt_succ_of_not_isMax hi)).hom ≫
       whiskerRight (φ.natTrans.app ⟨i, by simp⟩) _ ≫
       (iter₂.isoSucc i (Order.lt_succ_of_not_isMax hi)).inv ≫

From 6d4fc10fc4d341f84b84c01a44d5fe67ec85f262 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sun, 27 Oct 2024 22:59:08 +0100
Subject: [PATCH 10/28] fix

---
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index 73fbd53ce849c..d739917e114af 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -259,7 +259,7 @@ end
 namespace Hom
 
 variable [PartialOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J]
-  (iter₁ iter₂ : Φ.Iteration ε j)
+  {iter₁ iter₂ : Φ.Iteration ε j}
 
 lemma congr_app (φ φ' : iter₁ ⟶ iter₂) (i : J) (hi : i ≤ j) :
     φ.natTrans.app ⟨i, hi⟩ = φ'.natTrans.app ⟨i, hi⟩ := by

From f8a7628e06bf7289a28b0357aab1a702c36c9b30 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 12 Nov 2024 17:18:45 +0100
Subject: [PATCH 11/28] s/refine/exact/

---
 Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
index 4fba898fe5eff..5e804f4b55103 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
@@ -219,7 +219,7 @@ instance : Nonempty (iter₁ ⟶ iter₂) := by
   induction i using SuccOrder.limitRecOn with
   | hm i hi =>
     obtain rfl : i = ⊥ := by simpa using hi
-    refine fun hi' ↦ ⟨Hom.mkOfBot _ _⟩
+    exact fun hi' ↦ ⟨Hom.mkOfBot _ _⟩
   | hs i hi hi' =>
     exact fun hi'' ↦ ⟨Hom.mkOfSucc _ _ hi (hi' ((Order.le_succ i).trans hi'')).some⟩
   | hl i hi hi' =>

From 3398597efe63e423840d71ac11d4e0a5b7881e80 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 14 Nov 2024 19:57:05 +0100
Subject: [PATCH 12/28] wip

---
 Mathlib.lean                                  |   1 +
 .../SmallObject/Iteration/Nonempty.lean       | 195 ++++++++++++++++++
 2 files changed, 196 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 11ce7834660b5..e74ca61c24843 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2043,6 +2043,7 @@ import Mathlib.CategoryTheory.Sites.Whiskering
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.SmallObject.Construction
 import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
+import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
 import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 import Mathlib.CategoryTheory.Square
 import Mathlib.CategoryTheory.Subobject.Basic
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
new file mode 100644
index 0000000000000..67772bfefc01e
--- /dev/null
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
@@ -0,0 +1,195 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
+
+/-!
+# Existence of objects in the category of iterations of functors
+
+Given a functor `Φ : C ⥤ C` and a natural transformation `ε : 𝟭 C ⟶ Φ`,
+we shall show in this file that for any well ordered set `J`,
+and `j : J`, the category `Functor.Iteration ε j` is nonempty.
+
+-/
+
+universe u
+
+section
+
+namespace CategoryTheory
+
+open Category
+
+namespace Functor
+
+variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ}
+  {J : Type u} [LinearOrder J] [SuccOrder J]
+
+variable {j : J} (hj : ¬IsMax j) (F : Set.Iic j ⥤ C) {X : C}
+  (τ : F.obj ⟨j, by simp⟩ ⟶ X)
+
+namespace extendToSucc
+
+variable (X)
+
+def obj (i : Set.Iic (Order.succ j)) : C :=
+  if hij : i.1 ≤ j then F.obj ⟨i.1, hij⟩ else X
+
+def objIso (i : Set.Iic j) :
+    obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i := eqToIso (dif_pos i.2)
+
+def objSuccIso :
+    obj F X ⟨Order.succ j, by simp⟩ ≅ X :=
+  eqToIso (dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj))
+
+variable {X}
+
+def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ Order.succ j) :
+    obj F X ⟨i₁, hi.trans hi₂⟩ ⟶ obj F X ⟨i₂, hi₂⟩ :=
+  if h₁ : i₂ ≤ j then
+    (objIso F X ⟨i₁, hi.trans h₁⟩).hom ≫ F.map (homOfLE hi) ≫ (objIso F X ⟨i₂, h₁⟩).inv
+  else
+    if h₂ : i₁ ≤ j then
+      (objIso F X ⟨i₁, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫
+        (objSuccIso hj F X).inv ≫ eqToHom (by
+          congr
+          exact le_antisymm (Order.succ_le_of_lt (not_le.1 h₁)) hi₂)
+    else
+      eqToHom (by
+        congr
+        rw [le_antisymm hi₂ (Order.succ_le_of_lt (not_le.1 h₁)),
+          le_antisymm (hi.trans hi₂) (Order.succ_le_of_lt (not_le.1 h₂))])
+
+lemma map_eq (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
+    map hj F τ i₁ i₂ hi (hi₂.trans (Order.le_succ j)) =
+      (objIso F X ⟨i₁, hi.trans hi₂⟩).hom ≫ F.map (homOfLE hi) ≫
+        (objIso F X ⟨i₂, hi₂⟩).inv :=
+  dif_pos hi₂
+
+lemma map_self_succ :
+    map hj F τ j (Order.succ j) (Order.le_succ j) (by rfl) =
+      (objIso F X ⟨j, by simp⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv := by
+  dsimp [map]
+  rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
+    dif_pos (by rfl), map_id, comp_id, id_comp]
+
+@[simp]
+lemma map_id (i : J) (hi : i ≤ Order.succ j) :
+    map hj F τ i i (by rfl) hi = 𝟙 _ := by
+  dsimp [map]
+  by_cases h₁ : i ≤ j
+  · rw [dif_pos h₁, CategoryTheory.Functor.map_id, id_comp, Iso.hom_inv_id]
+  · obtain rfl : i = Order.succ j := le_antisymm hi (Order.succ_le_of_lt (not_le.1 h₁))
+    rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
+      dif_neg h₁]
+
+lemma map_comp (i₁ i₂ i₃ : J) (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) (h : i₃ ≤ Order.succ j) :
+    map hj F τ i₁ i₃ (h₁₂.trans h₂₃) h =
+      map hj F τ i₁ i₂ h₁₂ (h₂₃.trans h) ≫ map hj F τ i₂ i₃ h₂₃ h := by
+  by_cases h₁ : i₃ ≤ j
+  · rw [map_eq hj F τ i₁ i₂ _ (h₂₃.trans h₁), map_eq hj F τ i₂ i₃ _ h₁,
+      map_eq hj F τ i₁ i₃ _ h₁, assoc, assoc, Iso.inv_hom_id_assoc, ← map_comp_assoc,
+      homOfLE_comp]
+  · obtain rfl : i₃ = Order.succ j := le_antisymm h (Order.succ_le_of_lt (not_le.1 h₁))
+    obtain h₂ | rfl := h₂₃.lt_or_eq
+    · rw [Order.lt_succ_iff_of_not_isMax hj] at h₂
+      rw [map_eq hj F τ i₁ i₂ _ h₂]
+      dsimp [map]
+      rw [dif_neg h₁, dif_pos (h₁₂.trans h₂), dif_neg h₁, dif_pos h₂,
+        assoc, assoc, Iso.inv_hom_id_assoc,comp_id, ← map_comp_assoc, homOfLE_comp]
+    · rw [map_id, comp_id]
+
+end extendToSucc
+
+open extendToSucc in
+include hj in
+def extendToSucc : Set.Iic (Order.succ j) ⥤ C where
+  obj := obj F X
+  map {i₁ i₂} f := map hj F τ i₁ i₂ (leOfHom f) i₂.2
+  map_id _ := extendToSucc.map_id _ F τ _ _
+  map_comp {i₁ i₂ i₃} f g := extendToSucc.map_comp hj F τ i₁ i₂ i₃ (leOfHom f) (leOfHom g) i₃.2
+
+def extendToSuccObjIso (i : Set.Iic j) :
+    (extendToSucc hj F τ).obj ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i :=
+  extendToSucc.objIso F X i
+
+def extendToSuccObjSuccIso :
+    (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ ≅ X :=
+  extendToSucc.objSuccIso hj F X
+
+def extendToSuccRestrictionLEIso :
+    Iteration.restrictionLE (extendToSucc hj F τ) (Order.le_succ j) ≅ F :=
+  NatIso.ofComponents (extendToSuccObjIso hj F τ) (by
+    rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f
+    simp only [Set.mem_Iic] at h₁ h₂
+    dsimp [extendToSucc, extendToSuccObjIso]
+    rw [extendToSucc.map_eq _ _ _ _ _ _ h₂, assoc, assoc, Iso.inv_hom_id, comp_id]
+    rfl)
+
+lemma extendToSucc_map_le_succ :
+    (extendToSucc hj F τ).map (homOfLE (Order.le_succ j)) =
+        (extendToSuccObjIso hj F τ ⟨j, by simp⟩).hom ≫ τ ≫
+          (extendToSuccObjSuccIso hj F τ).inv :=
+  extendToSucc.map_self_succ _ _ _
+
+end Functor
+
+end CategoryTheory
+
+end
+
+namespace CategoryTheory
+
+variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ}
+  {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J]
+
+namespace Functor
+
+namespace Iteration
+
+variable (ε J) in
+/-- The obvious term in `Iteration ε ⊥`: it is given by the identity functor. -/
+def mkOfBot : Iteration ε (⊥ : J) where
+  F := (Functor.const _).obj (𝟭 C)
+  isoZero := Iso.refl _
+  isoSucc _ h := by simp at h
+  mapSucc'_eq _ h := by simp at h
+  isColimit x hx h := by
+    exfalso
+    refine hx.not_isMin (by simpa using h)
+
+namespace mkOfSucc
+
+variable {j : J} (hj : ¬IsMax j) (iter : Iteration ε j)
+
+/-- Auxiliary definition for `Functor.Iteration.mkOfSucc`. -/
+def isoSucc (i : J) (hi : i < Order.succ j) :
+    (extendToSucc hj iter.F (whiskerLeft _ ε)).obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ ≅
+      (extendToSucc hj iter.F (whiskerLeft _ ε)).obj ⟨i, hi.le⟩ ⋙ Φ :=
+  if hij : i < j then
+    extendToSuccObjIso _ _ _ ⟨Order.succ i, Order.succ_le_of_lt hij⟩ ≪≫
+      iter.isoSucc i hij ≪≫ (isoWhiskerRight (extendToSuccObjIso _ _ _ ⟨i, hij.le⟩).symm _)
+  else
+    have hij' : i = j := le_antisymm
+      (by simpa only [Order.lt_succ_iff_of_not_isMax hj] using hi) (by simpa using hij)
+    eqToIso (by subst hij'; rfl) ≪≫ extendToSuccObjSuccIso hj iter.F (whiskerLeft _ ε) ≪≫
+      isoWhiskerRight ((extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨j, by simp⟩).symm.trans
+          (eqToIso (by subst hij'; rfl))) _
+
+end mkOfSucc
+
+noncomputable def mkOfSucc {j : J} (hj : ¬IsMax j) (iter : Iteration ε j) :
+    Iteration ε (Order.succ j) where
+  F := extendToSucc hj iter.F (whiskerLeft _ ε)
+  isoZero := (extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨⊥, by simp⟩).trans iter.isoZero
+  isoSucc i hi := mkOfSucc.isoSucc hj iter i hi
+  mapSucc'_eq := sorry
+  isColimit := sorry
+
+end Iteration
+
+end Functor
+
+end CategoryTheory

From 95f531052a60896b02c40cc71a8c05fb2c4986ae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 19 Nov 2024 19:47:25 +0100
Subject: [PATCH 13/28] cleaning up

---
 Mathlib.lean                                  |   1 +
 .../SmallObject/Iteration/ExtendToSucc.lean   | 161 +++++++++++++++
 .../SmallObject/Iteration/Nonempty.lean       | 195 +++++-------------
 3 files changed, 211 insertions(+), 146 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 710e12041ad16..ec249d4f1b97e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2079,6 +2079,7 @@ import Mathlib.CategoryTheory.Sites.Whiskering
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.SmallObject.Construction
 import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
+import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
 import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
 import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 import Mathlib.CategoryTheory.Square
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
new file mode 100644
index 0000000000000..166469022df52
--- /dev/null
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
@@ -0,0 +1,161 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
+
+/-!
+# Extension of a functor from `Set.Iic j` to `Set.Iic (Order.succ j)`
+
+Given a linearly ordered type `J` with `SuccOrder J`, `j : J` that is not maximal,
+we define the extension of a functor `F : Set.Iic j ⥤ C` as a
+functor `Set.Iic (Order.succ j) ⥤ C` when an object `X : C` and a morphism
+`τ : F.obj ⟨j, _⟩ ⟶ X` is given.
+
+-/
+
+universe u
+
+namespace CategoryTheory
+
+open Category
+
+namespace Functor
+
+variable {C : Type*} [Category C]
+  {J : Type u} [LinearOrder J] [SuccOrder J] {j : J} (hj : ¬IsMax j)
+  (F : Set.Iic j ⥤ C) {X : C} (τ : F.obj ⟨j, by simp⟩ ⟶ X)
+
+namespace extendToSucc
+
+variable (X)
+
+/-- `extendToSucc`, on objects: it coincides with `F.obj` for `i ≤ j`, and
+it sends `Order.succ j` to the given object `X`. -/
+def obj (i : Set.Iic (Order.succ j)) : C :=
+  if hij : i.1 ≤ j then F.obj ⟨i.1, hij⟩ else X
+
+/-- The isomorphism `obj F X ⟨i, _⟩ ≅ F.obj i` when `i : Set.Iic j`. -/
+def objIso (i : Set.Iic j) :
+    obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i := eqToIso (dif_pos i.2)
+
+/-- The isomorphism `obj F X ⟨Order.succ j, _⟩ ≅ X`. -/
+def objSuccIso :
+    obj F X ⟨Order.succ j, by simp⟩ ≅ X :=
+  eqToIso (dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj))
+
+variable {X}
+
+/-- `extendToSucc`, on morphisms. -/
+def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ Order.succ j) :
+    obj F X ⟨i₁, hi.trans hi₂⟩ ⟶ obj F X ⟨i₂, hi₂⟩ :=
+  if h₁ : i₂ ≤ j then
+    (objIso F X ⟨i₁, hi.trans h₁⟩).hom ≫ F.map (homOfLE hi) ≫ (objIso F X ⟨i₂, h₁⟩).inv
+  else
+    if h₂ : i₁ ≤ j then
+      (objIso F X ⟨i₁, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫
+        (objSuccIso hj F X).inv ≫ eqToHom (by
+          congr
+          exact le_antisymm (Order.succ_le_of_lt (not_le.1 h₁)) hi₂)
+    else
+      eqToHom (by
+        congr
+        rw [le_antisymm hi₂ (Order.succ_le_of_lt (not_le.1 h₁)),
+          le_antisymm (hi.trans hi₂) (Order.succ_le_of_lt (not_le.1 h₂))])
+
+lemma map_eq (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
+    map hj F τ i₁ i₂ hi (hi₂.trans (Order.le_succ j)) =
+      (objIso F X ⟨i₁, hi.trans hi₂⟩).hom ≫ F.map (homOfLE hi) ≫
+        (objIso F X ⟨i₂, hi₂⟩).inv :=
+  dif_pos hi₂
+
+lemma map_self_succ :
+    map hj F τ j (Order.succ j) (Order.le_succ j) (by rfl) =
+      (objIso F X ⟨j, by simp⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv := by
+  dsimp [map]
+  rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
+    dif_pos (by rfl), map_id, comp_id, id_comp]
+
+@[simp]
+lemma map_id (i : J) (hi : i ≤ Order.succ j) :
+    map hj F τ i i (by rfl) hi = 𝟙 _ := by
+  dsimp [map]
+  by_cases h₁ : i ≤ j
+  · rw [dif_pos h₁, CategoryTheory.Functor.map_id, id_comp, Iso.hom_inv_id]
+  · obtain rfl : i = Order.succ j := le_antisymm hi (Order.succ_le_of_lt (not_le.1 h₁))
+    rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
+      dif_neg h₁]
+
+lemma map_comp (i₁ i₂ i₃ : J) (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) (h : i₃ ≤ Order.succ j) :
+    map hj F τ i₁ i₃ (h₁₂.trans h₂₃) h =
+      map hj F τ i₁ i₂ h₁₂ (h₂₃.trans h) ≫ map hj F τ i₂ i₃ h₂₃ h := by
+  by_cases h₁ : i₃ ≤ j
+  · rw [map_eq hj F τ i₁ i₂ _ (h₂₃.trans h₁), map_eq hj F τ i₂ i₃ _ h₁,
+      map_eq hj F τ i₁ i₃ _ h₁, assoc, assoc, Iso.inv_hom_id_assoc, ← map_comp_assoc,
+      homOfLE_comp]
+  · obtain rfl : i₃ = Order.succ j := le_antisymm h (Order.succ_le_of_lt (not_le.1 h₁))
+    obtain h₂ | rfl := h₂₃.lt_or_eq
+    · rw [Order.lt_succ_iff_of_not_isMax hj] at h₂
+      rw [map_eq hj F τ i₁ i₂ _ h₂]
+      dsimp [map]
+      rw [dif_neg h₁, dif_pos (h₁₂.trans h₂), dif_neg h₁, dif_pos h₂,
+        assoc, assoc, Iso.inv_hom_id_assoc,comp_id, ← map_comp_assoc, homOfLE_comp]
+    · rw [map_id, comp_id]
+
+end extendToSucc
+
+open extendToSucc in
+include hj in
+/-- The extension to `Set.Iic (Order.succ j) ⥤ C` of a functor `F : Set.Iic j ⥤ C`,
+when we specify a morphism `F.obj ⟨j, _⟩ ⟶ X`. -/
+def extendToSucc : Set.Iic (Order.succ j) ⥤ C where
+  obj := obj F X
+  map {i₁ i₂} f := map hj F τ i₁ i₂ (leOfHom f) i₂.2
+  map_id _ := extendToSucc.map_id _ F τ _ _
+  map_comp {i₁ i₂ i₃} f g := extendToSucc.map_comp hj F τ i₁ i₂ i₃ (leOfHom f) (leOfHom g) i₃.2
+
+/-- The isomorphism `(extendToSucc hj F τ).obj ⟨i, _⟩ ≅ F.obj i` when `i : Set.Iic j` -/
+def extendToSuccObjIso (i : Set.Iic j) :
+    (extendToSucc hj F τ).obj ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i :=
+  extendToSucc.objIso F X i
+
+/-- The isomorphism `(extendToSucc hj F τ).obj ⟨Order.succ j, _⟩ ≅ X`. -/
+def extendToSuccObjSuccIso :
+    (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ ≅ X :=
+  extendToSucc.objSuccIso hj F X
+
+@[reassoc]
+lemma extendToSuccObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
+    (extendToSucc hj F τ).map (homOfLE hi :
+      ⟨i₁, hi.trans (hi₂.trans (Order.le_succ j))⟩ ⟶ ⟨i₂, hi₂.trans (Order.le_succ j)⟩) ≫
+    (extendToSuccObjIso hj F τ ⟨i₂, hi₂⟩).hom =
+      (extendToSuccObjIso hj F τ ⟨i₁, hi.trans hi₂⟩).hom ≫ F.map (homOfLE hi) := by
+  dsimp [extendToSucc, extendToSuccObjIso]
+  rw [extendToSucc.map_eq _ _ _ _ _ _ hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]
+
+/-- The isomorphism expressing that `extendToSucc hj F τ` extends `F`. -/
+@[simps!]
+def extendToSuccRestrictionLEIso :
+    Iteration.restrictionLE (extendToSucc hj F τ) (Order.le_succ j) ≅ F :=
+  NatIso.ofComponents (extendToSuccObjIso hj F τ) (by
+    rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f
+    apply extendToSuccObjIso_hom_naturality)
+
+lemma extentToSucc_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
+    (extendToSucc hj F τ).map (homOfLE hi :
+      ⟨i₁, hi.trans (hi₂.trans (Order.le_succ j))⟩ ⟶ ⟨i₂, hi₂.trans (Order.le_succ j)⟩) =
+      (extendToSuccObjIso hj F τ ⟨i₁, hi.trans hi₂⟩).hom ≫ F.map (homOfLE hi) ≫
+      (extendToSuccObjIso hj F τ ⟨i₂, hi₂⟩).inv := by
+  rw [← extendToSuccObjIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]
+
+lemma extendToSucc_map_le_succ :
+    (extendToSucc hj F τ).map (homOfLE (Order.le_succ j)) =
+        (extendToSuccObjIso hj F τ ⟨j, by simp⟩).hom ≫ τ ≫
+          (extendToSuccObjSuccIso hj F τ).inv :=
+  extendToSucc.map_self_succ _ _ _
+
+end Functor
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
index 67772bfefc01e..5c792d72b67b7 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
+import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
 
 /-!
 # Existence of objects in the category of iterations of functors
@@ -11,136 +12,18 @@ import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 Given a functor `Φ : C ⥤ C` and a natural transformation `ε : 𝟭 C ⟶ Φ`,
 we shall show in this file that for any well ordered set `J`,
 and `j : J`, the category `Functor.Iteration ε j` is nonempty.
+As we already know from the main result in `SmallObject.Iteration.UniqueHom`
+that such objects, if they exists, are unique up to a unique isomorphism,
+we shall show the existence of a term in `Functor.Iteration ε j` by
+transfinite induction.
 
 -/
 
 universe u
 
-section
-
 namespace CategoryTheory
 
-open Category
-
-namespace Functor
-
-variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ}
-  {J : Type u} [LinearOrder J] [SuccOrder J]
-
-variable {j : J} (hj : ¬IsMax j) (F : Set.Iic j ⥤ C) {X : C}
-  (τ : F.obj ⟨j, by simp⟩ ⟶ X)
-
-namespace extendToSucc
-
-variable (X)
-
-def obj (i : Set.Iic (Order.succ j)) : C :=
-  if hij : i.1 ≤ j then F.obj ⟨i.1, hij⟩ else X
-
-def objIso (i : Set.Iic j) :
-    obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i := eqToIso (dif_pos i.2)
-
-def objSuccIso :
-    obj F X ⟨Order.succ j, by simp⟩ ≅ X :=
-  eqToIso (dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj))
-
-variable {X}
-
-def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ Order.succ j) :
-    obj F X ⟨i₁, hi.trans hi₂⟩ ⟶ obj F X ⟨i₂, hi₂⟩ :=
-  if h₁ : i₂ ≤ j then
-    (objIso F X ⟨i₁, hi.trans h₁⟩).hom ≫ F.map (homOfLE hi) ≫ (objIso F X ⟨i₂, h₁⟩).inv
-  else
-    if h₂ : i₁ ≤ j then
-      (objIso F X ⟨i₁, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫
-        (objSuccIso hj F X).inv ≫ eqToHom (by
-          congr
-          exact le_antisymm (Order.succ_le_of_lt (not_le.1 h₁)) hi₂)
-    else
-      eqToHom (by
-        congr
-        rw [le_antisymm hi₂ (Order.succ_le_of_lt (not_le.1 h₁)),
-          le_antisymm (hi.trans hi₂) (Order.succ_le_of_lt (not_le.1 h₂))])
-
-lemma map_eq (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
-    map hj F τ i₁ i₂ hi (hi₂.trans (Order.le_succ j)) =
-      (objIso F X ⟨i₁, hi.trans hi₂⟩).hom ≫ F.map (homOfLE hi) ≫
-        (objIso F X ⟨i₂, hi₂⟩).inv :=
-  dif_pos hi₂
-
-lemma map_self_succ :
-    map hj F τ j (Order.succ j) (Order.le_succ j) (by rfl) =
-      (objIso F X ⟨j, by simp⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv := by
-  dsimp [map]
-  rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
-    dif_pos (by rfl), map_id, comp_id, id_comp]
-
-@[simp]
-lemma map_id (i : J) (hi : i ≤ Order.succ j) :
-    map hj F τ i i (by rfl) hi = 𝟙 _ := by
-  dsimp [map]
-  by_cases h₁ : i ≤ j
-  · rw [dif_pos h₁, CategoryTheory.Functor.map_id, id_comp, Iso.hom_inv_id]
-  · obtain rfl : i = Order.succ j := le_antisymm hi (Order.succ_le_of_lt (not_le.1 h₁))
-    rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
-      dif_neg h₁]
-
-lemma map_comp (i₁ i₂ i₃ : J) (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) (h : i₃ ≤ Order.succ j) :
-    map hj F τ i₁ i₃ (h₁₂.trans h₂₃) h =
-      map hj F τ i₁ i₂ h₁₂ (h₂₃.trans h) ≫ map hj F τ i₂ i₃ h₂₃ h := by
-  by_cases h₁ : i₃ ≤ j
-  · rw [map_eq hj F τ i₁ i₂ _ (h₂₃.trans h₁), map_eq hj F τ i₂ i₃ _ h₁,
-      map_eq hj F τ i₁ i₃ _ h₁, assoc, assoc, Iso.inv_hom_id_assoc, ← map_comp_assoc,
-      homOfLE_comp]
-  · obtain rfl : i₃ = Order.succ j := le_antisymm h (Order.succ_le_of_lt (not_le.1 h₁))
-    obtain h₂ | rfl := h₂₃.lt_or_eq
-    · rw [Order.lt_succ_iff_of_not_isMax hj] at h₂
-      rw [map_eq hj F τ i₁ i₂ _ h₂]
-      dsimp [map]
-      rw [dif_neg h₁, dif_pos (h₁₂.trans h₂), dif_neg h₁, dif_pos h₂,
-        assoc, assoc, Iso.inv_hom_id_assoc,comp_id, ← map_comp_assoc, homOfLE_comp]
-    · rw [map_id, comp_id]
-
-end extendToSucc
-
-open extendToSucc in
-include hj in
-def extendToSucc : Set.Iic (Order.succ j) ⥤ C where
-  obj := obj F X
-  map {i₁ i₂} f := map hj F τ i₁ i₂ (leOfHom f) i₂.2
-  map_id _ := extendToSucc.map_id _ F τ _ _
-  map_comp {i₁ i₂ i₃} f g := extendToSucc.map_comp hj F τ i₁ i₂ i₃ (leOfHom f) (leOfHom g) i₃.2
-
-def extendToSuccObjIso (i : Set.Iic j) :
-    (extendToSucc hj F τ).obj ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i :=
-  extendToSucc.objIso F X i
-
-def extendToSuccObjSuccIso :
-    (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ ≅ X :=
-  extendToSucc.objSuccIso hj F X
-
-def extendToSuccRestrictionLEIso :
-    Iteration.restrictionLE (extendToSucc hj F τ) (Order.le_succ j) ≅ F :=
-  NatIso.ofComponents (extendToSuccObjIso hj F τ) (by
-    rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f
-    simp only [Set.mem_Iic] at h₁ h₂
-    dsimp [extendToSucc, extendToSuccObjIso]
-    rw [extendToSucc.map_eq _ _ _ _ _ _ h₂, assoc, assoc, Iso.inv_hom_id, comp_id]
-    rfl)
-
-lemma extendToSucc_map_le_succ :
-    (extendToSucc hj F τ).map (homOfLE (Order.le_succ j)) =
-        (extendToSuccObjIso hj F τ ⟨j, by simp⟩).hom ≫ τ ≫
-          (extendToSuccObjSuccIso hj F τ).inv :=
-  extendToSucc.map_self_succ _ _ _
-
-end Functor
-
-end CategoryTheory
-
-end
-
-namespace CategoryTheory
+open Category Limits
 
 variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ}
   {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J]
@@ -160,33 +43,53 @@ def mkOfBot : Iteration ε (⊥ : J) where
     exfalso
     refine hx.not_isMin (by simpa using h)
 
-namespace mkOfSucc
-
-variable {j : J} (hj : ¬IsMax j) (iter : Iteration ε j)
-
-/-- Auxiliary definition for `Functor.Iteration.mkOfSucc`. -/
-def isoSucc (i : J) (hi : i < Order.succ j) :
-    (extendToSucc hj iter.F (whiskerLeft _ ε)).obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ ≅
-      (extendToSucc hj iter.F (whiskerLeft _ ε)).obj ⟨i, hi.le⟩ ⋙ Φ :=
-  if hij : i < j then
-    extendToSuccObjIso _ _ _ ⟨Order.succ i, Order.succ_le_of_lt hij⟩ ≪≫
-      iter.isoSucc i hij ≪≫ (isoWhiskerRight (extendToSuccObjIso _ _ _ ⟨i, hij.le⟩).symm _)
-  else
-    have hij' : i = j := le_antisymm
-      (by simpa only [Order.lt_succ_iff_of_not_isMax hj] using hi) (by simpa using hij)
-    eqToIso (by subst hij'; rfl) ≪≫ extendToSuccObjSuccIso hj iter.F (whiskerLeft _ ε) ≪≫
-      isoWhiskerRight ((extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨j, by simp⟩).symm.trans
-          (eqToIso (by subst hij'; rfl))) _
-
-end mkOfSucc
-
+/-- When `j : J` is not maximal, this is the extension as `Iteration ε (Order.succ j)`
+of any `iter : Iteration ε j`. -/
 noncomputable def mkOfSucc {j : J} (hj : ¬IsMax j) (iter : Iteration ε j) :
     Iteration ε (Order.succ j) where
   F := extendToSucc hj iter.F (whiskerLeft _ ε)
   isoZero := (extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨⊥, by simp⟩).trans iter.isoZero
-  isoSucc i hi := mkOfSucc.isoSucc hj iter i hi
-  mapSucc'_eq := sorry
-  isColimit := sorry
+  isoSucc i hi :=
+    if hij : i < j then
+      extendToSuccObjIso _ _ _ ⟨Order.succ i, Order.succ_le_of_lt hij⟩ ≪≫
+        iter.isoSucc i hij ≪≫ (isoWhiskerRight (extendToSuccObjIso _ _ _ ⟨i, hij.le⟩).symm _)
+    else
+      have hij' : i = j := le_antisymm
+        (by simpa only [Order.lt_succ_iff_of_not_isMax hj] using hi) (by simpa using hij)
+      eqToIso (by subst hij'; rfl) ≪≫ extendToSuccObjSuccIso hj iter.F (whiskerLeft _ ε) ≪≫
+        isoWhiskerRight ((extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨j, by simp⟩).symm.trans
+            (eqToIso (by subst hij'; rfl))) _
+  mapSucc'_eq i hi := by
+    obtain hi' | rfl := ((Order.lt_succ_iff_of_not_isMax hj).mp hi).lt_or_eq
+    · ext X
+      have := iter.mapSucc_eq i hi'
+      dsimp [mapSucc, mapSucc'] at this ⊢
+      rw [extentToSucc_map _ _ _ _ _ _ (Order.succ_le_of_lt hi'), this, dif_pos hi']
+      dsimp
+      rw [assoc, assoc]
+      erw [ε.naturality_assoc]
+    · ext X
+      dsimp [mapSucc']
+      rw [dif_neg (gt_irrefl i), extendToSucc_map_le_succ]
+      dsimp
+      rw [id_comp, comp_id]
+      erw [ε.naturality_assoc]
+  isColimit i hi hij := by
+    have hij' : i ≤ j := by
+      obtain hij | rfl := hij.lt_or_eq
+      · exact (Order.lt_succ_iff_of_not_isMax hj).1 hij
+      · exfalso
+        exact Order.not_isSuccLimit_succ_of_not_isMax hj hi
+    refine (IsColimit.precomposeHomEquiv
+      (isoWhiskerLeft (monotone_inclusion_lt_le_of_le hij').functor
+        (extendToSuccRestrictionLEIso hj iter.F (whiskerLeft _ ε))).symm _).1
+      (IsColimit.ofIsoColimit (iter.isColimit i hi hij')
+      (Iso.symm (Cocones.ext (extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨i, hij'⟩)
+      (fun ⟨k, hk⟩ ↦ ?_))))
+    dsimp
+    rw [assoc, extendToSuccObjIso_hom_naturality hj iter.F (whiskerLeft _ ε)]
+    dsimp
+    rw [Iso.inv_hom_id_assoc]
 
 end Iteration
 

From 943044b70565c86472b5b64f835faf22cb178e32 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 19 Nov 2024 20:29:36 +0100
Subject: [PATCH 14/28] fixing imports

---
 Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
index 5c792d72b67b7..cf96cd6faf32b 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
-import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
 
 /-!

From 638cb34c0dc91993dd5755d4db225ac9861fc43c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 19 Nov 2024 21:45:17 +0100
Subject: [PATCH 15/28] wip

---
 Mathlib.lean                                  |  1 +
 .../SmallObject/Iteration/Basic.lean          | 28 ++++++-
 .../Iteration/FunctorOfCocone.lean            | 64 ++++++++++++++++
 .../SmallObject/Iteration/Nonempty.lean       | 73 +++++++++++++++++++
 .../SmallObject/Iteration/UniqueHom.lean      |  9 ++-
 5 files changed, 173 insertions(+), 2 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index ec249d4f1b97e..d1478ad6c5c7d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2082,6 +2082,7 @@ import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
 import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
 import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
+import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
 import Mathlib.CategoryTheory.Square
 import Mathlib.CategoryTheory.Subobject.Basic
 import Mathlib.CategoryTheory.Subobject.Comma
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index d739917e114af..784140777ec63 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.Category.Preorder
-import Mathlib.CategoryTheory.Limits.IsLimit
+import Mathlib.CategoryTheory.Limits.HasLimits
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.SuccPred.Limit
 
@@ -239,6 +239,14 @@ def trunc (iter : Iteration ε j) {i : J} (hi : i ≤ j) : Iteration ε i where
   mapSucc'_eq k hk := iter.mapSucc'_eq k (lt_of_lt_of_le hk hi)
   isColimit k hk' hk := iter.isColimit k hk' (hk.trans hi)
 
+@[simp]
+lemma trunc_refl (iter : Iteration ε j) :
+    iter.trunc (Preorder.le_refl j) = iter := rfl
+
+@[simp]
+lemma trunc_trunc (iter : Iteration ε j) {i : J} (hi : i ≤ j) {k : J} (hk : k ≤ i) :
+    (iter.trunc hi).trunc hk = iter.trunc (hk.trans hi) := rfl
+
 variable (ε) in
 /-- The truncation functor `Iteration ε j ⥤ Iteration ε i` when `i ≤ j`. -/
 @[simps obj]
@@ -272,4 +280,22 @@ end Iteration
 
 end Functor
 
+open Limits
+
+variable (C J) [Preorder J]
+
+class HasIterationOfShape where
+  hasColimitsOfShape_of_isSuccLimit (j : J) (hj : Order.IsSuccLimit j) :
+    HasColimitsOfShape (Set.Iio j) C := by infer_instance
+  hasColimitsOfShape : HasColimitsOfShape J C := by infer_instance
+
+attribute [instance] HasIterationOfShape.hasColimitsOfShape
+
+variable {J}
+
+lemma hasColimitOfShape_of_isSuccLimit [HasIterationOfShape C J] (j : J)
+    (hj : Order.IsSuccLimit j) :
+    HasColimitsOfShape (Set.Iio j) C :=
+    HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit j hj
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
new file mode 100644
index 0000000000000..46faba599e7fc
--- /dev/null
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
+
+/-!
+# ...
+
+-/
+
+universe u
+
+namespace CategoryTheory
+
+open Category Limits
+
+namespace Functor
+
+variable {C : Type*} [Category C]
+  {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J]
+  {j : J} {F : Set.Iio j ⥤ C} (c : Cocone F)
+
+namespace ofCocone
+
+def obj (i : J) (_ : i ≤ j) : C :=
+  if hi : i < j then
+    F.obj ⟨i, hi⟩
+  else c.pt
+
+def objIso (i : J) (hi : i < j) :
+    obj c i hi.le ≅ F.obj ⟨i, hi⟩ :=
+  eqToIso (dif_pos hi)
+
+def objIsoPt :
+    obj c j (by rfl) ≅ c.pt :=
+  eqToIso (dif_neg (by simp))
+
+def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
+    obj c i₁ (hi.trans hi₂) ⟶ obj c i₂ hi₂ :=
+  if h₂ : i₂ < j then
+    (objIso c i₁ (lt_of_le_of_lt hi h₂)).hom ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
+  else
+    have h₂' : i₂ = j := le_antisymm hi₂ (by simpa using h₂)
+    if h₁ : i₁ < j then
+      (objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom (by subst h₂'; rfl)
+    else
+      have h₁' : i₁ = j := le_antisymm (hi.trans hi₂) (by simpa using h₁)
+      eqToHom (by subst h₁' h₂'; rfl)
+
+end ofCocone
+
+open ofCocone in
+def ofCocone : Set.Iic j ⥤ C where
+  obj i := obj c i.1 i.2
+  map f := map c _ _ (leOfHom f) _
+  map_id := sorry
+  map_comp := sorry
+
+end Functor
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
index cf96cd6faf32b..d1688e59eb544 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
@@ -3,7 +3,10 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
+import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
 import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
+import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
+import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 
 /-!
 # Existence of objects in the category of iterations of functors
@@ -90,6 +93,76 @@ noncomputable def mkOfSucc {j : J} (hj : ¬IsMax j) (iter : Iteration ε j) :
     dsimp
     rw [Iso.inv_hom_id_assoc]
 
+section
+
+variable [WellFoundedLT J] {j : J} (hj : Order.IsSuccLimit j)
+  (iter : ∀ (i : J) (_ : i < j), Iteration ε i)
+
+namespace mkOfLimit
+
+abbrev obj (i : J) (hi : i < j) : C ⥤ C := (iter i hi).F.obj ⟨i, by simp⟩
+
+noncomputable def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
+    obj iter i₁ (lt_of_le_of_lt hi hi₂) ⟶ obj iter i₂ hi₂ :=
+  ((iter i₁ (lt_of_le_of_lt hi hi₂)).iso ((iter i₂ hi₂).trunc hi)).hom.natTrans.app
+    ⟨i₁, by simp⟩ ≫ (iter i₂ hi₂).F.map (homOfLE hi)
+
+@[simp]
+lemma map_id (i : J) (hi : i < j) :
+    map iter i i (by rfl) hi = 𝟙 _ := by
+  simp [map]
+
+lemma map_comp (i₁ i₂ i₃ : J) (hi : i₁ ≤ i₂) (hi' : i₂ ≤ i₃) (hi₃ : i₃ < j) :
+    map iter i₁ i₃ (hi.trans hi') hi₃ =
+      map iter i₁ i₂ hi (lt_of_le_of_lt hi' hi₃) ≫
+        map iter i₂ i₃ hi' hi₃ := by
+  dsimp [map]
+  rw [assoc, NatTrans.naturality_assoc]
+  dsimp
+  rw [← truncFunctor_map_natTrans_app _ hi i₁ (by rfl), truncFunctor_map_iso_hom,
+    ← NatTrans.comp_app_assoc, ← natTrans_comp, ← Functor.map_comp]
+  dsimp only [truncFunctor_obj, trunc_trunc]
+  rw [iso_hom_comp_iso_hom, homOfLE_comp]
+
+@[simps]
+noncomputable def functor : Set.Iio j ⥤ C ⥤ C where
+  obj i := obj iter i.1 i.2
+  map f := map iter _ _ (leOfHom f) _
+  map_id _ := map_id iter _ _
+  map_comp _ _ := map_comp iter _ _ _ _ _ _
+
+end mkOfLimit
+
+section
+
+open mkOfLimit
+
+variable [HasColimit (functor iter)]
+
+include hj iter in
+noncomputable def mkOfLimit :
+    Iteration ε j where
+  F := Functor.ofCocone (colimit.cocone (functor iter))
+  isoZero := by
+    have := hj
+    sorry
+  isoSucc := sorry
+  mapSucc'_eq := sorry
+  isColimit := sorry
+
+end
+end
+
+instance [WellFoundedLT J] [HasIterationOfShape C J] (j : J) : Nonempty (Iteration ε j) := by
+  induction j using SuccOrder.limitRecOn with
+  | hm i hi =>
+      obtain rfl : i = ⊥ := by simpa using hi
+      exact ⟨mkOfBot ε J⟩
+  | hs i hi hi' => exact ⟨mkOfSucc hi hi'.some⟩
+  | hl i hi hi' =>
+      have := hasColimitOfShape_of_isSuccLimit C i hi
+      exact ⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩
+
 end Iteration
 
 end Functor
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
index 5e804f4b55103..bb40843af6cc7 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
@@ -240,7 +240,14 @@ noncomputable def iso : iter₁ ≅ iter₂ where
 @[simp]
 lemma iso_refl : iso iter₁ iter₁ = Iso.refl _ := by aesop_cat
 
-lemma iso_trans : iso iter₁ iter₂ ≪≫ iso iter₂ iter₃ = iso iter₁ iter₃ := by aesop_cat
+lemma iso_hom_comp_iso_hom :
+    (iso iter₁ iter₂).hom ≫ (iso iter₂ iter₃).hom = (iso iter₁ iter₃).hom :=
+  Subsingleton.elim _ _
+
+lemma truncFunctor_map_iso_hom {i : J} (hi : i ≤ j) :
+    (truncFunctor ε hi).map (iso iter₁ iter₂).hom =
+      (iso (iter₁.trunc hi) (iter₂.trunc hi)).hom :=
+  Subsingleton.elim _ _
 
 end Iteration
 

From 659a203e080248fa672e16f0e6e6cd13f0d70dfe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 19 Nov 2024 22:41:47 +0100
Subject: [PATCH 16/28] wip

---
 .../Iteration/FunctorOfCocone.lean            | 93 ++++++++++++++++---
 .../SmallObject/Iteration/Nonempty.lean       | 25 ++---
 2 files changed, 96 insertions(+), 22 deletions(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
index 46faba599e7fc..27a325789a149 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
@@ -7,7 +7,11 @@ Authors: Joël Riou
 import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 
 /-!
-# ...
+# The functor from `Set.Iic j` deduced from a cocone
+
+Given a functor `F : Set.Iio j ⥤ C` and `c : Cocone F`, we define
+an extension of `F` as a functor `Set.Iic j ⥤ C` for which
+the top element is mapped to `c.pt`.
 
 -/
 
@@ -20,26 +24,30 @@ open Category Limits
 namespace Functor
 
 variable {C : Type*} [Category C]
-  {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J]
+  {J : Type u} [LinearOrder J]
   {j : J} {F : Set.Iio j ⥤ C} (c : Cocone F)
 
 namespace ofCocone
 
-def obj (i : J) (_ : i ≤ j) : C :=
+/-- Auxiliary definition for `Functor.ofCocone`. -/
+def obj (i : J) : C :=
   if hi : i < j then
     F.obj ⟨i, hi⟩
   else c.pt
 
+/-- Auxiliary definition for `Functor.ofCocone`. -/
 def objIso (i : J) (hi : i < j) :
-    obj c i hi.le ≅ F.obj ⟨i, hi⟩ :=
+    obj c i ≅ F.obj ⟨i, hi⟩ :=
   eqToIso (dif_pos hi)
 
+/-- Auxiliary definition for `Functor.ofCocone`. -/
 def objIsoPt :
-    obj c j (by rfl) ≅ c.pt :=
+    obj c j  ≅ c.pt :=
   eqToIso (dif_neg (by simp))
 
+/-- Auxiliary definition for `Functor.ofCocone`. -/
 def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
-    obj c i₁ (hi.trans hi₂) ⟶ obj c i₂ hi₂ :=
+    obj c i₁ ⟶ obj c i₂ :=
   if h₂ : i₂ < j then
     (objIso c i₁ (lt_of_le_of_lt hi h₂)).hom ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
   else
@@ -50,14 +58,77 @@ def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
       have h₁' : i₁ = j := le_antisymm (hi.trans hi₂) (by simpa using h₁)
       eqToHom (by subst h₁' h₂'; rfl)
 
+lemma map_id (i : J) (hi : i ≤ j) :
+    map c i i (by rfl) hi = 𝟙 _:= by
+  dsimp [map]
+  obtain hi' | rfl := hi.lt_or_eq
+  · rw [dif_pos hi', F.map_id, id_comp, Iso.hom_inv_id]
+  · rw [dif_neg (by simp), dif_neg (by simp)]
+
+lemma map_comp (i₁ i₂ i₃ : J) (hi : i₁ ≤ i₂) (hi' : i₂ ≤ i₃) (hi₃ : i₃ ≤ j) :
+    map c i₁ i₃ (hi.trans hi') hi₃ =
+      map c i₁ i₂ hi (hi'.trans hi₃) ≫
+        map c i₂ i₃ hi' hi₃ := by
+  obtain hi₁₂ | rfl := hi.lt_or_eq
+  · obtain hi₂₃ | rfl := hi'.lt_or_eq
+    · dsimp [map]
+      obtain hi₃' | rfl := hi₃.lt_or_eq
+      · rw [dif_pos hi₃', dif_pos (hi₂₃.trans hi₃'), dif_pos hi₃', assoc, assoc,
+          Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp]
+      · rw [dif_neg (by simp), dif_pos (hi₁₂.trans hi₂₃), dif_pos hi₂₃, dif_neg (by simp),
+          dif_pos hi₂₃, eqToHom_refl, comp_id, assoc, assoc, Iso.inv_hom_id_assoc,
+          Cocone.w_assoc]
+    · rw [map_id, comp_id]
+  · rw [map_id, id_comp]
+
 end ofCocone
 
-open ofCocone in
+/-- Given a functor `F : Set.Iio j ⥤ C` and a cocone `c : Cocone F`,
+where `j : J` and `J` is linearly ordered, this is the functor
+`Set.Iic j ⥤ C` which extends `F` and sends the top element to `c.pt`. -/
 def ofCocone : Set.Iic j ⥤ C where
-  obj i := obj c i.1 i.2
-  map f := map c _ _ (leOfHom f) _
-  map_id := sorry
-  map_comp := sorry
+  obj i := ofCocone.obj c i.1
+  map {_ j} f := ofCocone.map c _ _ (leOfHom f) j.2
+  map_id i := ofCocone.map_id _ _ i.2
+  map_comp {_ _ i₃} _ _ := ofCocone.map_comp _ _ _ _ _ _ i₃.2
+
+/-- The isomorphism `(ofCocone c).obj ⟨i, _⟩ ≅ F.obj ⟨i, _⟩` when `i < j`. -/
+def ofCoconeObjIso (i : J) (hi : i < j) :
+    (ofCocone c).obj ⟨i, hi.le⟩ ≅ F.obj ⟨i, hi⟩ :=
+  ofCocone.objIso c _ _
+
+/-- The isomorphism `(ofCocone c).obj ⟨j, _⟩ ≅ c.pt`. -/
+def ofCoconeObjIsoPt :
+    (ofCocone c).obj ⟨j, by simp⟩ ≅ c.pt :=
+  ofCocone.objIsoPt c
+
+lemma ofCocone_map_to_top (i : J) (hi : i < j) :
+    (ofCocone c).map (homOfLE hi.le) =
+      (ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv := by
+  dsimp [ofCocone, ofCocone.map, ofCoconeObjIso, ofCoconeObjIsoPt]
+  rw [dif_neg (by simp), dif_pos hi, comp_id]
+
+lemma ofCocone_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
+    (ofCocone c).map (homOfLE hi : ⟨i₁, hi.trans hi₂.le⟩ ⟶ ⟨i₂, hi₂.le⟩) =
+      (ofCoconeObjIso c i₁ (lt_of_le_of_lt hi hi₂)).hom ≫ F.map (homOfLE hi) ≫
+        (ofCoconeObjIso c i₂ hi₂).inv := by
+  dsimp [ofCocone, ofCoconeObjIso, ofCocone.map]
+  rw [dif_pos hi₂]
+
+@[reassoc]
+lemma ofCoconeObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
+    (ofCocone c).map (homOfLE hi : ⟨i₁, hi.trans hi₂.le⟩ ⟶ ⟨i₂, hi₂.le⟩) ≫
+      (ofCoconeObjIso c i₂ hi₂).hom =
+      (ofCoconeObjIso c i₁ (lt_of_le_of_lt hi hi₂)).hom ≫ F.map (homOfLE hi) := by
+  rw [ofCocone_map c i₁ i₂ hi hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]
+
+/-- The isomorphism expressing that `ofCocone c` extends the functor `F`
+when `c : Cocone F`. -/
+@[simps!]
+def restrictionLTOfCoconeIso :
+    Iteration.restrictionLT (ofCocone c) (Preorder.le_refl j) ≅ F :=
+  NatIso.ofComponents (fun ⟨i, hi⟩ ↦ ofCoconeObjIso c i hi)
+    (by intros; apply ofCoconeObjIso_hom_naturality)
 
 end Functor
 
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
index d1688e59eb544..a3063b9efaca3 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
@@ -100,10 +100,8 @@ variable [WellFoundedLT J] {j : J} (hj : Order.IsSuccLimit j)
 
 namespace mkOfLimit
 
-abbrev obj (i : J) (hi : i < j) : C ⥤ C := (iter i hi).F.obj ⟨i, by simp⟩
-
 noncomputable def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
-    obj iter i₁ (lt_of_le_of_lt hi hi₂) ⟶ obj iter i₂ hi₂ :=
+    (iter i₁ (lt_of_le_of_lt hi hi₂)).F.obj ⟨i₁, by simp⟩ ⟶ (iter i₂ hi₂).F.obj ⟨i₂, by simp⟩ :=
   ((iter i₁ (lt_of_le_of_lt hi hi₂)).iso ((iter i₂ hi₂).trunc hi)).hom.natTrans.app
     ⟨i₁, by simp⟩ ≫ (iter i₂ hi₂).F.map (homOfLE hi)
 
@@ -126,15 +124,13 @@ lemma map_comp (i₁ i₂ i₃ : J) (hi : i₁ ≤ i₂) (hi' : i₂ ≤ i₃) (
 
 @[simps]
 noncomputable def functor : Set.Iio j ⥤ C ⥤ C where
-  obj i := obj iter i.1 i.2
+  obj i := (iter i.1 i.2).F.obj ⟨i.1, by simp⟩
   map f := map iter _ _ (leOfHom f) _
   map_id _ := map_id iter _ _
   map_comp _ _ := map_comp iter _ _ _ _ _ _
 
 end mkOfLimit
 
-section
-
 open mkOfLimit
 
 variable [HasColimit (functor iter)]
@@ -143,15 +139,22 @@ include hj iter in
 noncomputable def mkOfLimit :
     Iteration ε j where
   F := Functor.ofCocone (colimit.cocone (functor iter))
-  isoZero := by
+  isoZero := (Functor.ofCoconeObjIso _ ⊥ (Ne.bot_lt (by simpa using hj.1))).trans
+    ((iter ⊥ _).isoZero)
+  isoSucc i hi :=
+    Functor.ofCoconeObjIso _ (Order.succ i) ((Order.IsSuccLimit.succ_lt_iff hj).2 hi) ≪≫
+      (iter (Order.succ i) ((Order.IsSuccLimit.succ_lt_iff hj).2 hi)).isoSucc i (by
+        rw [Order.lt_succ_iff_not_isMax, not_isMax_iff]
+        exact ⟨_, hi⟩) ≪≫
+        isoWhiskerRight ((Iteration.eval ε (Preorder.le_refl i)).mapIso
+            (((iter (Order.succ i) _).trunc (Order.le_succ i)).iso (iter i hi)) ≪≫
+            (Functor.ofCoconeObjIso (colimit.cocone (functor iter)) i hi).symm) Φ
+  mapSucc'_eq := sorry
+  isColimit := by
     have := hj
     sorry
-  isoSucc := sorry
-  mapSucc'_eq := sorry
-  isColimit := sorry
 
 end
-end
 
 instance [WellFoundedLT J] [HasIterationOfShape C J] (j : J) : Nonempty (Iteration ε j) := by
   induction j using SuccOrder.limitRecOn with

From b394a4925da336107314069cab16494731c782ab Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Wed, 20 Nov 2024 19:16:37 +0100
Subject: [PATCH 17/28] wip

---
 .../Iteration/FunctorOfCocone.lean            | 11 ++++
 .../SmallObject/Iteration/Nonempty.lean       | 64 +++++++++++++++++--
 2 files changed, 71 insertions(+), 4 deletions(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
index 27a325789a149..35b3bf90ea04c 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
@@ -108,6 +108,7 @@ lemma ofCocone_map_to_top (i : J) (hi : i < j) :
   dsimp [ofCocone, ofCocone.map, ofCoconeObjIso, ofCoconeObjIsoPt]
   rw [dif_neg (by simp), dif_pos hi, comp_id]
 
+@[reassoc]
 lemma ofCocone_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
     (ofCocone c).map (homOfLE hi : ⟨i₁, hi.trans hi₂.le⟩ ⟶ ⟨i₂, hi₂.le⟩) =
       (ofCoconeObjIso c i₁ (lt_of_le_of_lt hi hi₂)).hom ≫ F.map (homOfLE hi) ≫
@@ -130,6 +131,16 @@ def restrictionLTOfCoconeIso :
   NatIso.ofComponents (fun ⟨i, hi⟩ ↦ ofCoconeObjIso c i hi)
     (by intros; apply ofCoconeObjIso_hom_naturality)
 
+variable {c} in
+/-- If `c` is a colimit cocone, then so is `coconeOfLE (ofCocone c) (Preorder.le_refl j)`. -/
+def isColimitCoconeOfLEOfCocone (hc : IsColimit c) :
+    IsColimit (Iteration.coconeOfLE (ofCocone c) (Preorder.le_refl j)) :=
+  (IsColimit.precomposeInvEquiv (restrictionLTOfCoconeIso c) _).1
+    (IsColimit.ofIsoColimit hc
+      (Cocones.ext (ofCoconeObjIsoPt c).symm (fun ⟨i, hi⟩ ↦ by
+        dsimp
+        rw [ofCocone_map_to_top _ _ hi, Iso.inv_hom_id_assoc])))
+
 end Functor
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
index a3063b9efaca3..f74d00b08eb65 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
@@ -100,6 +100,7 @@ variable [WellFoundedLT J] {j : J} (hj : Order.IsSuccLimit j)
 
 namespace mkOfLimit
 
+/-- Auxiliary definition for `mkOfLimit`. -/
 noncomputable def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
     (iter i₁ (lt_of_le_of_lt hi hi₂)).F.obj ⟨i₁, by simp⟩ ⟶ (iter i₂ hi₂).F.obj ⟨i₂, by simp⟩ :=
   ((iter i₁ (lt_of_le_of_lt hi hi₂)).iso ((iter i₂ hi₂).trunc hi)).hom.natTrans.app
@@ -122,6 +123,7 @@ lemma map_comp (i₁ i₂ i₃ : J) (hi : i₁ ≤ i₂) (hi' : i₂ ≤ i₃) (
   dsimp only [truncFunctor_obj, trunc_trunc]
   rw [iso_hom_comp_iso_hom, homOfLE_comp]
 
+/-- Auxiliary definition for `mkOfLimit`. -/
 @[simps]
 noncomputable def functor : Set.Iio j ⥤ C ⥤ C where
   obj i := (iter i.1 i.2).F.obj ⟨i.1, by simp⟩
@@ -129,6 +131,33 @@ noncomputable def functor : Set.Iio j ⥤ C ⥤ C where
   map_id _ := map_id iter _ _
   map_comp _ _ := map_comp iter _ _ _ _ _ _
 
+/-- Auxiliary definition for `mkOfLimit`. -/
+noncomputable def restrictionLTFunctorIso (i : J) (hi : i < j) :
+    (monotone_inclusion_lt_lt_of_le hi.le).functor ⋙ functor iter ≅
+      restrictionLT (iter i hi).F (by rfl) :=
+  NatIso.ofComponents (fun ⟨k, hk⟩ ↦ (eval ε (Preorder.le_refl k)).mapIso
+    ((iter k (hk.trans hi)).iso ((iter i hi).trunc hk.le))) (by
+      rintro ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f
+      dsimp [map]
+      rw [assoc, NatTrans.naturality]
+      dsimp
+      simp only [← assoc]; congr 1
+      dsimp
+      rw [← truncFunctor_map_natTrans_app _ (i := k₁) (j := k₂) (leOfHom f) _ (by rfl),
+        truncFunctor_map_iso_hom, ← NatTrans.comp_app, ← natTrans_comp]
+      erw [iso_hom_comp_iso_hom]
+      rfl)
+
+@[reassoc]
+lemma restrictionLTFunctorIso_inv_app_map (k i : J) (hik : k < i) (hij : i < j) :
+    (restrictionLTFunctorIso iter i hij).inv.app ⟨k, hik⟩ ≫ map iter k i hik.le hij =
+      (iter i hij).F.map (homOfLE hik.le) := by
+  dsimp [restrictionLTFunctorIso, map]
+  rw [← NatTrans.comp_app_assoc, ← natTrans_comp, Iso.inv_hom_id, natTrans_id,
+    NatTrans.id_app]
+  dsimp
+  rw [id_comp]
+
 end mkOfLimit
 
 open mkOfLimit
@@ -136,6 +165,9 @@ open mkOfLimit
 variable [HasColimit (functor iter)]
 
 include hj iter in
+/-- When `j : J` satisfies `Order.IsSuccLimit j` and we have `iter i hij : Iteration ε i`
+for any `i : J` such that `hij : i < j`, then this is a term in `Iteration ε j`,
+provided a suitable colimit indexed by `Set.Iio j` exists. -/
 noncomputable def mkOfLimit :
     Iteration ε j where
   F := Functor.ofCocone (colimit.cocone (functor iter))
@@ -149,10 +181,34 @@ noncomputable def mkOfLimit :
         isoWhiskerRight ((Iteration.eval ε (Preorder.le_refl i)).mapIso
             (((iter (Order.succ i) _).trunc (Order.le_succ i)).iso (iter i hi)) ≪≫
             (Functor.ofCoconeObjIso (colimit.cocone (functor iter)) i hi).symm) Φ
-  mapSucc'_eq := sorry
-  isColimit := by
-    have := hj
-    sorry
+  mapSucc'_eq i hi := by
+    have hi' : Order.succ i < j := (Order.IsSuccLimit.succ_lt_iff hj).mpr hi
+    have hi'' : i < Order.succ i := by
+      simp only [Order.lt_succ_iff_not_isMax, not_isMax_iff]
+      exact ⟨_, hi⟩
+    have := (iter _ hi').mapSucc_eq i hi''
+    dsimp [mapSucc', mapSucc] at this ⊢
+    rw [ofCocone_map _ _ _ _ hi', functor_map, map, this]
+    ext X
+    dsimp
+    rw [assoc, assoc, assoc, map_comp_assoc]
+    erw [← ε.naturality_assoc, ← ε.naturality_assoc]
+    rfl
+  isColimit i hi hij := by
+    apply Nonempty.some
+    obtain hij' | rfl := hij.lt_or_eq
+    · refine ⟨(IsColimit.precomposeInvEquiv
+        (isoWhiskerLeft (monotone_inclusion_lt_lt_of_le hij).functor
+          (restrictionLTOfCoconeIso (colimit.cocone (functor iter))) ≪≫
+          restrictionLTFunctorIso iter i hij') _).1
+        (IsColimit.ofIsoColimit ((iter i hij').isColimit i hi (by rfl))
+        (Cocones.ext
+          (ofCoconeObjIso (colimit.cocone (functor iter)) i hij').symm (fun ⟨k, hk⟩ ↦ ?_)))⟩
+      dsimp
+      rw [ofCocone_map _ _ _ _ hij', assoc]
+      dsimp
+      rw [Iso.inv_hom_id_assoc, restrictionLTFunctorIso_inv_app_map_assoc]
+    · exact ⟨Functor.isColimitCoconeOfLEOfCocone (colimit.isColimit _)⟩
 
 end
 

From 9c6f1e6a6f11cb977e1e90252a34a74e367edeb7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Wed, 20 Nov 2024 19:17:15 +0100
Subject: [PATCH 18/28] fixed Mathlib.lean

---
 Mathlib.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 33bc6d4704015..eea2f71c70ac0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2085,9 +2085,9 @@ import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.SmallObject.Construction
 import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
+import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
 import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
 import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
-import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
 import Mathlib.CategoryTheory.Square
 import Mathlib.CategoryTheory.Subobject.Basic
 import Mathlib.CategoryTheory.Subobject.Comma

From 7318f01bb5f5873c895246ed3776f0a637bc7e95 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Wed, 20 Nov 2024 19:32:20 +0100
Subject: [PATCH 19/28] cleaning up

---
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index 784140777ec63..a82672bb5e9c7 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -284,7 +284,11 @@ open Limits
 
 variable (C J) [Preorder J]
 
-class HasIterationOfShape where
+/-- A category `C` has iterations of shape `J` when certain shapes
+of colimits exists. When `J` is well ordered, this assumption is used in
+order to show that the category `Iteration ε j` is nonempty for any `j : J`,
+see the file `CategoryTheory.SmallObject.Nonempty`. -/
+class HasIterationOfShape : Prop where
   hasColimitsOfShape_of_isSuccLimit (j : J) (hj : Order.IsSuccLimit j) :
     HasColimitsOfShape (Set.Iio j) C := by infer_instance
   hasColimitsOfShape : HasColimitsOfShape J C := by infer_instance

From 1b87f3e81822297de7f52fecfd4d3071505eea75 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 30 Nov 2024 21:59:30 +0100
Subject: [PATCH 20/28] added functorofcocone

---
 Mathlib.lean                                  |   1 +
 .../Iteration/FunctorOfCocone.lean            | 146 ++++++++++++++++++
 2 files changed, 147 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index e7bf4ac3e66d4..e5d597cc75bb3 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2130,6 +2130,7 @@ import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.SmallObject.Construction
 import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
+import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
 import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
 import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 import Mathlib.CategoryTheory.Square
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
new file mode 100644
index 0000000000000..35b3bf90ea04c
--- /dev/null
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
+
+/-!
+# The functor from `Set.Iic j` deduced from a cocone
+
+Given a functor `F : Set.Iio j ⥤ C` and `c : Cocone F`, we define
+an extension of `F` as a functor `Set.Iic j ⥤ C` for which
+the top element is mapped to `c.pt`.
+
+-/
+
+universe u
+
+namespace CategoryTheory
+
+open Category Limits
+
+namespace Functor
+
+variable {C : Type*} [Category C]
+  {J : Type u} [LinearOrder J]
+  {j : J} {F : Set.Iio j ⥤ C} (c : Cocone F)
+
+namespace ofCocone
+
+/-- Auxiliary definition for `Functor.ofCocone`. -/
+def obj (i : J) : C :=
+  if hi : i < j then
+    F.obj ⟨i, hi⟩
+  else c.pt
+
+/-- Auxiliary definition for `Functor.ofCocone`. -/
+def objIso (i : J) (hi : i < j) :
+    obj c i ≅ F.obj ⟨i, hi⟩ :=
+  eqToIso (dif_pos hi)
+
+/-- Auxiliary definition for `Functor.ofCocone`. -/
+def objIsoPt :
+    obj c j  ≅ c.pt :=
+  eqToIso (dif_neg (by simp))
+
+/-- Auxiliary definition for `Functor.ofCocone`. -/
+def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
+    obj c i₁ ⟶ obj c i₂ :=
+  if h₂ : i₂ < j then
+    (objIso c i₁ (lt_of_le_of_lt hi h₂)).hom ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
+  else
+    have h₂' : i₂ = j := le_antisymm hi₂ (by simpa using h₂)
+    if h₁ : i₁ < j then
+      (objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom (by subst h₂'; rfl)
+    else
+      have h₁' : i₁ = j := le_antisymm (hi.trans hi₂) (by simpa using h₁)
+      eqToHom (by subst h₁' h₂'; rfl)
+
+lemma map_id (i : J) (hi : i ≤ j) :
+    map c i i (by rfl) hi = 𝟙 _:= by
+  dsimp [map]
+  obtain hi' | rfl := hi.lt_or_eq
+  · rw [dif_pos hi', F.map_id, id_comp, Iso.hom_inv_id]
+  · rw [dif_neg (by simp), dif_neg (by simp)]
+
+lemma map_comp (i₁ i₂ i₃ : J) (hi : i₁ ≤ i₂) (hi' : i₂ ≤ i₃) (hi₃ : i₃ ≤ j) :
+    map c i₁ i₃ (hi.trans hi') hi₃ =
+      map c i₁ i₂ hi (hi'.trans hi₃) ≫
+        map c i₂ i₃ hi' hi₃ := by
+  obtain hi₁₂ | rfl := hi.lt_or_eq
+  · obtain hi₂₃ | rfl := hi'.lt_or_eq
+    · dsimp [map]
+      obtain hi₃' | rfl := hi₃.lt_or_eq
+      · rw [dif_pos hi₃', dif_pos (hi₂₃.trans hi₃'), dif_pos hi₃', assoc, assoc,
+          Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp]
+      · rw [dif_neg (by simp), dif_pos (hi₁₂.trans hi₂₃), dif_pos hi₂₃, dif_neg (by simp),
+          dif_pos hi₂₃, eqToHom_refl, comp_id, assoc, assoc, Iso.inv_hom_id_assoc,
+          Cocone.w_assoc]
+    · rw [map_id, comp_id]
+  · rw [map_id, id_comp]
+
+end ofCocone
+
+/-- Given a functor `F : Set.Iio j ⥤ C` and a cocone `c : Cocone F`,
+where `j : J` and `J` is linearly ordered, this is the functor
+`Set.Iic j ⥤ C` which extends `F` and sends the top element to `c.pt`. -/
+def ofCocone : Set.Iic j ⥤ C where
+  obj i := ofCocone.obj c i.1
+  map {_ j} f := ofCocone.map c _ _ (leOfHom f) j.2
+  map_id i := ofCocone.map_id _ _ i.2
+  map_comp {_ _ i₃} _ _ := ofCocone.map_comp _ _ _ _ _ _ i₃.2
+
+/-- The isomorphism `(ofCocone c).obj ⟨i, _⟩ ≅ F.obj ⟨i, _⟩` when `i < j`. -/
+def ofCoconeObjIso (i : J) (hi : i < j) :
+    (ofCocone c).obj ⟨i, hi.le⟩ ≅ F.obj ⟨i, hi⟩ :=
+  ofCocone.objIso c _ _
+
+/-- The isomorphism `(ofCocone c).obj ⟨j, _⟩ ≅ c.pt`. -/
+def ofCoconeObjIsoPt :
+    (ofCocone c).obj ⟨j, by simp⟩ ≅ c.pt :=
+  ofCocone.objIsoPt c
+
+lemma ofCocone_map_to_top (i : J) (hi : i < j) :
+    (ofCocone c).map (homOfLE hi.le) =
+      (ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv := by
+  dsimp [ofCocone, ofCocone.map, ofCoconeObjIso, ofCoconeObjIsoPt]
+  rw [dif_neg (by simp), dif_pos hi, comp_id]
+
+@[reassoc]
+lemma ofCocone_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
+    (ofCocone c).map (homOfLE hi : ⟨i₁, hi.trans hi₂.le⟩ ⟶ ⟨i₂, hi₂.le⟩) =
+      (ofCoconeObjIso c i₁ (lt_of_le_of_lt hi hi₂)).hom ≫ F.map (homOfLE hi) ≫
+        (ofCoconeObjIso c i₂ hi₂).inv := by
+  dsimp [ofCocone, ofCoconeObjIso, ofCocone.map]
+  rw [dif_pos hi₂]
+
+@[reassoc]
+lemma ofCoconeObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
+    (ofCocone c).map (homOfLE hi : ⟨i₁, hi.trans hi₂.le⟩ ⟶ ⟨i₂, hi₂.le⟩) ≫
+      (ofCoconeObjIso c i₂ hi₂).hom =
+      (ofCoconeObjIso c i₁ (lt_of_le_of_lt hi hi₂)).hom ≫ F.map (homOfLE hi) := by
+  rw [ofCocone_map c i₁ i₂ hi hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]
+
+/-- The isomorphism expressing that `ofCocone c` extends the functor `F`
+when `c : Cocone F`. -/
+@[simps!]
+def restrictionLTOfCoconeIso :
+    Iteration.restrictionLT (ofCocone c) (Preorder.le_refl j) ≅ F :=
+  NatIso.ofComponents (fun ⟨i, hi⟩ ↦ ofCoconeObjIso c i hi)
+    (by intros; apply ofCoconeObjIso_hom_naturality)
+
+variable {c} in
+/-- If `c` is a colimit cocone, then so is `coconeOfLE (ofCocone c) (Preorder.le_refl j)`. -/
+def isColimitCoconeOfLEOfCocone (hc : IsColimit c) :
+    IsColimit (Iteration.coconeOfLE (ofCocone c) (Preorder.le_refl j)) :=
+  (IsColimit.precomposeInvEquiv (restrictionLTOfCoconeIso c) _).1
+    (IsColimit.ofIsoColimit hc
+      (Cocones.ext (ofCoconeObjIsoPt c).symm (fun ⟨i, hi⟩ ↦ by
+        dsimp
+        rw [ofCocone_map_to_top _ _ hi, Iso.inv_hom_id_assoc])))
+
+end Functor
+
+end CategoryTheory

From e0a256f8a699459ccdbd5ce3ef074a1a8087924e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Fri, 20 Dec 2024 19:57:55 +0100
Subject: [PATCH 21/28] Update
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean

---
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index a82672bb5e9c7..3392aa5965cd0 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -300,6 +300,6 @@ variable {J}
 lemma hasColimitOfShape_of_isSuccLimit [HasIterationOfShape C J] (j : J)
     (hj : Order.IsSuccLimit j) :
     HasColimitsOfShape (Set.Iio j) C :=
-    HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit j hj
+  HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit j hj
 
 end CategoryTheory

From fabd79fb3fbb26fe6ad473aa86debbbf734dae1a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 21 Dec 2024 12:20:05 +0100
Subject: [PATCH 22/28] fix docstrings

---
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index 3392aa5965cd0..fead154da0423 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -18,13 +18,14 @@ a category `Iteration ε j`. An object in this category consists of
 a functor `F : Set.Iic j ⥤ C ⥤ C` equipped with the data
 which makes it the `i`th-iteration of `Φ` for all `i` such that `i ≤ j`.
 Under suitable assumptions on `C`, we shall show that this category
-`Iteration ε j` is equivalent to the punctual category (TODO).
+`Iteration ε j` is equivalent to the punctual category.
 In this file, we show that the there is at most one morphism between
 two objects. In `SmallObject.Iteration.UniqueHom`, we shall show
 that there does always exist a unique morphism between
-two objects (TODO). Then, we shall show the existence of
-an object (TODO). In these proofs, which are all done using
-transfinite induction, we have to treat three cases separately:
+two objects. Then, we shall show the existence of
+an object in `SmallObject.Iteration.Nonempty`.
+In these proofs, which are all done using transfinite induction,
+we have to treat three cases separately:
 * the case `j = ⊥`;
 * the case `j` is a successor;
 * the case `j` is a limit element.

From 0a5f49b66e29033885523953fc55e52847b0d36a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 26 Dec 2024 02:25:16 +0100
Subject: [PATCH 23/28] wip

---
 .../SmallObject/Iteration/Basic.lean          | 320 ++++++++++++++----
 1 file changed, 253 insertions(+), 67 deletions(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index fead154da0423..b75c1e5ac3f75 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -8,7 +8,7 @@ import Mathlib.CategoryTheory.Limits.HasLimits
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.SuccPred.Limit
 
-/-! # Transfinite iterations of a functor
+/-! # Transfinite iterations of a construction
 
 In this file, given a functor `Φ : C ⥤ C` and a natural transformation
 `ε : 𝟭 C ⟶ Φ`, we shall define the transfinite iterations of `Φ` (TODO).
@@ -32,27 +32,71 @@ we have to treat three cases separately:
 
 -/
 
-universe u
+universe w v u
 
 namespace CategoryTheory
 
 open Category Limits
 
-variable {C : Type*} [Category C] {Φ : C ⥤ C} (ε : 𝟭 C ⟶ Φ) {J : Type u}
+variable {C : Type u} [Category.{v} C] {J : Type w}
 
-namespace Functor
+namespace SmallObject
 
-namespace Iteration
+section
+
+variable [Preorder J]
+
+variable (C J) in
+/-- A category `C` has iterations of shape `J` when certain shapes
+of colimits exists. When `J` is well ordered, this assumption is used in
+order to show that the category `Iteration ε j` is nonempty for any `j : J`,
+see the file `CategoryTheory.SmallObject.Nonempty`. -/
+class HasIterationOfShape : Prop where
+  hasColimitsOfShape_of_isSuccLimit (j : J) (hj : Order.IsSuccLimit j) :
+    HasColimitsOfShape (Set.Iio j) C := by infer_instance
+  hasColimitsOfShape : HasColimitsOfShape J C := by infer_instance
+
+attribute [instance] HasIterationOfShape.hasColimitsOfShape
 
-variable [Preorder J] {j : J} (F : Set.Iic j ⥤ C)
+variable (C) in
+lemma hasColimitOfShape_of_isSuccLimit [HasIterationOfShape C J] (j : J)
+    (hj : Order.IsSuccLimit j) :
+    HasColimitsOfShape (Set.Iio j) C :=
+  HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit j hj
+
+end
 
-/-- The map `F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩` when `F : Set.Iic j ⥤ C`
-and `i : J` is such that `i < j`. -/
-noncomputable abbrev mapSucc' [SuccOrder J] (i : J) (hi : i < j) :
-    F.obj ⟨i, hi.le⟩ ⟶ F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ :=
-  F.map <| homOfLE <| Subtype.mk_le_mk.2 <| Order.le_succ i
+variable (C) in
+/-- A successor structure () on a category consists of the
+data of an object `succ X` for any `X : C`, a map `toSucc X : X ⟶ toSucc X`
+(which does not need to be natural), and a zeroth object `X₀`.
+-/
+structure SuccStruct where
+  /-- the zeroth object -/
+  X₀ : C
+  /-- the successor of an object -/
+  succ (X : C) : C
+  /-- the map to the successor -/
+  toSucc (X : C) : X ⟶ succ X
+
+namespace SuccStruct
+
+/-- Given a functor `Φ : C ⥤ C`, a natural transformation of the form `𝟭 C ⟶ Φ`
+induces a successor structure. -/
+@[simps]
+def ofNatTrans {Φ : C ⥤ C} (ε : 𝟭 C ⟶ Φ) : SuccStruct (C ⥤ C) where
+  succ G := G ⋙ Φ
+  toSucc _ := whiskerLeft _ ε
+  X₀ := 𝟭 C
+
+lemma congr_toSucc (Φ : SuccStruct C) {X Y : C} (h : X = Y) :
+    Φ.toSucc X = eqToHom (by rw [h]) ≫ Φ.toSucc Y ≫ eqToHom (by rw [h]) := by
+  subst h
+  simp
+
+namespace Iteration
 
-variable {i : J} (hi : i ≤ j)
+variable [Preorder J] {j : J} (F : Set.Iic j ⥤ C) {i : J} (hi : i ≤ j)
 
 /-- The functor `Set.Iio i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C`
 when `i ≤ j`. -/
@@ -92,65 +136,226 @@ lemma restrictionLE_map {k₁ k₂ : Set.Iic i} (φ : k₁ ⟶ k₂) :
 
 end Iteration
 
-/-- The category of `j`th iterations of a functor `Φ` equipped with a natural
-transformation `ε : 𝟭 C ⟶ Φ`. An object consists of the data of all iterations
-of `Φ` for `i : J` such that `i ≤ j` (this is the field `F`). Such objects are
-equipped with data and properties which characterizes the iterations up to a unique
-isomorphism for the three types of elements: `⊥`, successors, limit elements. -/
-structure Iteration [Preorder J] [OrderBot J] [SuccOrder J] (j : J) where
+variable (Φ : SuccStruct C) [LinearOrder J] [OrderBot J] [SuccOrder J]
+    [HasIterationOfShape C J]
+
+/-- The category of `j`th iterations of a succesor structure `Φ : SuccStruct C`.
+An object consists of the data of all iterations of `Φ` for `i : J` such
+that `i ≤ j` (this is the field `F`). Such objects are
+equipped with data and properties which characterizes uniquely the iterations
+on three types of elements: `⊥`, successors, limit elements. -/
+@[ext]
+structure Iteration [WellFoundedLT J] (j : J) where
   /-- The data of all `i`th iterations for `i : J` such that `i ≤ j`. -/
-  F : Set.Iic j ⥤ C ⥤ C
-  /-- The zeroth iteration is the identity functor. -/
-  isoZero : F.obj ⟨⊥, bot_le⟩ ≅ 𝟭 C
-  /-- The iteration on a successor element is obtained by composition of
-  the previous iteration with `Φ`. -/
-  isoSucc (i : J) (hi : i < j) : F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ ≅ F.obj ⟨i, hi.le⟩ ⋙ Φ
-  /-- The natural map from an iteration to its successor is induced by `ε`. -/
-  mapSucc'_eq (i : J) (hi : i < j) :
-    Iteration.mapSucc' F i hi = whiskerLeft _ ε ≫ (isoSucc i hi).inv
+  F : Set.Iic j ⥤ C
+  /-- The zeroth iteration is the zeroth object . -/
+  obj_bot : F.obj ⟨⊥, bot_le⟩ = Φ.X₀
+  /-- The iteration on a successor element identifies to the successor. -/
+  obj_succ (i : J) (hi : i < j) :
+    F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ = Φ.succ (F.obj ⟨i, hi.le⟩)
+  /-- The natural map from an iteration to its successor is induced by `toSucc`. -/
+  map_succ (i : J) (hi : i < j) :
+    F.map (homOfLE (Order.le_succ i) : ⟨i, hi.le⟩ ⟶ ⟨Order.succ i, Order.succ_le_of_lt hi⟩) =
+      Φ.toSucc _ ≫ eqToHom (by rw [obj_succ _ hi])
   /-- If `i` is a limit element, the `i`th iteration is the colimit
   of `k`th iterations for `k < i`. -/
-  isColimit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) :
-    IsColimit (Iteration.coconeOfLE F hij)
+  obj_limit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) :
+    letI := hasColimitOfShape_of_isSuccLimit C i hi
+    F.obj ⟨i, hij⟩ = colimit (Iteration.restrictionLT F hij)
+  map_eq_ι (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j)
+      (k : J) (hk : k < i) :
+    letI := hasColimitOfShape_of_isSuccLimit C i hi
+    F.map (homOfLE hk.le : ⟨k, hk.le.trans hij⟩ ⟶ ⟨i, hij⟩) =
+      colimit.ι (Iteration.restrictionLT F hij) ⟨k, hk⟩ ≫
+        eqToHom (by rw [obj_limit i hi])
+
+variable [WellFoundedLT J]
 
 namespace Iteration
 
-variable {ε}
+variable {Φ}
 variable {j : J}
 
 section
 
-variable [Preorder J] [OrderBot J] [SuccOrder J] (iter : Φ.Iteration ε j)
+variable  (iter : Φ.Iteration j)
+
+def isoBot : iter.F.obj ⟨⊥, bot_le⟩ ≅ Φ.X₀ :=
+  eqToIso (by rw [obj_bot])
+
+def isoSucc (i : J) (hi : i < j) :
+    iter.F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ ≅
+      Φ.succ (iter.F.obj ⟨i, hi.le⟩) :=
+  eqToIso (by rw [obj_succ _ i hi])
+
+/-- Variant of `map_succ'` involving the isomorphism `isoSucc`. -/
+lemma map_succ' (i : J) (hi : i < j) :
+    iter.F.map (homOfLE (Order.le_succ i) :
+        ⟨i, hi.le⟩ ⟶ ⟨Order.succ i, Order.succ_le_of_lt hi⟩) =
+      Φ.toSucc _ ≫ (iter.isoSucc i hi).inv :=
+  iter.map_succ i hi
+
+noncomputable def isColimit (i : J)
+    (hi : Order.IsSuccLimit i) (hij : i ≤ j) :
+    IsColimit (Iteration.coconeOfLE iter.F hij) := by
+  have := hasColimitOfShape_of_isSuccLimit C i hi
+  exact IsColimit.ofIsoColimit (colimit.isColimit _)
+    (Cocones.ext (eqToIso (iter.obj_limit i hi hij).symm)
+    (fun ⟨k, hk⟩ ↦ (iter.map_eq_ι i hi hij k hk).symm))
+
+@[simps F]
+def trunc (iter : Φ.Iteration j) {i : J} (hi : i ≤ j) : Φ.Iteration i where
+  F := restrictionLE iter.F hi
+  obj_bot := iter.obj_bot
+  obj_succ k hk := iter.obj_succ k (lt_of_lt_of_le hk hi)
+  obj_limit k hk hk' := iter.obj_limit k hk (hk'.trans hi)
+  map_succ k hk := iter.map_succ k (lt_of_lt_of_le hk hi)
+  map_eq_ι k hk hki l hl := iter.map_eq_ι k hk (hki.trans hi) l hl
 
-/-- For `iter : Φ.Iteration.ε j`, this is the map
-`iter.F.obj ⟨i, _⟩ ⟶ iter.F.obj ⟨Order.succ i, _⟩` if `i : J` is such that `i < j`. -/
-noncomputable abbrev mapSucc (i : J) (hi : i < j) :
-    iter.F.obj ⟨i, hi.le⟩ ⟶ iter.F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ :=
-  mapSucc' iter.F i hi
+end
 
-lemma mapSucc_eq (i : J) (hi : i < j) :
-    iter.mapSucc i hi = whiskerLeft _ ε ≫ (iter.isoSucc i hi).inv :=
-  iter.mapSucc'_eq _ hi
+namespace subsingleton
 
-end
+variable {F G : Set.Iic j ⥤ C} (hobj : F.obj = G.obj)
 
-section
+omit [OrderBot J] [SuccOrder J] [WellFoundedLT J]
+
+def MapEq (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j) : Prop :=
+  F.map (homOfLE h₁₂ : ⟨i₁, h₁₂.trans h₂⟩ ⟶ ⟨i₂, h₂⟩) =
+    eqToHom (by rw [hobj]) ≫
+      G.map (homOfLE h₁₂ : ⟨i₁, _⟩ ⟶ ⟨i₂, _⟩) ≫ eqToHom (by rw [hobj])
+
+def mapEq_of_eq {k : J} (hkj : k ≤ j) (h : restrictionLE F hkj = restrictionLE G hkj)
+    (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ k) :
+    MapEq hobj i₁ i₂ h₁₂ (h₂.trans hkj) := by
+  exact Functor.congr_hom h (homOfLE h₁₂ : ⟨i₁, h₁₂.trans h₂⟩ ⟶ ⟨i₂, h₂⟩)
+
+lemma congr_colimit_ι {F G : Set.Iio j ⥤ C} (h : F = G) (hj : Order.IsSuccLimit j)
+    (i : Set.Iio j) :
+    letI := hasColimitOfShape_of_isSuccLimit C j hj
+    colimit.ι F i = by
+      refine eqToHom (by rw [h]) ≫ colimit.ι G i ≫ eqToHom (by rw [h]) := by
+  subst h
+  simp
+
+omit [HasIterationOfShape C J]
+
+lemma mapEq_rfl (i : J) (h : i ≤ j) : MapEq hobj i i (by simp) h := by
+  simp [MapEq]
+
+variable {hobj} in
+lemma mapEq_trans {i₁ i₂ i₃ : J} (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) {h₃ : i₃ ≤ j}
+    (m₁₂ : MapEq hobj i₁ i₂ h₁₂ (h₂₃.trans h₃)) (m₂₃ : MapEq hobj i₂ i₃ h₂₃ h₃) :
+    MapEq hobj i₁ i₃ (h₁₂.trans h₂₃) h₃ := by
+  dsimp [MapEq] at m₁₂ m₂₃ ⊢
+  rw [← homOfLE_comp (X := Set.Iic j) (x := ⟨i₁, _⟩)
+    (y := ⟨i₂, h₂₃.trans h₃⟩) (z := ⟨i₃, _⟩) h₁₂ h₂₃, Functor.map_comp,
+    Functor.map_comp, m₁₂, m₂₃]
+  simp
+
+lemma functor_eq (hmap : ∀ (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j), MapEq hobj i₁ i₂ h₁₂ h₂) :
+    F = G :=
+  Functor.ext (by simp [hobj]) (by
+    rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f
+    exact hmap i₁ i₂ (leOfHom f) h₂)
+
+end subsingleton
+
+open subsingleton in
+instance subsingleton : Subsingleton (Φ.Iteration j) where
+  allEq iter₁ iter₂ := by
+    suffices iter₁.F = iter₂.F by aesop
+    revert iter₁ iter₂
+    induction j using SuccOrder.limitRecOn with
+    | hm j h =>
+        intro iter₁ iter₂
+        obtain rfl := h.eq_bot
+        fapply Functor.ext
+        · rintro ⟨i, hi⟩
+          obtain rfl : i = ⊥ := by simpa using hi
+          simp only [obj_bot]
+        · rintro ⟨i, hi⟩ ⟨i', hi'⟩ f
+          obtain rfl : i = ⊥ := by simpa using hi
+          obtain rfl : i' = ⊥ := by simpa using hi'
+          obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
+          simp
+    | hs j hj₁ hj₂ =>
+        intro iter₁ iter₂
+        have hobj : iter₁.F.obj = iter₂.F.obj := by
+          ext ⟨i, hi⟩
+          wlog h : i ≤ j generalizing i
+          · obtain hi | rfl := hi.lt_or_eq
+            · exact this _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).mp hi)
+            · simp only [obj_succ _ _ (Order.lt_succ_of_not_isMax hj₁), this _ _ (by rfl)]
+          exact Functor.congr_obj (hj₂ (iter₁.trunc (Order.le_succ _))
+            (iter₂.trunc (Order.le_succ _))) ⟨i, h⟩
+        have hsucc : MapEq hobj _ _ (Order.le_succ j) (by simp) := by
+          simp only [MapEq, map_succ _ _ (Order.lt_succ_of_not_isMax hj₁),
+            Φ.congr_toSucc (congr_fun hobj ⟨j, _⟩), assoc, eqToHom_trans]
+        apply functor_eq hobj
+        intro i₁ i₂
+        wlog hi₂ : i₂ ≤ j generalizing i₂
+        · intro h₁₂ h₂
+          obtain h₂ | rfl := h₂.lt_or_eq
+          · exact (hi₂ ((Order.lt_succ_iff_of_not_isMax hj₁).mp h₂)).elim
+          · by_cases hi₁ : i₁ ≤ j
+            · exact mapEq_trans _ _ (this j (by simp) hi₁ (Order.le_succ j)) hsucc
+            · obtain rfl : i₁ = Order.succ j :=
+                le_antisymm h₁₂ ((Order.succ_le_iff_of_not_isMax hj₁).mpr (by simpa using hi₁))
+              apply mapEq_rfl
+        intro h₁₂ h₂
+        exact mapEq_of_eq hobj (Order.le_succ j)
+          (hj₂ (iter₁.trunc (Order.le_succ j)) (iter₂.trunc (Order.le_succ j))) _ _ _ hi₂
+    | hl j h₁ h₂ =>
+        intro iter₁ iter₂
+        have hobj : iter₁.F.obj = iter₂.F.obj := by
+          ext ⟨i, hi⟩
+          wlog h : i < j generalizing i
+          · obtain rfl : j = i := le_antisymm (by simpa using h) hi
+            simp only [obj_limit _ _ h₁]
+            congr 1
+            fapply Functor.ext
+            · rintro ⟨i, hi⟩
+              exact this _ _ hi
+            · rintro ⟨i₁, hi₁⟩ ⟨i₂, hi₂⟩ f
+              exact Functor.congr_hom (h₂ i₂ hi₂ (iter₁.trunc hi₂.le) (iter₂.trunc hi₂.le))
+                (homOfLE (leOfHom f) : ⟨i₁, leOfHom f⟩ ⟶ ⟨i₂, by simp⟩)
+          exact Functor.congr_obj (h₂ i h (iter₁.trunc h.le) (iter₂.trunc h.le)) ⟨i, by simp⟩
+        apply functor_eq hobj
+        intro i₁ i₂ h₁₂ hi₂
+        by_cases h₃ : i₂ < j
+        · exact mapEq_of_eq hobj hi₂
+            (h₂ _ h₃ (iter₁.trunc h₃.le) (iter₂.trunc h₃.le)) _ _ _ (by rfl)
+        · obtain rfl : j = i₂ := le_antisymm (by simpa using h₃) hi₂
+          by_cases h₄ : i₁ < j
+          · dsimp [MapEq]
+            have : restrictionLT iter₁.F hi₂ = restrictionLT iter₂.F hi₂ :=
+              Functor.ext (fun k ↦ congr_fun hobj ⟨k.1, k.2.le⟩) (by
+                rintro ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f
+                exact Functor.congr_hom (h₂ k₂ hk₂ (iter₁.trunc hk₂.le) (iter₂.trunc hk₂.le))
+                  (homOfLE (leOfHom f) : ⟨k₁, leOfHom f⟩ ⟶ ⟨k₂, by simp⟩))
+            simp only [map_eq_ι _ _ h₁ _ _ h₄, assoc, eqToHom_trans,
+              congr_colimit_ι this h₁]
+          · obtain rfl : i₁ = j := le_antisymm h₁₂ (by simpa using h₄)
+            exact mapEq_rfl hobj i₁ hi₂
+
+
+#exit
 
-variable [Preorder J] [OrderBot J] [SuccOrder J] (iter₁ iter₂ : Φ.Iteration ε j)
 
 /-- A morphism between two objects `iter₁` and `iter₂` in the
-category `Φ.Iteration ε j` of `j`th iterations of a functor `Φ`
-equipped with a natural transformation `ε : 𝟭 C ⟶ Φ` consists of a natural
-transformation `natTrans : iter₁.F ⟶ iter₂.F` which is compatible with the
-isomorphisms `isoZero` and `isoSucc`. -/
+category `Φ.Iteration ε j` of `j`th iterations of a successor structure
+consists of a natural transformation `natTrans : iter₁.F ⟶ iter₂.F` which
+is compatible with the isomorphisms `isoZero` and `isoSucc`. -/
 structure Hom where
   /-- A natural transformation `iter₁.F ⟶ iter₂.F` -/
   natTrans : iter₁.F ⟶ iter₂.F
   natTrans_app_zero :
     natTrans.app ⟨⊥, bot_le⟩ = iter₁.isoZero.hom ≫ iter₂.isoZero.inv := by aesop_cat
   natTrans_app_succ (i : J) (hi : i < j) :
-    natTrans.app ⟨Order.succ i, Order.succ_le_of_lt hi⟩ = (iter₁.isoSucc i hi).hom ≫
-      whiskerRight (natTrans.app ⟨i, hi.le⟩) _ ≫ (iter₂.isoSucc i hi).inv := by aesop_cat
+    sorry
+    --natTrans.app ⟨Order.succ i, Order.succ_le_of_lt hi⟩ = (iter₁.isoSucc i hi).hom ≫
+    --  (natTrans.app ⟨i, hi.le⟩) _ ≫ (iter₂.isoSucc i hi).inv := by aesop_cat
 
 namespace Hom
 
@@ -283,24 +488,5 @@ end Functor
 
 open Limits
 
-variable (C J) [Preorder J]
-
-/-- A category `C` has iterations of shape `J` when certain shapes
-of colimits exists. When `J` is well ordered, this assumption is used in
-order to show that the category `Iteration ε j` is nonempty for any `j : J`,
-see the file `CategoryTheory.SmallObject.Nonempty`. -/
-class HasIterationOfShape : Prop where
-  hasColimitsOfShape_of_isSuccLimit (j : J) (hj : Order.IsSuccLimit j) :
-    HasColimitsOfShape (Set.Iio j) C := by infer_instance
-  hasColimitsOfShape : HasColimitsOfShape J C := by infer_instance
-
-attribute [instance] HasIterationOfShape.hasColimitsOfShape
-
-variable {J}
-
-lemma hasColimitOfShape_of_isSuccLimit [HasIterationOfShape C J] (j : J)
-    (hj : Order.IsSuccLimit j) :
-    HasColimitsOfShape (Set.Iio j) C :=
-  HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit j hj
 
 end CategoryTheory

From faf9569ff817c2d0ea38e1d6c17797c114d14c30 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 26 Dec 2024 14:48:50 +0100
Subject: [PATCH 24/28] refactor(CategoryTheory/SmallObject): better
 definitions

---
 .../SmallObject/Iteration/Basic.lean          | 329 +++++---------
 .../SmallObject/Iteration/ExtendToSucc.lean   |  26 +-
 .../Iteration/FunctorOfCocone.lean            |  14 +-
 .../SmallObject/Iteration/Iteration.lean      |  57 +++
 .../SmallObject/Iteration/Nonempty.lean       | 402 ++++++++++--------
 5 files changed, 410 insertions(+), 418 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/SmallObject/Iteration/Iteration.lean

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index b75c1e5ac3f75..cfffa3581fcb1 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -10,25 +10,43 @@ import Mathlib.Order.SuccPred.Limit
 
 /-! # Transfinite iterations of a construction
 
-In this file, given a functor `Φ : C ⥤ C` and a natural transformation
-`ε : 𝟭 C ⟶ Φ`, we shall define the transfinite iterations of `Φ` (TODO).
-
-Given `j : J` where `J` is a well ordered set, we first introduce
-a category `Iteration ε j`. An object in this category consists of
-a functor `F : Set.Iic j ⥤ C ⥤ C` equipped with the data
-which makes it the `i`th-iteration of `Φ` for all `i` such that `i ≤ j`.
-Under suitable assumptions on `C`, we shall show that this category
-`Iteration ε j` is equivalent to the punctual category.
-In this file, we show that the there is at most one morphism between
-two objects. In `SmallObject.Iteration.UniqueHom`, we shall show
-that there does always exist a unique morphism between
-two objects. Then, we shall show the existence of
-an object in `SmallObject.Iteration.Nonempty`.
-In these proofs, which are all done using transfinite induction,
-we have to treat three cases separately:
-* the case `j = ⊥`;
-* the case `j` is a successor;
-* the case `j` is a limit element.
+In this file, we introduce the structure `SuccStruct` on a category `C`.
+It consists of the data of an object `X₀ : C`, a successor map `succ : C → C`
+and a morphism `toSucc : X ⟶ succ X` for any `X : C`. The map `toSucc`
+does not have to be natural in `X`. For any element `j : J` in
+well-ordered type `J`, we would like to define
+the iteration of `Φ : SuccStruct C`, as a functor `F : J ⥤ C`
+such that `F.obj ⊥ = X₀`, `F.obj j ⟶ F.obj (Order.succ j)` is `toSucc (F.obj j)`
+when `j` is not maximal, and when `j` is limit, `F.obj j` should be the
+colimit of the `F.obj k` for `k < j`.
+
+In the small object argument, we shall apply this to the iteration of
+a functor `F : C ⥤ C` equipped with a natural transformation `ε : 𝟭 C ⟶ F`:
+this will correspond to the case of
+`SuccStruct.ofTrans ε : SuccStruct (C ⥤ C)`, for which `X₀ := 𝟭 C`,
+`succ G := G ⋙ F` and `toSucc G : G ⟶ G ⋙ F` is given by `whiskerLeft G ε`.
+
+The construction of the iteration of `Φ : SuccStruct C` is done
+by transfinite induction. However, for a limit element `j : J`,
+the definition of `F.obj j` does not involve only
+the objects `F.obj i` for `i < j`, but it also
+involves the maps `F.obj i₁ ⟶ F.obj i₂` for `i₁ ≤ i₂ < j`.
+Then, this is a straightforward application of definitions by
+transfinite induction. In order to solve this technical difficulty,
+we introduce a structure `Φ.Iteration j` for any `j : J`. This
+structure contains all the expected data and properties for
+all the indices that are `≤ j`. In this file, we show that
+`Φ.Iteration j` is a subsingleton. The uniqueness shall ne
+obtained in the file `SmallObject.Iteration.Nonempty`, and
+the construction of the functor `Φ.iterationFunctor J : J ⥤ C`
+and of its colimit `Φ.iteration J : C` is done in the
+file `SmallObject.Iteration.Iteration`.
+
+The map `Φ.toSucc X : X ⟶ Φ.succ X` does not have to be natural
+(and it is not in certain applications). Then, two isomorphic
+objects `X` and `Y` may have non isomorphic successors. This is
+the reason why we make an extensive use of equalities of objects
+in the definitions.
 
 -/
 
@@ -44,6 +62,48 @@ namespace SmallObject
 
 section
 
+variable [Preorder J] {j : J} (F : Set.Iic j ⥤ C) {i : J} (hi : i ≤ j)
+
+/-- The functor `Set.Iio i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C`
+when `i ≤ j`. -/
+def restrictionLT : Set.Iio i ⥤ C :=
+  (monotone_inclusion_lt_le_of_le hi).functor ⋙ F
+
+@[simp]
+lemma restrictionLT_obj (k : J) (hk : k < i) :
+    (restrictionLT F hi).obj ⟨k, hk⟩ = F.obj ⟨k, hk.le.trans hi⟩ := rfl
+
+@[simp]
+lemma restrictionLT_map {k₁ k₂ : Set.Iio i} (φ : k₁ ⟶ k₂) :
+    (restrictionLT F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl
+
+/-- Given `F : Set.Iic j ⥤ C`, `i : J` such that `hi : i ≤ j`, this is the
+cocone consisting of all maps `F.obj ⟨k, hk⟩ ⟶ F.obj ⟨i, hi⟩` for `k : J` such that `k < i`. -/
+@[simps]
+def coconeOfLE : Cocone (restrictionLT F hi) where
+  pt := F.obj ⟨i, hi⟩
+  ι :=
+    { app := fun ⟨k, hk⟩ => F.map (homOfLE (by simpa using hk.le))
+      naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ _ => by
+        simp [comp_id, ← Functor.map_comp, homOfLE_comp] }
+
+/-- The functor `Set.Iic i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C`
+when `i ≤ j`. -/
+def restrictionLE : Set.Iic i ⥤ C :=
+  (monotone_inclusion_le_le_of_le hi).functor ⋙ F
+
+@[simp]
+lemma restrictionLE_obj (k : J) (hk : k ≤ i) :
+    (restrictionLE F hi).obj ⟨k, hk⟩ = F.obj ⟨k, hk.trans hi⟩ := rfl
+
+@[simp]
+lemma restrictionLE_map {k₁ k₂ : Set.Iic i} (φ : k₁ ⟶ k₂) :
+    (restrictionLE F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl
+
+end
+
+section
+
 variable [Preorder J]
 
 variable (C J) in
@@ -84,9 +144,9 @@ namespace SuccStruct
 /-- Given a functor `Φ : C ⥤ C`, a natural transformation of the form `𝟭 C ⟶ Φ`
 induces a successor structure. -/
 @[simps]
-def ofNatTrans {Φ : C ⥤ C} (ε : 𝟭 C ⟶ Φ) : SuccStruct (C ⥤ C) where
-  succ G := G ⋙ Φ
-  toSucc _ := whiskerLeft _ ε
+def ofNatTrans {F : C ⥤ C} (ε : 𝟭 C ⟶ F) : SuccStruct (C ⥤ C) where
+  succ G := G ⋙ F
+  toSucc G := whiskerLeft G ε
   X₀ := 𝟭 C
 
 lemma congr_toSucc (Φ : SuccStruct C) {X Y : C} (h : X = Y) :
@@ -94,48 +154,6 @@ lemma congr_toSucc (Φ : SuccStruct C) {X Y : C} (h : X = Y) :
   subst h
   simp
 
-namespace Iteration
-
-variable [Preorder J] {j : J} (F : Set.Iic j ⥤ C) {i : J} (hi : i ≤ j)
-
-/-- The functor `Set.Iio i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C`
-when `i ≤ j`. -/
-def restrictionLT : Set.Iio i ⥤ C :=
-  (monotone_inclusion_lt_le_of_le hi).functor ⋙ F
-
-@[simp]
-lemma restrictionLT_obj (k : J) (hk : k < i) :
-    (restrictionLT F hi).obj ⟨k, hk⟩ = F.obj ⟨k, hk.le.trans hi⟩ := rfl
-
-@[simp]
-lemma restrictionLT_map {k₁ k₂ : Set.Iio i} (φ : k₁ ⟶ k₂) :
-    (restrictionLT F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl
-
-/-- Given `F : Set.Iic j ⥤ C`, `i : J` such that `hi : i ≤ j`, this is the
-cocone consisting of all maps `F.obj ⟨k, hk⟩ ⟶ F.obj ⟨i, hi⟩` for `k : J` such that `k < i`. -/
-@[simps]
-def coconeOfLE : Cocone (restrictionLT F hi) where
-  pt := F.obj ⟨i, hi⟩
-  ι :=
-    { app := fun ⟨k, hk⟩ => F.map (homOfLE (by simpa using hk.le))
-      naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ _ => by
-        simp [comp_id, ← Functor.map_comp, homOfLE_comp] }
-
-/-- The functor `Set.Iic i ⥤ C` obtained by "restriction" of `F : Set.Iic j ⥤ C`
-when `i ≤ j`. -/
-def restrictionLE : Set.Iic i ⥤ C :=
-  (monotone_inclusion_le_le_of_le hi).functor ⋙ F
-
-@[simp]
-lemma restrictionLE_obj (k : J) (hk : k ≤ i) :
-    (restrictionLE F hi).obj ⟨k, hk⟩ = F.obj ⟨k, hk.trans hi⟩ := rfl
-
-@[simp]
-lemma restrictionLE_map {k₁ k₂ : Set.Iic i} (φ : k₁ ⟶ k₂) :
-    (restrictionLE F hi).map φ = F.map (homOfLE (by simpa using leOfHom φ)) := rfl
-
-end Iteration
-
 variable (Φ : SuccStruct C) [LinearOrder J] [OrderBot J] [SuccOrder J]
     [HasIterationOfShape C J]
 
@@ -161,12 +179,12 @@ structure Iteration [WellFoundedLT J] (j : J) where
   of `k`th iterations for `k < i`. -/
   obj_limit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) :
     letI := hasColimitOfShape_of_isSuccLimit C i hi
-    F.obj ⟨i, hij⟩ = colimit (Iteration.restrictionLT F hij)
+    F.obj ⟨i, hij⟩ = colimit (restrictionLT F hij)
   map_eq_ι (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j)
       (k : J) (hk : k < i) :
     letI := hasColimitOfShape_of_isSuccLimit C i hi
     F.map (homOfLE hk.le : ⟨k, hk.le.trans hij⟩ ⟶ ⟨i, hij⟩) =
-      colimit.ι (Iteration.restrictionLT F hij) ⟨k, hk⟩ ≫
+      colimit.ι (restrictionLT F hij) ⟨k, hk⟩ ≫
         eqToHom (by rw [obj_limit i hi])
 
 variable [WellFoundedLT J]
@@ -178,11 +196,14 @@ variable {j : J}
 
 section
 
-variable  (iter : Φ.Iteration j)
+variable (iter : Φ.Iteration j)
 
+/-- The isomorphism `iter.F.obj ⟨⊥, bot_le⟩ ≅ Φ.X₀`. -/
 def isoBot : iter.F.obj ⟨⊥, bot_le⟩ ≅ Φ.X₀ :=
   eqToIso (by rw [obj_bot])
 
+/-- The object `iter.F.obj ⟨Order.succ i, _⟩` identifies to
+the successor of `iter.F.obj ⟨i, _⟩` when `i < j`. -/
 def isoSucc (i : J) (hi : i < j) :
     iter.F.obj ⟨Order.succ i, Order.succ_le_of_lt hi⟩ ≅
       Φ.succ (iter.F.obj ⟨i, hi.le⟩) :=
@@ -195,9 +216,11 @@ lemma map_succ' (i : J) (hi : i < j) :
       Φ.toSucc _ ≫ (iter.isoSucc i hi).inv :=
   iter.map_succ i hi
 
+/-- When `i : J` is limit, `iter.F.obj ⟨i, _⟩` identifies
+to the colimit of the restriction of `iter.F` to `Set.Iio i`. -/
 noncomputable def isColimit (i : J)
     (hi : Order.IsSuccLimit i) (hij : i ≤ j) :
-    IsColimit (Iteration.coconeOfLE iter.F hij) := by
+    IsColimit (coconeOfLE iter.F hij) := by
   have := hasColimitOfShape_of_isSuccLimit C i hi
   exact IsColimit.ofIsoColimit (colimit.isColimit _)
     (Cocones.ext (eqToIso (iter.obj_limit i hi hij).symm)
@@ -214,6 +237,17 @@ def trunc (iter : Φ.Iteration j) {i : J} (hi : i ≤ j) : Φ.Iteration i where
 
 end
 
+omit [OrderBot J] [SuccOrder J] [WellFoundedLT J] in
+lemma congr_colimit_ι {F G : Set.Iio j ⥤ C} (h : F = G) (hj : Order.IsSuccLimit j)
+    (i : Set.Iio j) :
+    letI := hasColimitOfShape_of_isSuccLimit C j hj
+    colimit.ι F i = by
+      refine eqToHom (by rw [h]) ≫ colimit.ι G i ≫ eqToHom (by rw [h]) := by
+  subst h
+  simp
+
+/-! Auxiliary definitions for the proof of `Subsingleton (Φ.Iteration j)`. -/
+
 namespace subsingleton
 
 variable {F G : Set.Iic j ⥤ C} (hobj : F.obj = G.obj)
@@ -225,19 +259,12 @@ def MapEq (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j) : Prop :
     eqToHom (by rw [hobj]) ≫
       G.map (homOfLE h₁₂ : ⟨i₁, _⟩ ⟶ ⟨i₂, _⟩) ≫ eqToHom (by rw [hobj])
 
-def mapEq_of_eq {k : J} (hkj : k ≤ j) (h : restrictionLE F hkj = restrictionLE G hkj)
+omit [HasIterationOfShape C J] in
+lemma mapEq_of_eq {k : J} (hkj : k ≤ j) (h : restrictionLE F hkj = restrictionLE G hkj)
     (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ k) :
     MapEq hobj i₁ i₂ h₁₂ (h₂.trans hkj) := by
   exact Functor.congr_hom h (homOfLE h₁₂ : ⟨i₁, h₁₂.trans h₂⟩ ⟶ ⟨i₂, h₂⟩)
 
-lemma congr_colimit_ι {F G : Set.Iio j ⥤ C} (h : F = G) (hj : Order.IsSuccLimit j)
-    (i : Set.Iio j) :
-    letI := hasColimitOfShape_of_isSuccLimit C j hj
-    colimit.ι F i = by
-      refine eqToHom (by rw [h]) ≫ colimit.ι G i ≫ eqToHom (by rw [h]) := by
-  subst h
-  simp
-
 omit [HasIterationOfShape C J]
 
 lemma mapEq_rfl (i : J) (h : i ≤ j) : MapEq hobj i i (by simp) h := by
@@ -339,154 +366,10 @@ instance subsingleton : Subsingleton (Φ.Iteration j) where
           · obtain rfl : i₁ = j := le_antisymm h₁₂ (by simpa using h₄)
             exact mapEq_rfl hobj i₁ hi₂
 
-
-#exit
-
-
-/-- A morphism between two objects `iter₁` and `iter₂` in the
-category `Φ.Iteration ε j` of `j`th iterations of a successor structure
-consists of a natural transformation `natTrans : iter₁.F ⟶ iter₂.F` which
-is compatible with the isomorphisms `isoZero` and `isoSucc`. -/
-structure Hom where
-  /-- A natural transformation `iter₁.F ⟶ iter₂.F` -/
-  natTrans : iter₁.F ⟶ iter₂.F
-  natTrans_app_zero :
-    natTrans.app ⟨⊥, bot_le⟩ = iter₁.isoZero.hom ≫ iter₂.isoZero.inv := by aesop_cat
-  natTrans_app_succ (i : J) (hi : i < j) :
-    sorry
-    --natTrans.app ⟨Order.succ i, Order.succ_le_of_lt hi⟩ = (iter₁.isoSucc i hi).hom ≫
-    --  (natTrans.app ⟨i, hi.le⟩) _ ≫ (iter₂.isoSucc i hi).inv := by aesop_cat
-
-namespace Hom
-
-attribute [simp, reassoc] natTrans_app_zero
-
-/-- The identity morphism in the category `Φ.Iteration ε j`. -/
-@[simps]
-def id : Hom iter₁ iter₁ where
-  natTrans := 𝟙 _
-
-variable {iter₁ iter₂}
-
--- Note: this is not made a global ext lemma because it is shown below
--- that the type of morphisms is a subsingleton.
-lemma ext' {f g : Hom iter₁ iter₂} (h : f.natTrans = g.natTrans) : f = g := by
-  cases f
-  cases g
-  subst h
-  rfl
-
-attribute [local ext] ext'
-
-/-- The composition of morphisms in the category `Iteration ε j`. -/
-@[simps]
-def comp {iter₃ : Iteration ε j} (f : Hom iter₁ iter₂) (g : Hom iter₂ iter₃) :
-    Hom iter₁ iter₃ where
-  natTrans := f.natTrans ≫ g.natTrans
-  natTrans_app_succ i hi := by simp [natTrans_app_succ _ _ hi]
-
-instance : Category (Iteration ε j) where
-  Hom := Hom
-  id := id
-  comp := comp
-
-instance {J} {j : J} [PartialOrder J] [OrderBot J] [WellFoundedLT J] [SuccOrder J]
-    {iter₁ iter₂ : Iteration ε j} :
-    Subsingleton (iter₁ ⟶ iter₂) where
-  allEq f g := by
-    apply ext'
-    suffices ∀ i hi, f.natTrans.app ⟨i, hi⟩ = g.natTrans.app ⟨i, hi⟩ by
-      ext ⟨i, hi⟩ : 2
-      apply this
-    intro i
-    induction i using SuccOrder.limitRecOn with
-    | hm j H =>
-      obtain rfl := H.eq_bot
-      simp [natTrans_app_zero]
-    | hs j H IH =>
-      intro hj
-      simp [Hom.natTrans_app_succ, IH, (Order.lt_succ_of_not_isMax H).trans_le hj]
-    | hl j H IH =>
-      refine fun hj ↦ (iter₁.isColimit j H hj).hom_ext ?_
-      rintro ⟨k, hk⟩
-      simp [IH k hk]
-
-end Hom
-
-@[simp]
-lemma natTrans_id : Hom.natTrans (𝟙 iter₁) = 𝟙 _ := rfl
-
-variable {iter₁ iter₂}
-
-@[simp, reassoc]
-lemma natTrans_comp {iter₃ : Iteration ε j} (φ : iter₁ ⟶ iter₂) (ψ : iter₂ ⟶ iter₃) :
-    (φ ≫ ψ).natTrans = φ.natTrans ≫ ψ.natTrans := rfl
-
-@[reassoc]
-lemma natTrans_naturality (φ : iter₁ ⟶ iter₂) (i₁ i₂ : J) (h : i₁ ≤ i₂) (h' : i₂ ≤ j) :
-    iter₁.F.map (by exact homOfLE h) ≫ φ.natTrans.app ⟨i₂, h'⟩ =
-      φ.natTrans.app ⟨i₁, h.trans h'⟩ ≫ iter₂.F.map (by exact homOfLE h) := by
-  apply φ.natTrans.naturality
-
-variable (ε) in
-/-- The evaluation functor `Iteration ε j ⥤ C ⥤ C` at `i : J` when `i ≤ j`. -/
-@[simps]
-def eval {i : J} (hi : i ≤ j) : Iteration ε j ⥤ C ⥤ C where
-  obj iter := iter.F.obj ⟨i, hi⟩
-  map φ := φ.natTrans.app _
-
-/-- Given `iter : Iteration ε j` and `i : J` such that `i ≤ j`, this is the
-induced element in `Iteration ε i`. -/
-@[simps F isoZero isoSucc]
-def trunc (iter : Iteration ε j) {i : J} (hi : i ≤ j) : Iteration ε i where
-  F := restrictionLE iter.F hi
-  isoZero := iter.isoZero
-  isoSucc k hk := iter.isoSucc k (lt_of_lt_of_le hk hi)
-  mapSucc'_eq k hk := iter.mapSucc'_eq k (lt_of_lt_of_le hk hi)
-  isColimit k hk' hk := iter.isColimit k hk' (hk.trans hi)
-
-@[simp]
-lemma trunc_refl (iter : Iteration ε j) :
-    iter.trunc (Preorder.le_refl j) = iter := rfl
-
-@[simp]
-lemma trunc_trunc (iter : Iteration ε j) {i : J} (hi : i ≤ j) {k : J} (hk : k ≤ i) :
-    (iter.trunc hi).trunc hk = iter.trunc (hk.trans hi) := rfl
-
-variable (ε) in
-/-- The truncation functor `Iteration ε j ⥤ Iteration ε i` when `i ≤ j`. -/
-@[simps obj]
-def truncFunctor {i : J} (hi : i ≤ j) : Iteration ε j ⥤ Iteration ε i where
-  obj iter := iter.trunc hi
-  map {iter₁ iter₂} φ :=
-    { natTrans := whiskerLeft _ φ.natTrans
-      natTrans_app_succ := fun k hk => φ.natTrans_app_succ k (lt_of_lt_of_le hk hi) }
-
-@[simp]
-lemma truncFunctor_map_natTrans_app
-    (φ : iter₁ ⟶ iter₂) {i : J} (hi : i ≤ j) (k : J) (hk : k ≤ i) :
-    ((truncFunctor ε hi).map φ).natTrans.app ⟨k, hk⟩ =
-      φ.natTrans.app ⟨k, hk.trans hi⟩ := rfl
-
-end
-
-namespace Hom
-
-variable [PartialOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J]
-  {iter₁ iter₂ : Φ.Iteration ε j}
-
-lemma congr_app (φ φ' : iter₁ ⟶ iter₂) (i : J) (hi : i ≤ j) :
-    φ.natTrans.app ⟨i, hi⟩ = φ'.natTrans.app ⟨i, hi⟩ := by
-  obtain rfl := Subsingleton.elim φ φ'
-  rfl
-
-end Hom
-
 end Iteration
 
-end Functor
-
-open Limits
+end SuccStruct
 
+end SmallObject
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
index 166469022df52..33f037475201a 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
@@ -20,7 +20,7 @@ universe u
 
 namespace CategoryTheory
 
-open Category
+open Category SmallObject
 
 namespace Functor
 
@@ -37,14 +37,22 @@ it sends `Order.succ j` to the given object `X`. -/
 def obj (i : Set.Iic (Order.succ j)) : C :=
   if hij : i.1 ≤ j then F.obj ⟨i.1, hij⟩ else X
 
+lemma obj_eq (i : Set.Iic j) :
+    obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ = F.obj i := dif_pos i.2
+
 /-- The isomorphism `obj F X ⟨i, _⟩ ≅ F.obj i` when `i : Set.Iic j`. -/
 def objIso (i : Set.Iic j) :
-    obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i := eqToIso (dif_pos i.2)
+    obj F X ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i :=
+  eqToIso (obj_eq _ _ _)
+
+include hj in
+lemma obj_succ_eq : obj F X ⟨Order.succ j, by simp⟩ = X :=
+  dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj)
 
 /-- The isomorphism `obj F X ⟨Order.succ j, _⟩ ≅ X`. -/
 def objSuccIso :
     obj F X ⟨Order.succ j, by simp⟩ ≅ X :=
-  eqToIso (dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj))
+  eqToIso (obj_succ_eq hj _ _)
 
 variable {X}
 
@@ -116,11 +124,19 @@ def extendToSucc : Set.Iic (Order.succ j) ⥤ C where
   map_id _ := extendToSucc.map_id _ F τ _ _
   map_comp {i₁ i₂ i₃} f g := extendToSucc.map_comp hj F τ i₁ i₂ i₃ (leOfHom f) (leOfHom g) i₃.2
 
+lemma extendToSucc_obj_eq (i : Set.Iic j) :
+    (extendToSucc hj F τ).obj ⟨i, i.2.trans (Order.le_succ j)⟩ = F.obj i :=
+  extendToSucc.obj_eq F X i
+
 /-- The isomorphism `(extendToSucc hj F τ).obj ⟨i, _⟩ ≅ F.obj i` when `i : Set.Iic j` -/
 def extendToSuccObjIso (i : Set.Iic j) :
     (extendToSucc hj F τ).obj ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i :=
   extendToSucc.objIso F X i
 
+def extendToSucc_obj_succ_eq :
+    (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ = X :=
+  extendToSucc.obj_succ_eq hj F X
+
 /-- The isomorphism `(extendToSucc hj F τ).obj ⟨Order.succ j, _⟩ ≅ X`. -/
 def extendToSuccObjSuccIso :
     (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ ≅ X :=
@@ -138,12 +154,12 @@ lemma extendToSuccObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi
 /-- The isomorphism expressing that `extendToSucc hj F τ` extends `F`. -/
 @[simps!]
 def extendToSuccRestrictionLEIso :
-    Iteration.restrictionLE (extendToSucc hj F τ) (Order.le_succ j) ≅ F :=
+    restrictionLE (extendToSucc hj F τ) (Order.le_succ j) ≅ F :=
   NatIso.ofComponents (extendToSuccObjIso hj F τ) (by
     rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f
     apply extendToSuccObjIso_hom_naturality)
 
-lemma extentToSucc_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
+lemma extendToSucc_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
     (extendToSucc hj F τ).map (homOfLE hi :
       ⟨i₁, hi.trans (hi₂.trans (Order.le_succ j))⟩ ⟶ ⟨i₂, hi₂.trans (Order.le_succ j)⟩) =
       (extendToSuccObjIso hj F τ ⟨i₁, hi.trans hi₂⟩).hom ≫ F.map (homOfLE hi) ≫
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
index 35b3bf90ea04c..3c601d1afeffd 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
@@ -19,7 +19,7 @@ universe u
 
 namespace CategoryTheory
 
-open Category Limits
+open Category Limits SmallObject
 
 namespace Functor
 
@@ -92,11 +92,19 @@ def ofCocone : Set.Iic j ⥤ C where
   map_id i := ofCocone.map_id _ _ i.2
   map_comp {_ _ i₃} _ _ := ofCocone.map_comp _ _ _ _ _ _ i₃.2
 
+lemma ofCocone_obj_eq (i : J) (hi : i < j) :
+    (ofCocone c).obj ⟨i, hi.le⟩ = F.obj ⟨i, hi⟩ :=
+  dif_pos hi
+
 /-- The isomorphism `(ofCocone c).obj ⟨i, _⟩ ≅ F.obj ⟨i, _⟩` when `i < j`. -/
 def ofCoconeObjIso (i : J) (hi : i < j) :
     (ofCocone c).obj ⟨i, hi.le⟩ ≅ F.obj ⟨i, hi⟩ :=
   ofCocone.objIso c _ _
 
+lemma ofCocone_obj_eq_pt :
+    (ofCocone c).obj ⟨j, by simp⟩ = c.pt :=
+  dif_neg (by simp)
+
 /-- The isomorphism `(ofCocone c).obj ⟨j, _⟩ ≅ c.pt`. -/
 def ofCoconeObjIsoPt :
     (ofCocone c).obj ⟨j, by simp⟩ ≅ c.pt :=
@@ -127,14 +135,14 @@ lemma ofCoconeObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂
 when `c : Cocone F`. -/
 @[simps!]
 def restrictionLTOfCoconeIso :
-    Iteration.restrictionLT (ofCocone c) (Preorder.le_refl j) ≅ F :=
+    restrictionLT (ofCocone c) (Preorder.le_refl j) ≅ F :=
   NatIso.ofComponents (fun ⟨i, hi⟩ ↦ ofCoconeObjIso c i hi)
     (by intros; apply ofCoconeObjIso_hom_naturality)
 
 variable {c} in
 /-- If `c` is a colimit cocone, then so is `coconeOfLE (ofCocone c) (Preorder.le_refl j)`. -/
 def isColimitCoconeOfLEOfCocone (hc : IsColimit c) :
-    IsColimit (Iteration.coconeOfLE (ofCocone c) (Preorder.le_refl j)) :=
+    IsColimit (coconeOfLE (ofCocone c) (Preorder.le_refl j)) :=
   (IsColimit.precomposeInvEquiv (restrictionLTOfCoconeIso c) _).1
     (IsColimit.ofIsoColimit hc
       (Cocones.ext (ofCoconeObjIsoPt c).symm (fun ⟨i, hi⟩ ↦ by
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Iteration.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Iteration.lean
new file mode 100644
index 0000000000000..3aa25e1015337
--- /dev/null
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Iteration.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
+
+/-!
+# The transfinite iteration of a successor structure
+
+Given a successor structure `Φ : SuccStruct C` (see the file `SmallObject.Iteration.Basic`)
+and a well-ordered type `J`, we define the iteration `Φ.iteration J : C`. It is
+defined as the colimit of a functor `Φ.iterationFunctor J : J ⥤ C`.
+
+-/
+
+universe w v u
+
+namespace CategoryTheory.SmallObject.SuccStruct
+
+open Limits
+
+variable {C : Type u} [Category.{v} C] (Φ : SuccStruct C)
+  (J : Type u) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J]
+  [HasIterationOfShape C J]
+
+variable {J} in
+/-- Given `Φ : SuccStruct C` and an element `j : J` in a well-ordered type,
+this is the unique element in `Φ.Iteration j`. -/
+noncomputable def iter (j : J) : Φ.Iteration j := Classical.arbitrary _
+
+/-- Given `Φ : SuccStruct C` and a well-ordered type `J`, this
+is the functor `J ⥤ C` which gives the iterations of `Φ` indexed by `J`. -/
+@[simps (config := .lemmasOnly)]
+noncomputable def iterationFunctor : J ⥤ C where
+  obj j := (Φ.iter j).F.obj ⟨j, by simp⟩
+  map f := Iteration.mapObj _ _ (leOfHom f) _ _ (leOfHom f)
+
+/-- Given `Φ : SuccStruct C` and a well-ordered type `J`,
+this is an object of `C` which is the iteration of `Φ` to the power `J`:
+it is defined as the colimit of the functor `Φ.iterationFunctor J`. -/
+noncomputable def iteration : C := colimit (Φ.iterationFunctor J)
+
+/-- The colimit cocone expressing that `Φ.iteration J` is the colimit
+of `Φ.iterationFunctor J`. -/
+noncomputable def iterationCocone : Cocone (Φ.iterationFunctor J) :=
+  colimit.cocone _
+
+@[simp]
+lemma iterationCocone_pt : (Φ.iterationCocone J).pt = Φ.iteration J := rfl
+
+/-- `Φ.iteration J` identifies to the colimit of `Φ.iterationFunctor J`. -/
+noncomputable def isColimitIterationCocone : IsColimit (Φ.iterationCocone J) :=
+  colimit.isColimit _
+
+end CategoryTheory.SmallObject.SuccStruct
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
index 68fb16121f519..416b8382c34e1 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean
@@ -3,21 +3,16 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
-import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
+import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
 import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
-import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 
 /-!
-# Existence of objects in the category of iterations of functors
+# Existence of the iteration of a successor structure
 
-Given a functor `Φ : C ⥤ C` and a natural transformation `ε : 𝟭 C ⟶ Φ`,
-we shall show in this file that for any well ordered set `J`,
-and `j : J`, the category `Functor.Iteration ε j` is nonempty.
-As we already know from the main result in `SmallObject.Iteration.UniqueHom`
-that such objects, if they exist, are unique up to a unique isomorphism,
-we shall show the existence of a term in `Functor.Iteration ε j` by
-transfinite induction.
+Given `Φ : SuccStruct C`, we show by transfinite induction
+that for any element `j` in a well ordered set `J`,
+the type `Φ.Iteration j` is nonempty.
 
 -/
 
@@ -25,205 +20,238 @@ universe u
 
 namespace CategoryTheory
 
-open Category Limits
+namespace SmallObject
+
+namespace SuccStruct
 
-variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ}
-  {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J]
+open Category Limits
 
-namespace Functor
+variable {C : Type*} [Category C] (Φ : SuccStruct C)
+  {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J]
+  [HasIterationOfShape C J]
 
 namespace Iteration
 
-variable (ε J) in
+variable (J) in
 /-- The obvious term in `Iteration ε ⊥`: it is given by the identity functor. -/
-def mkOfBot : Iteration ε (⊥ : J) where
-  F := (Functor.const _).obj (𝟭 C)
-  isoZero := Iso.refl _
-  isoSucc _ h := by simp at h
-  mapSucc'_eq _ h := by simp at h
-  isColimit x hx h := by
-    exfalso
-    refine hx.not_isMin (by simpa using h)
-
-/-- When `j : J` is not maximal, this is the extension as `Iteration ε (Order.succ j)`
-of any `iter : Iteration ε j`. -/
-noncomputable def mkOfSucc {j : J} (hj : ¬IsMax j) (iter : Iteration ε j) :
-    Iteration ε (Order.succ j) where
-  F := extendToSucc hj iter.F (whiskerLeft _ ε)
-  isoZero := (extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨⊥, by simp⟩).trans iter.isoZero
-  isoSucc i hi :=
-    if hij : i < j then
-      extendToSuccObjIso _ _ _ ⟨Order.succ i, Order.succ_le_of_lt hij⟩ ≪≫
-        iter.isoSucc i hij ≪≫ (isoWhiskerRight (extendToSuccObjIso _ _ _ ⟨i, hij.le⟩).symm _)
-    else
-      have hij' : i = j := le_antisymm
-        (by simpa only [Order.lt_succ_iff_of_not_isMax hj] using hi) (by simpa using hij)
-      eqToIso (by subst hij'; rfl) ≪≫ extendToSuccObjSuccIso hj iter.F (whiskerLeft _ ε) ≪≫
-        isoWhiskerRight ((extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨j, by simp⟩).symm.trans
-            (eqToIso (by subst hij'; rfl))) _
-  mapSucc'_eq i hi := by
-    obtain hi' | rfl := ((Order.lt_succ_iff_of_not_isMax hj).mp hi).lt_or_eq
-    · ext X
-      have := iter.mapSucc_eq i hi'
-      dsimp [mapSucc, mapSucc'] at this ⊢
-      rw [extentToSucc_map _ _ _ _ _ _ (Order.succ_le_of_lt hi'), this, dif_pos hi']
-      dsimp
-      rw [assoc, assoc]
-      erw [ε.naturality_assoc]
-    · ext X
-      dsimp [mapSucc']
-      rw [dif_neg (gt_irrefl i), extendToSucc_map_le_succ]
-      dsimp
-      rw [id_comp, comp_id]
-      erw [ε.naturality_assoc]
-  isColimit i hi hij := by
-    have hij' : i ≤ j := by
-      obtain hij | rfl := hij.lt_or_eq
-      · exact (Order.lt_succ_iff_of_not_isMax hj).1 hij
-      · exfalso
-        exact Order.not_isSuccLimit_succ_of_not_isMax hj hi
-    refine (IsColimit.precomposeHomEquiv
-      (isoWhiskerLeft (monotone_inclusion_lt_le_of_le hij').functor
-        (extendToSuccRestrictionLEIso hj iter.F (whiskerLeft _ ε))).symm _).1
-      (IsColimit.ofIsoColimit (iter.isColimit i hi hij')
-      (Iso.symm (Cocones.ext (extendToSuccObjIso hj iter.F (whiskerLeft _ ε) ⟨i, hij'⟩)
-      (fun ⟨k, hk⟩ ↦ ?_))))
-    dsimp
-    rw [assoc, extendToSuccObjIso_hom_naturality hj iter.F (whiskerLeft _ ε)]
-    dsimp
-    rw [Iso.inv_hom_id_assoc]
-
-section
-
-variable [WellFoundedLT J] {j : J} (hj : Order.IsSuccLimit j)
-  (iter : ∀ (i : J) (_ : i < j), Iteration ε i)
+def mkOfBot : Φ.Iteration (⊥ : J) where
+  F := (Functor.const _).obj Φ.X₀
+  obj_bot := rfl
+  obj_succ _ h := by simp at h
+  map_succ  _ h := by simp at h
+  obj_limit x hx h := (hx.not_isMin (by simpa using h)).elim
+  map_eq_ι _ _ h₁ _ h₂ := by
+    obtain rfl := le_bot_iff.1 h₁
+    simp at h₂
 
-namespace mkOfLimit
+variable {Φ}
 
-/-- Auxiliary definition for `mkOfLimit`. -/
-noncomputable def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
-    (iter i₁ (lt_of_le_of_lt hi hi₂)).F.obj ⟨i₁, by simp⟩ ⟶ (iter i₂ hi₂).F.obj ⟨i₂, by simp⟩ :=
-  ((iter i₁ (lt_of_le_of_lt hi hi₂)).iso ((iter i₂ hi₂).trunc hi)).hom.natTrans.app
-    ⟨i₁, by simp⟩ ≫ (iter i₂ hi₂).F.map (homOfLE hi)
+open Functor in
+/-- When `j : J` is not maximal, this is the extension as `Φ.Iteration (Order.succ j)`
+of any `iter : Φ.Iteration j`. -/
+noncomputable def mkOfSucc {j : J} (hj : ¬IsMax j) (iter : Φ.Iteration j) :
+    Φ.Iteration (Order.succ j) where
+  F := extendToSucc hj iter.F (Φ.toSucc _)
+  obj_bot := by rw [extendToSucc_obj_eq _ _ _ ⟨⊥, bot_le⟩, obj_bot]
+  obj_succ i hi₁ := by
+    have hi₂ := (Order.lt_succ_iff_of_not_isMax hj).1 hi₁
+    rw [extendToSucc_obj_eq _ _ _ ⟨i, hi₂⟩]
+    by_cases hi₃ : i < j
+    · rw [extendToSucc_obj_eq _ _ _ ⟨Order.succ i, Order.succ_le_of_lt hi₃⟩, obj_succ _ _ hi₃]
+    · obtain rfl : i = j := le_antisymm hi₂ (by simpa using hi₃)
+      rw [extendToSucc_obj_succ_eq]
+  map_succ i hi₁ := by
+    rw [Order.lt_succ_iff_of_not_isMax hj] at hi₁
+    by_cases hi₂ : i < j
+    · simp [extendToSucc_map _ _ _ _ _ _ (Order.succ_le_of_lt hi₂), map_succ _ _ hi₂,
+        extendToSuccObjIso, extendToSucc.objIso,
+        Φ.congr_toSucc (extendToSucc_obj_eq hj iter.F (Φ.toSucc _) ⟨i, hi₂.le⟩)]
+    · obtain rfl : j = i := le_antisymm (by simpa using hi₂) hi₁
+      simp [extendToSucc_map_le_succ,
+        Φ.congr_toSucc (extendToSucc_obj_eq hj iter.F (Φ.toSucc _) ⟨j, by simp⟩),
+        extendToSuccObjIso, extendToSucc.objIso,
+        extendToSuccObjSuccIso, extendToSucc.objSuccIso]
+  obj_limit i hi hij := by
+    rw [Order.IsSuccLimit.le_succ_iff hi] at hij
+    rw [extendToSucc_obj_eq hj iter.F (Φ.toSucc _) ⟨i, hij⟩, obj_limit _ _ hi]
+    congr 1
+    fapply Functor.ext
+    · rintro ⟨k, hk⟩
+      exact (extendToSucc_obj_eq hj iter.F (Φ.toSucc _) ⟨k, _⟩).symm
+    · rintro ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f
+      simp [extendToSucc_map _ _ _ k₁ k₂ (leOfHom f) (hk₂.le.trans hij),
+        extendToSuccObjIso, extendToSucc.objIso,
+        extendToSuccObjSuccIso, extendToSucc.objSuccIso]
+  map_eq_ι i hi hij k hk := by
+    have hij' := (Order.IsSuccLimit.le_succ_iff hi).1 hij
+    have : restrictionLT iter.F hij' =
+        restrictionLT (extendToSucc hj iter.F (Φ.toSucc _)) hij := by
+      fapply Functor.ext
+      · rintro ⟨l, hl⟩
+        exact (extendToSucc_obj_eq hj iter.F (Φ.toSucc _) ⟨l, _⟩).symm
+      · rintro ⟨l₁, hl₁⟩ ⟨l₂, hl₂⟩ f
+        simp [extendToSucc_map _ _ _ l₁ l₂ (leOfHom f) (hl₂.le.trans hij'),
+          extendToSuccObjIso, extendToSucc.objIso]
+    simp [extendToSucc_map _ _ _ _ _ _ hij', map_eq_ι _ i hi _ _ hk,
+      congr_colimit_ι this hi, extendToSuccObjIso, extendToSucc.objIso]
 
-@[simp]
-lemma map_id (i : J) (hi : i < j) :
-    map iter i i (by rfl) hi = 𝟙 _ := by
-  simp [map]
-
-lemma map_comp (i₁ i₂ i₃ : J) (hi : i₁ ≤ i₂) (hi' : i₂ ≤ i₃) (hi₃ : i₃ < j) :
-    map iter i₁ i₃ (hi.trans hi') hi₃ =
-      map iter i₁ i₂ hi (lt_of_le_of_lt hi' hi₃) ≫
-        map iter i₂ i₃ hi' hi₃ := by
-  dsimp [map]
-  rw [assoc, NatTrans.naturality_assoc]
+lemma congr_obj {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂)
+    (k : J) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) :
+    iter₁.F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩ := by
+  wlog h : j₁ ≤ j₂ generalizing j₁ j₂
+  · exact (this iter₂ iter₁ h₂ h₁ (le_of_lt (by simpa using h))).symm
+  rw [Subsingleton.elim iter₁ (iter₂.trunc h)]
   dsimp
-  rw [← truncFunctor_map_natTrans_app _ hi i₁ (by rfl), truncFunctor_map_iso_hom,
-    ← NatTrans.comp_app_assoc, ← natTrans_comp, ← Functor.map_comp]
-  dsimp only [truncFunctor_obj, trunc_trunc]
-  rw [iso_hom_comp_iso_hom, homOfLE_comp]
 
-/-- Auxiliary definition for `mkOfLimit`. -/
+lemma congr_map {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂)
+    {k₁ k₂ : J} (h : k₁ ≤ k₂) (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) :
+    iter₁.F.map (homOfLE h : ⟨k₁, h.trans h₁⟩ ⟶ ⟨k₂, h₁⟩) =
+      eqToHom (congr_obj iter₁ iter₂ k₁ (h.trans h₁) (h.trans h₂)) ≫
+        iter₂.F.map (homOfLE h) ≫
+        eqToHom (congr_obj iter₁ iter₂ k₂ h₁ h₂).symm := by
+  wlog hj : j₁ ≤ j₂ generalizing j₁ j₂
+  · simp [this iter₂ iter₁ h₂ h₁ ((not_le.1 hj).le)]
+  exact Functor.congr_hom (congr_arg F (Subsingleton.elim iter₁ (iter₂.trunc hj)))
+    (homOfLE h : ⟨k₁, _⟩ ⟶ ⟨k₂, _⟩)
+
+/-- Given `iter₁ : Φ.Iteration j₁` and `iter₂ : Φ.Iteration j₂`, with `j₁ ≤ j₂`,
+if `k₁ ≤ k₂` are elements such that `k₁ ≤ j₁` and `k₂ ≤ k₂`, then this
+is the canonical map `iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩`. -/
+def mapObj {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂)
+    {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂) :
+    iter₁.F.obj ⟨k₁, h₁⟩ ⟶ iter₂.F.obj ⟨k₂, h₂⟩ :=
+  eqToHom (congr_obj iter₁ iter₂ k₁ h₁ (h₁.trans hj)) ≫
+    iter₂.F.map (homOfLE h₁₂)
+
+@[simp]
+lemma mapObj_refl {j : J} (iter : Φ.Iteration j)
+    {k l : J} (h : k ≤ l) (h' : l ≤ j) :
+    mapObj iter iter h (h.trans h') h' (by rfl) = iter.F.map (homOfLE h) := by
+  simp [mapObj]
+
+@[reassoc (attr := simp)]
+lemma mapObj_trans {j₁ j₂ j₃ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂)
+    (iter₃ : Φ.Iteration j₃) {k₁ k₂ k₃ : J} (h₁₂ : k₁ ≤ k₂) (h₂₃ : k₂ ≤ k₃)
+    (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (h₃ : k₃ ≤ j₃) (h₁₂' : j₁ ≤ j₂) (h₂₃' : j₂ ≤ j₃) :
+    mapObj iter₁ iter₂ h₁₂ h₁ h₂ h₁₂' ≫ mapObj iter₂ iter₃ h₂₃ h₂ h₃ h₂₃' =
+      mapObj iter₁ iter₃ (h₁₂.trans h₂₃) h₁ h₃ (h₁₂'.trans h₂₃') := by
+  simp [mapObj, congr_map iter₂ iter₃ h₁₂ h₂ (h₂.trans h₂₃'), ← Functor.map_comp]
+
+namespace mkOfLimit
+
+open Functor
+
+variable {j : J} (hj : Order.IsSuccLimit j) (iter : ∀ (i : J), i < j → Φ.Iteration i)
+
+/-- Assuming `j : J` is a limit element and that we have `∀ (i : J), i < j → Φ.Iteration i`,
+this is the inductive system `Set.Iio j ⥤ C` which sends `⟨i, _⟩` to
+`(iter i _).F.obj ⟨i, _⟩`. -/
 @[simps]
-noncomputable def functor : Set.Iio j ⥤ C ⥤ C where
+noncomputable def inductiveSystem : Set.Iio j ⥤ C where
   obj i := (iter i.1 i.2).F.obj ⟨i.1, by simp⟩
-  map f := map iter _ _ (leOfHom f) _
-  map_id _ := map_id iter _ _
-  map_comp _ _ := map_comp iter _ _ _ _ _ _
-
-/-- Auxiliary definition for `mkOfLimit`. -/
-noncomputable def restrictionLTFunctorIso (i : J) (hi : i < j) :
-    (monotone_inclusion_lt_lt_of_le hi.le).functor ⋙ functor iter ≅
-      restrictionLT (iter i hi).F (by rfl) :=
-  NatIso.ofComponents (fun ⟨k, hk⟩ ↦ (eval ε (Preorder.le_refl k)).mapIso
-    ((iter k (hk.trans hi)).iso ((iter i hi).trunc hk.le))) (by
-      rintro ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f
-      dsimp [map]
-      rw [assoc, NatTrans.naturality]
-      dsimp
-      simp only [← assoc]; congr 1
-      dsimp
-      rw [← truncFunctor_map_natTrans_app _ (i := k₁) (j := k₂) (leOfHom f) _ (by rfl),
-        truncFunctor_map_iso_hom, ← NatTrans.comp_app, ← natTrans_comp]
-      erw [iso_hom_comp_iso_hom]
-      rfl)
-
-@[reassoc]
-lemma restrictionLTFunctorIso_inv_app_map (k i : J) (hik : k < i) (hij : i < j) :
-    (restrictionLTFunctorIso iter i hij).inv.app ⟨k, hik⟩ ≫ map iter k i hik.le hij =
-      (iter i hij).F.map (homOfLE hik.le) := by
-  dsimp [restrictionLTFunctorIso, map]
-  rw [← NatTrans.comp_app_assoc, ← natTrans_comp, Iso.inv_hom_id, natTrans_id,
-    NatTrans.id_app]
-  dsimp
-  rw [id_comp]
+  map {i₁ i₂} f := mapObj (iter i₁.1 i₁.2) (iter i₂.1 i₂.2) (leOfHom f)
+    (by simp) (by simp) (leOfHom f)
+
+/-- The extension of `inductiveSystem iter` to a functor `Set.Iic j ⥤ C` which
+sends the top element to the colimit of `inductiveSystem iter`. -/
+noncomputable def functor : Set.Iic j ⥤ C :=
+  letI := hasColimitOfShape_of_isSuccLimit C j hj
+  ofCocone (colimit.cocone (inductiveSystem iter))
+
+lemma functor_obj (i : J) (hi : i < j) {k : J} (iter' : Φ.Iteration k) (hk : i ≤ k) :
+    (functor hj iter).obj ⟨i, hi.le⟩ = iter'.F.obj ⟨i, hk⟩ := by
+  dsimp only [functor]
+  rw [ofCocone_obj_eq _ _ hi]
+  apply congr_obj
+
+lemma functor_obj_eq_colimit :
+    letI := hasColimitOfShape_of_isSuccLimit C j hj
+    (functor hj iter).obj ⟨j, by simp⟩ = colimit (inductiveSystem iter) := by
+  apply ofCocone_obj_eq_pt
+
+lemma functor_map {i₁ i₂ : J} (h₁₂ : i₁ ≤ i₂) (hi₂ : i₂ < j)
+    {k : J} (iter' : Φ.Iteration k) (hk : i₂ ≤ k) :
+    (functor hj iter).map (homOfLE h₁₂ : ⟨i₁, h₁₂.trans hi₂.le⟩ ⟶ ⟨i₂, hi₂.le⟩) =
+      eqToHom (functor_obj hj iter i₁ (lt_of_le_of_lt h₁₂ hi₂) iter' (h₁₂.trans hk)) ≫
+        iter'.F.map (homOfLE h₁₂) ≫
+        eqToHom (functor_obj hj iter i₂ hi₂ iter' hk).symm := by
+  simp [functor, ofCocone_map _ _ _ _ hi₂, congr_map (iter i₂ hi₂) iter' _ _ hk,
+    ofCoconeObjIso, ofCocone.objIso, mapObj]
+
+lemma restrictionLT_functor_of_lt {i : J} (hij : i < j) {k : J} (iter' : Φ.Iteration k)
+    (hk : i ≤ k) :
+    restrictionLT (functor hj iter) hij.le = restrictionLT iter'.F hk := by
+  fapply Functor.ext
+  · rintro ⟨l, hl⟩
+    exact functor_obj hj _ _ (hl.trans hij) iter' _
+  · rintro ⟨l₁, h₁⟩ ⟨l₂, h₂⟩ f
+    exact functor_map hj _ _ (h₂.trans hij) _ _
+
+lemma restrictionLT_functor :
+    restrictionLT (functor hj iter) (le_refl j) = inductiveSystem iter := by
+  fapply Functor.ext
+  · rintro ⟨l, hl⟩
+    exact functor_obj hj _ _ hl _ _
+  · rintro ⟨l₁, h₁⟩ ⟨l₂, h₂⟩ f
+    simp [functor_map _ _ _ h₂ (iter l₂ h₂) (by rfl), mapObj]
+
+lemma functor_map_to_top (i : J) (hij : i < j) :
+    letI := hasColimitOfShape_of_isSuccLimit C j hj
+    (functor hj iter).map (homOfLE hij.le : ⟨i, hij.le⟩ ⟶ ⟨j, by simp⟩) =
+      eqToHom (functor_obj _ _ _ hij _ _) ≫ colimit.ι (inductiveSystem iter) ⟨i, hij⟩ ≫
+          eqToHom (functor_obj_eq_colimit hj iter).symm := by
+  simp [functor, ofCocone_map_to_top _ _ hij, ofCoconeObjIso, ofCocone.objIso,
+    ofCoconeObjIsoPt, ofCocone.objIsoPt]
 
 end mkOfLimit
 
-open mkOfLimit
-
-variable [HasColimit (functor iter)]
-
-include hj iter in
-/-- When `j : J` satisfies `Order.IsSuccLimit j` and we have `iter i hij : Iteration ε i`
-for any `i : J` such that `hij : i < j`, then this is a term in `Iteration ε j`,
-provided a suitable colimit indexed by `Set.Iio j` exists. -/
-noncomputable def mkOfLimit :
-    Iteration ε j where
-  F := Functor.ofCocone (colimit.cocone (functor iter))
-  isoZero := (Functor.ofCoconeObjIso _ ⊥ (Ne.bot_lt (by simpa using hj.1))).trans
-    ((iter ⊥ _).isoZero)
-  isoSucc i hi :=
-    Functor.ofCoconeObjIso _ (Order.succ i) ((Order.IsSuccLimit.succ_lt_iff hj).2 hi) ≪≫
-      (iter (Order.succ i) ((Order.IsSuccLimit.succ_lt_iff hj).2 hi)).isoSucc i (by
-        rw [Order.lt_succ_iff_not_isMax, not_isMax_iff]
-        exact ⟨_, hi⟩) ≪≫
-        isoWhiskerRight ((Iteration.eval ε (Preorder.le_refl i)).mapIso
-            (((iter (Order.succ i) _).trunc (Order.le_succ i)).iso (iter i hi)) ≪≫
-            (Functor.ofCoconeObjIso (colimit.cocone (functor iter)) i hi).symm) Φ
-  mapSucc'_eq i hi := by
-    have hi' : Order.succ i < j := (Order.IsSuccLimit.succ_lt_iff hj).mpr hi
-    have hi'' : i < Order.succ i := by
-      simp only [Order.lt_succ_iff_not_isMax, not_isMax_iff]
-      exact ⟨_, hi⟩
-    have := (iter _ hi').mapSucc_eq i hi''
-    dsimp [mapSucc', mapSucc] at this ⊢
-    rw [ofCocone_map _ _ _ _ hi', functor_map, map, this]
-    ext X
-    dsimp
-    rw [assoc, assoc, assoc, map_comp_assoc]
-    erw [← ε.naturality_assoc, ← ε.naturality_assoc]
-    rfl
-  isColimit i hi hij := by
-    apply Nonempty.some
-    obtain hij' | rfl := hij.lt_or_eq
-    · refine ⟨(IsColimit.precomposeInvEquiv
-        (isoWhiskerLeft (monotone_inclusion_lt_lt_of_le hij).functor
-          (restrictionLTOfCoconeIso (colimit.cocone (functor iter))) ≪≫
-          restrictionLTFunctorIso iter i hij') _).1
-        (IsColimit.ofIsoColimit ((iter i hij').isColimit i hi (by rfl))
-        (Cocones.ext
-          (ofCoconeObjIso (colimit.cocone (functor iter)) i hij').symm (fun ⟨k, hk⟩ ↦ ?_)))⟩
-      dsimp
-      rw [ofCocone_map _ _ _ _ hij', assoc]
-      dsimp
-      rw [Iso.inv_hom_id_assoc, restrictionLTFunctorIso_inv_app_map_assoc]
-    · exact ⟨Functor.isColimitCoconeOfLEOfCocone (colimit.isColimit _)⟩
-
-end
-
-instance [WellFoundedLT J] [HasIterationOfShape C J] (j : J) : Nonempty (Iteration ε j) := by
+open mkOfLimit in
+/-- When `j` is a limit element, this is the element in `Φ.Iteration j`
+that is constructed from elements in `Φ.Iteration i` for all `i < j`. -/
+noncomputable def mkOfLimit {j : J} (hj : Order.IsSuccLimit j)
+    (iter : ∀ (i : J), i < j → Φ.Iteration i) :
+    Φ.Iteration j where
+  F := functor hj iter
+  obj_bot := functor_obj hj iter ⊥ (Order.IsSuccLimit.bot_lt hj) (mkOfBot Φ J) (by rfl)
+  obj_succ i hi₁ := by
+    have hi₂ := (Order.IsSuccLimit.succ_lt_iff hj).2 hi₁
+    rw [functor_obj hj iter (Order.succ i) hi₂ (iter (Order.succ i) hi₂) (by rfl),
+      functor_obj hj iter i hi₁ (iter (Order.succ i) hi₂) (Order.le_succ i),
+      obj_succ _ _ (Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi₁))]
+  map_succ i hi₁ := by
+    have hi₂ := (Order.IsSuccLimit.succ_lt_iff hj).2 hi₁
+    simp [functor_map hj iter (Order.le_succ i) hi₂ (iter _ hi₂) (by rfl),
+      map_succ _ _ (Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi₁)),
+      Φ.congr_toSucc (functor_obj hj iter i hi₁ (iter _ hi₂) (Order.le_succ i))]
+  obj_limit i hi hij := by
+    obtain hij | rfl := hij.lt_or_eq
+    · rw [functor_obj hj iter i hij (iter _ hij) (by rfl), obj_limit _ i hi,
+        restrictionLT_functor_of_lt hj iter hij (iter i hij) (by rfl)]
+    · rw [functor_obj_eq_colimit, restrictionLT_functor]
+  map_eq_ι i hi hij := by
+    obtain hij | rfl := hij.lt_or_eq
+    · intro k hk
+      simp [functor_map hj iter _ hij (iter i hij) (by rfl),
+        map_eq_ι _ _ hi _ _ hk,
+        congr_colimit_ι (restrictionLT_functor_of_lt hj iter hij (iter i hij) (by rfl)) hi]
+    · intro k hk
+      simp [functor_map_to_top _ _ _ hk,
+        congr_colimit_ι (restrictionLT_functor hj iter) hi ⟨k, hk⟩]
+
+variable (Φ)
+
+instance nonempty (j : J) : Nonempty (Φ.Iteration j) := by
   induction j using SuccOrder.limitRecOn with
   | hm i hi =>
       obtain rfl : i = ⊥ := by simpa using hi
-      exact ⟨mkOfBot ε J⟩
+      exact ⟨mkOfBot Φ J⟩
   | hs i hi hi' => exact ⟨mkOfSucc hi hi'.some⟩
-  | hl i hi hi' =>
-      have := hasColimitOfShape_of_isSuccLimit C i hi
-      exact ⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩
+  | hl i hi hi' => exact ⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩
 
 end Iteration
 
-end Functor
+end SuccStruct
+
+end SmallObject
 
 end CategoryTheory

From 6a3aed8e8efae88b1806b6c9cdf7ec15c9555aa2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 26 Dec 2024 14:50:46 +0100
Subject: [PATCH 25/28] removed unused file

---
 Mathlib.lean                                  |   2 +-
 .../SmallObject/Iteration/UniqueHom.lean      | 256 ------------------
 2 files changed, 1 insertion(+), 257 deletions(-)
 delete mode 100644 Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 25b6753d6ca64..6eb498aa7d06b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2178,8 +2178,8 @@ import Mathlib.CategoryTheory.SmallObject.Construction
 import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
 import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
 import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
+import Mathlib.CategoryTheory.SmallObject.Iteration.Iteration
 import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
-import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
 import Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
 import Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
 import Mathlib.CategoryTheory.Square
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
deleted file mode 100644
index bb40843af6cc7..0000000000000
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
+++ /dev/null
@@ -1,256 +0,0 @@
-/-
-Copyright (c) 2024 Joël Riou. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joël Riou
--/
-import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
-
-/-!
-# Uniqueness of morphisms in the category of iterations of functors
-
-Given a functor `Φ : C ⥤ C` and a natural transformation `ε : 𝟭 C ⟶ Φ`,
-we show in this file that there exists a unique morphism
-between two arbitrary objects in the category `Functor.Iteration ε j`
-when `j : J` and `J` is a well orderered set.
-
--/
-
-universe u
-
-namespace CategoryTheory
-
-open Category Limits
-
-variable {C : Type*} [Category C] {Φ : C ⥤ C} {ε : 𝟭 C ⟶ Φ}
-  {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J]
-
-namespace Functor
-
-namespace Iteration
-
-namespace Hom
-
-/-- The (unique) morphism between two objects in `Iteration ε ⊥` -/
-def mkOfBot (iter₁ iter₂ : Iteration ε (⊥ : J)) : iter₁ ⟶ iter₂ where
-  natTrans :=
-    { app := fun ⟨i, hi⟩ => eqToHom (by congr; simpa using hi) ≫ iter₁.isoZero.hom ≫
-        iter₂.isoZero.inv ≫ eqToHom (by congr; symm; simpa using hi)
-      naturality := fun ⟨i, hi⟩ ⟨k, hk⟩ φ => by
-        obtain rfl : i = ⊥ := by simpa using hi
-        obtain rfl : k = ⊥ := by simpa using hk
-        obtain rfl : φ = 𝟙 _ := rfl
-        simp }
-  natTrans_app_succ i hi := by simp at hi
-
-section
-
-variable {i : J} {iter₁ iter₂ : Iteration ε (Order.succ i)}
-  (hi : ¬IsMax i) (φ : iter₁.trunc (SuccOrder.le_succ i) ⟶ iter₂.trunc (SuccOrder.le_succ i))
-
-/-- Auxiliary definition for `mkOfSucc`. -/
-noncomputable def mkOfSuccNatTransApp (k : J) (hk : k ≤ Order.succ i) :
-    iter₁.F.obj ⟨k, hk⟩ ⟶ iter₂.F.obj ⟨k, hk⟩ :=
-  if hk' : k = Order.succ i then
-    eqToHom (by subst hk'; rfl) ≫ (iter₁.isoSucc i (Order.lt_succ_of_not_isMax hi)).hom ≫
-      whiskerRight (φ.natTrans.app ⟨i, by simp⟩) _ ≫
-      (iter₂.isoSucc i (Order.lt_succ_of_not_isMax hi)).inv ≫
-      eqToHom (by subst hk'; rfl)
-  else
-    φ.natTrans.app ⟨k, Order.le_of_lt_succ (by
-      obtain hk | rfl := hk.lt_or_eq
-      · exact hk
-      · tauto)⟩
-
-lemma mkOfSuccNatTransApp_eq_of_le (k : J) (hk : k ≤ i) :
-    mkOfSuccNatTransApp hi φ k (hk.trans (Order.le_succ i)) =
-      φ.natTrans.app ⟨k, hk⟩ :=
-  dif_neg (by rintro rfl; simpa using lt_of_le_of_lt hk (Order.lt_succ_of_not_isMax hi))
-
-@[simp]
-lemma mkOfSuccNatTransApp_succ_eq :
-    mkOfSuccNatTransApp hi φ (Order.succ i) (by rfl) =
-      (iter₁.isoSucc i (Order.lt_succ_of_not_isMax hi)).hom ≫
-        whiskerRight (φ.natTrans.app ⟨i, by simp⟩) _ ≫
-        (iter₂.isoSucc i (Order.lt_succ_of_not_isMax hi)).inv := by
-  dsimp [mkOfSuccNatTransApp]
-  rw [dif_pos rfl, comp_id, id_comp]
-
-/-- Auxiliary definition for `mkOfSucc`. -/
-@[simps]
-noncomputable def mkOfSuccNatTrans :
-    iter₁.F ⟶ iter₂.F where
-  app := fun ⟨k, hk⟩ => mkOfSuccNatTransApp hi φ k hk
-  naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by
-    dsimp
-    have hk : k₁ ≤ k₂ := leOfHom f
-    obtain h₂ | rfl := hk₂.lt_or_eq
-    · replace h₂ : k₂ ≤ i := Order.le_of_lt_succ h₂
-      rw [mkOfSuccNatTransApp_eq_of_le hi φ k₂ h₂,
-        mkOfSuccNatTransApp_eq_of_le hi φ k₁ (hk.trans h₂)]
-      exact natTrans_naturality φ k₁ k₂ hk h₂
-    · obtain h₁ | rfl := hk.lt_or_eq
-      · have h₂ : k₁ ≤ i := Order.le_of_lt_succ h₁
-        let f₁ : (⟨k₁, hk⟩ : { l | l ≤ Order.succ i}) ⟶
-          ⟨i, Order.le_succ i⟩ := homOfLE h₂
-        let f₂ : (⟨i, Order.le_succ i⟩ : Set.Iic (Order.succ i)) ⟶
-          ⟨Order.succ i, by simp⟩ := homOfLE (Order.le_succ i)
-        obtain rfl : f = f₁ ≫ f₂ := rfl
-        rw [Functor.map_comp, Functor.map_comp, assoc,
-          mkOfSuccNatTransApp_eq_of_le hi φ k₁ h₂]
-        erw [← natTrans_naturality_assoc φ k₁ i h₂ (by rfl)]
-        rw [mkOfSuccNatTransApp_succ_eq]
-        dsimp
-        have ha : iter₁.F.map f₂ = iter₁.mapSucc i (Order.lt_succ_of_not_isMax hi) := rfl
-        have hb : iter₂.F.map f₂ = iter₂.mapSucc i (Order.lt_succ_of_not_isMax hi) := rfl
-        rw [ha, hb]
-        rw [iter₁.mapSucc_eq i, iter₂.mapSucc_eq i, assoc,
-          Iso.inv_hom_id_assoc]
-        ext X
-        dsimp
-        rw [← ε.naturality_assoc]
-        rfl
-      · obtain rfl : f = 𝟙 _ := rfl
-        rw [Functor.map_id, Functor.map_id, id_comp, comp_id]
-
-end
-
-/-- The (unique) morphism between two objects in `Iteration ε (Order.succ i)`,
-assuming we have a morphism between the truncations to `Iteration ε i`. -/
-noncomputable def mkOfSucc
-    {i : J} (iter₁ iter₂ : Iteration ε (Order.succ i)) (hi : ¬IsMax i)
-    (φ : iter₁.trunc (SuccOrder.le_succ i) ⟶ iter₂.trunc (SuccOrder.le_succ i)) :
-    iter₁ ⟶ iter₂ where
-  natTrans := mkOfSuccNatTrans hi φ
-  natTrans_app_zero := by
-    dsimp
-    rw [mkOfSuccNatTransApp_eq_of_le _ _ _ bot_le, φ.natTrans_app_zero]
-    rfl
-  natTrans_app_succ k hk := by
-    obtain hk' | rfl := (Order.le_of_lt_succ hk).lt_or_eq
-    · dsimp
-      rw [mkOfSuccNatTransApp_eq_of_le hi φ k hk'.le,
-        mkOfSuccNatTransApp_eq_of_le hi φ (Order.succ k) (Order.succ_le_of_lt hk'),
-        φ.natTrans_app_succ _ hk']
-      rfl
-    · simp [mkOfSuccNatTransApp_eq_of_le hi φ k (by rfl)]
-
-variable {j : J} {iter₁ iter₂ : Iteration ε j}
-
-section
-
-variable (φ : ∀ (i : J) (hi : i < j), iter₁.trunc hi.le ⟶ iter₂.trunc hi.le)
-  [WellFoundedLT J] (hj : Order.IsSuccLimit j)
-
-/-- Auxiliary definition for `mkOfLimit`. -/
-def mkOfLimitNatTransApp (i : J) (hi : i ≤ j) :
-    iter₁.F.obj ⟨i, hi⟩ ⟶ iter₂.F.obj ⟨i, hi⟩ :=
-  if h : i < j
-    then
-      (φ i h).natTrans.app ⟨i, by simp⟩
-    else by
-      obtain rfl : i = j := by
-        obtain h' | rfl := hi.lt_or_eq
-        · exfalso
-          exact h h'
-        · rfl
-      exact (iter₁.isColimit i hj (by simp)).desc (Cocone.mk _
-        { app := fun ⟨k, hk⟩ => (φ k hk).natTrans.app ⟨k, by simp⟩ ≫
-            iter₂.F.map (homOfLE (by exact hk.le))
-          naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by
-            have hf : k₁ ≤ k₂ := by simpa using leOfHom f
-            dsimp
-            rw [comp_id, congr_app (φ k₁ hk₁) ((truncFunctor ε hf).map (φ k₂ hk₂))]
-            erw [natTrans_naturality_assoc (φ k₂ hk₂) k₁ k₂ hf (by rfl)]
-            dsimp
-            rw [← Functor.map_comp, homOfLE_comp] })
-
-lemma mkOfLimitNatTransApp_eq_of_lt (i : J) (hi : i < j) :
-    mkOfLimitNatTransApp φ hj i hi.le = (φ i hi).natTrans.app ⟨i, by simp⟩ :=
-  dif_pos hi
-
-lemma mkOfLimitNatTransApp_naturality_top (i : J) (hi : i < j) :
-    iter₁.F.map (homOfLE (by simpa using hi.le) : ⟨i, hi.le⟩ ⟶ ⟨j, by simp⟩) ≫
-      mkOfLimitNatTransApp φ hj j (by rfl) =
-      mkOfLimitNatTransApp φ hj i hi.le ≫ iter₂.F.map (homOfLE (by simpa using hi.le)) := by
-  rw [mkOfLimitNatTransApp_eq_of_lt φ hj i hi, mkOfLimitNatTransApp, dif_neg (by simp)]
-  exact (iter₁.isColimit j hj (by rfl)).fac _ ⟨i, hi⟩
-
-/-- Auxiliary definition for `mkOfLimit`. -/
-@[simps]
-def mkOfLimitNatTrans : iter₁.F ⟶ iter₂.F where
-  app := fun ⟨k, hk⟩ => mkOfLimitNatTransApp φ hj k hk
-  naturality := fun ⟨k₁, hk₁⟩ ⟨k₂, hk₂⟩ f => by
-    have hk : k₁ ≤ k₂ := leOfHom f
-    obtain h₂ | rfl := hk₂.lt_or_eq
-    · dsimp
-      rw [mkOfLimitNatTransApp_eq_of_lt _ hj k₂ h₂,
-        mkOfLimitNatTransApp_eq_of_lt _ hj k₁ (lt_of_le_of_lt hk h₂),
-        congr_app (φ k₁ (lt_of_le_of_lt hk h₂)) ((truncFunctor ε hk).map (φ k₂ h₂))]
-      exact natTrans_naturality (φ k₂ h₂) k₁ k₂ hk (by rfl)
-    · obtain h₁ | rfl := hk₁.lt_or_eq
-      · exact mkOfLimitNatTransApp_naturality_top _ hj _ h₁
-      · obtain rfl : f = 𝟙 _ := rfl
-        simp only [map_id, id_comp, comp_id]
-
-/-- The (unique) morphism between two objects in `Iteration ε j` when `j` is a limit element,
-assuming we have a morphism between the truncations to `Iteration ε i` for all `i < j`. -/
-def mkOfLimit : iter₁ ⟶ iter₂ where
-  natTrans := mkOfLimitNatTrans φ hj
-  natTrans_app_zero := by
-    simp [mkOfLimitNatTransApp_eq_of_lt φ _ ⊥ (by simpa only [bot_lt_iff_ne_bot] using hj.ne_bot)]
-  natTrans_app_succ i h := by
-    dsimp
-    have h' := hj.succ_lt h
-    rw [mkOfLimitNatTransApp_eq_of_lt φ hj _ h',
-      (φ _ h').natTrans_app_succ i (Order.lt_succ_of_not_isMax (not_isMax_of_lt h)),
-      mkOfLimitNatTransApp_eq_of_lt φ _ _ h,
-      congr_app (φ i h) ((truncFunctor ε (Order.le_succ i)).map (φ (Order.succ i) h'))]
-    dsimp
-
-end
-
-variable [WellFoundedLT J]
-
-instance : Nonempty (iter₁ ⟶ iter₂) := by
-  let P := fun (i : J) => ∀ (hi : i ≤ j),
-    Nonempty ((truncFunctor ε hi).obj iter₁ ⟶ (truncFunctor ε hi).obj iter₂)
-  suffices ∀ i, P i from this j (by rfl)
-  intro i
-  induction i using SuccOrder.limitRecOn with
-  | hm i hi =>
-    obtain rfl : i = ⊥ := by simpa using hi
-    exact fun hi' ↦ ⟨Hom.mkOfBot _ _⟩
-  | hs i hi hi' =>
-    exact fun hi'' ↦ ⟨Hom.mkOfSucc _ _ hi (hi' ((Order.le_succ i).trans hi'')).some⟩
-  | hl i hi hi' =>
-    exact fun hi'' ↦ ⟨Hom.mkOfLimit (fun k hk ↦ (hi' k hk (hk.le.trans hi'')).some) hi⟩
-
-noncomputable instance : Unique (iter₁ ⟶ iter₂) :=
-  uniqueOfSubsingleton (Nonempty.some inferInstance)
-
-end Hom
-
-variable [WellFoundedLT J] {j : J} (iter₁ iter₂ iter₃ : Iteration ε j)
-
-/-- The canonical isomorphism between two objects in the category `Iteration ε j`. -/
-noncomputable def iso : iter₁ ≅ iter₂ where
-  hom := default
-  inv := default
-
-@[simp]
-lemma iso_refl : iso iter₁ iter₁ = Iso.refl _ := by aesop_cat
-
-lemma iso_hom_comp_iso_hom :
-    (iso iter₁ iter₂).hom ≫ (iso iter₂ iter₃).hom = (iso iter₁ iter₃).hom :=
-  Subsingleton.elim _ _
-
-lemma truncFunctor_map_iso_hom {i : J} (hi : i ≤ j) :
-    (truncFunctor ε hi).map (iso iter₁ iter₂).hom =
-      (iso (iter₁.trunc hi) (iter₂.trunc hi)).hom :=
-  Subsingleton.elim _ _
-
-end Iteration
-
-end Functor
-
-end CategoryTheory

From 64dcaa1799d4a8af7370d9620ba0f03fc8ecf6ac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 26 Dec 2024 15:30:24 +0100
Subject: [PATCH 26/28] fix

---
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean        | 2 ++
 Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index cfffa3581fcb1..6fd7e0b7b12dd 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -226,6 +226,8 @@ noncomputable def isColimit (i : J)
     (Cocones.ext (eqToIso (iter.obj_limit i hi hij).symm)
     (fun ⟨k, hk⟩ ↦ (iter.map_eq_ι i hi hij k hk).symm))
 
+/-- The element in `Φ.Iteration i` that is deduced from an element
+in `Φ.Iteration j` when `i ≤ j`. -/
 @[simps F]
 def trunc (iter : Φ.Iteration j) {i : J} (hi : i ≤ j) : Φ.Iteration i where
   F := restrictionLE iter.F hi
diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
index 33f037475201a..634e98a242ca7 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
@@ -133,7 +133,7 @@ def extendToSuccObjIso (i : Set.Iic j) :
     (extendToSucc hj F τ).obj ⟨i, i.2.trans (Order.le_succ j)⟩ ≅ F.obj i :=
   extendToSucc.objIso F X i
 
-def extendToSucc_obj_succ_eq :
+lemma extendToSucc_obj_succ_eq :
     (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ = X :=
   extendToSucc.obj_succ_eq hj F X
 

From b429049f115d1e0d2efba1cf7d9b3da299b7d91f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Thu, 26 Dec 2024 15:38:14 +0100
Subject: [PATCH 27/28] better docstring

---
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index 6fd7e0b7b12dd..1433ae256d2b4 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -27,9 +27,9 @@ this will correspond to the case of
 `succ G := G ⋙ F` and `toSucc G : G ⟶ G ⋙ F` is given by `whiskerLeft G ε`.
 
 The construction of the iteration of `Φ : SuccStruct C` is done
-by transfinite induction. However, for a limit element `j : J`,
-the definition of `F.obj j` does not involve only
-the objects `F.obj i` for `i < j`, but it also
+by transfinite induction, under an assumption `HasIterationOfShape C J`.
+However, for a limit element `j : J`, the definition of `F.obj j`
+does not involve only the objects `F.obj i` for `i < j`, but it also
 involves the maps `F.obj i₁ ⟶ F.obj i₂` for `i₁ ≤ i₂ < j`.
 Then, this is a straightforward application of definitions by
 transfinite induction. In order to solve this technical difficulty,

From 6e7169323234a07f9186ab3ebfc4707e41979580 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Thu, 26 Dec 2024 16:25:28 +0100
Subject: [PATCH 28/28] Update
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean

---
 Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
index 1433ae256d2b4..2c101474727ed 100644
--- a/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
+++ b/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@@ -256,6 +256,8 @@ variable {F G : Set.Iic j ⥤ C} (hobj : F.obj = G.obj)
 
 omit [OrderBot J] [SuccOrder J] [WellFoundedLT J]
 
+/-- Given two functors `Set.Iic j ⥤ C` that are equal on objects,
+this is the condition that they coincide on a given map. -/
 def MapEq (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ ≤ j) : Prop :=
   F.map (homOfLE h₁₂ : ⟨i₁, h₁₂.trans h₂⟩ ⟶ ⟨i₂, h₂⟩) =
     eqToHom (by rw [hobj]) ≫