awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : W.llp.TransfiniteCompositionOfShape J f
this :
  W.llp (X := h.toTransfiniteCompositionOfShape (W := W.llp).F.obj ⊥)
    (h.toTransfiniteCompositionOfShape (W := W.llp).incl.app ⊥)
⊢ W.llp f

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff _
    (Arrow.isoMk h.isoBot.symm (Iso.refl _))).2 this

Premises used: Iff.mpr, CategoryTheory.Iso.refl, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.Iso.symm, CategoryTheory.TransfiniteCompositionOfShape.isoBot, CategoryTheory.Arrow.isoMk
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
⊢ W.rlp.llp.IsStableUnderTransfiniteCompositionOfShape J

Tactic:
have := W.rlp.isStableUnderTransfiniteCompositionOfShape_llp J
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
this : W.rlp.llp.IsStableUnderTransfiniteCompositionOfShape J
⊢ W.rlp.llp.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
rw [isStableUnderTransfiniteCompositionOfShape_iff] at this

Premises used: CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
this : W.rlp.llp.transfiniteCompositionsOfShape J ≤ W.rlp.llp
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
le_trans (transfiniteCompositionsOfShape_monotone J W.le_llp_rlp) this

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_monotone, CategoryTheory.MorphismProperty.le_llp_rlp, le_trans
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
this : W.rlp.llp.transfiniteCompositionsOfShape J ≤ W.rlp.llp
⊢ W.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
exact le_trans (transfiniteCompositionsOfShape_monotone J W.le_llp_rlp) this

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_monotone, CategoryTheory.MorphismProperty.le_llp_rlp, le_trans
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
⊢ (coproducts.{w, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
simpa using transfiniteCompositionsOfShape_le_llp_rlp (coproducts.{w} W).pushouts J
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
rw : (coproducts.{w, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp
⊢ ((coproducts.{w, v, u} W).pushouts.transfiniteCompositionsOfShape J).retracts ≤ W.rlp.llp

Tactic:
rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp]

Premises used: CategoryTheory.MorphismProperty.rlp_retracts, CategoryTheory.MorphismProperty.le_llp_iff_le_rlp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
⊢ (coproducts.{w, v, u} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp

Tactic:
apply transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X : C
_ : ∀ ⦃Y : C⦄ (f : X ⟶ Y), transfiniteCompositions.{w, v, u} W f → W.rlp.llp f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), transfiniteCompositions.{w, v, u} W f → W.rlp.llp f

Tactic:
_
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf : transfiniteCompositions.{w, v, u} W f
⊢ ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W.transfiniteCompositionsOfShape J f

Tactic:
rw [transfiniteCompositions_iff] at hf

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositions_iff
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
hf :
  ∃ (J : Type w) (x : LinearOrder J) (x_1 : SuccOrder J) (x_2 : OrderBot J) (x_3 : WellFoundedLT J),
    W.transfiniteCompositionsOfShape J f
obtain :
  ∀ (w : Type w) (w_1 : LinearOrder w) (w_2 : SuccOrder w) (w_3 : OrderBot w) (w_4 : WellFoundedLT w)
    (hf : W.transfiniteCompositionsOfShape w f), W.rlp.llp f
⊢ W.rlp.llp f

Tactic:
obtain ⟨_, _, _, _, _, hf⟩ := hf
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
w : Type w
w_1 : LinearOrder w
w_2 : SuccOrder w
w_3 : OrderBot w
w_4 : WellFoundedLT w
hf : W.transfiniteCompositionsOfShape w f
⊢ W.rlp.llp f

Tactic:
W.transfiniteCompositionsOfShape_le_llp_rlp _ _ hf

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_llp_rlp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
w : Type w
w_1 : LinearOrder w
w_2 : SuccOrder w
w_3 : OrderBot w
w_4 : WellFoundedLT w
hf : W.transfiniteCompositionsOfShape w f
⊢ W.rlp.llp f

Tactic:
exact W.transfiniteCompositionsOfShape_le_llp_rlp _ _ hf

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_llp_rlp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp

Tactic:
simpa using transfiniteCompositions_le_llp_rlp.{w} (coproducts.{w} W).pushouts
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
rw : transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts).retracts ≤ W.rlp.llp

Tactic:
rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp]

Premises used: CategoryTheory.MorphismProperty.rlp_retracts, CategoryTheory.MorphismProperty.le_llp_iff_le_rlp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp

Tactic:
apply transfiniteCompositions_pushouts_coproducts_le_llp_rlp

Premises used: CategoryTheory.MorphismProperty.transfiniteCompositions_pushouts_coproducts_le_llp_rlp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
j : J
⊢ j ∈ Set.Iic j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
⊢ Cocone.pt (F := Φ.iterationFunctor J) (Φ.iterationCocone J) = Φ.iteration J

Tactic:
rfl

Premises used: CategoryTheory.SmallObject.SuccStruct.iteration, CategoryTheory.Limits.colimit, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i j : J
iter : Φ.Iteration j
hi : i ≤ j
⊢ i ≤ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
dsimp :
  Arrow.mk (X :=
      Functor.obj (C := (↑(Set.Iic i₁) : Type w)) (Iteration.F (Φ.iter i₁))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i₁) i₁ ⋯))
      (Y :=
      Functor.obj (C := (↑(Set.Iic i₂) : Type w)) (Iteration.F (Φ.iter i₂))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i₂) i₂ ⋯))
      (Iteration.mapObj (Φ.iter i₁) (Φ.iter i₂) ⋯ ⋯ ⋯ ⋯) =
    Arrow.mk (iter.F.map (homOfLE h₁₂))
⊢ Arrow.mk (X := Functor.obj (Φ.iterationFunctor J) i₁) (Functor.map (Φ.iterationFunctor J) (homOfLE h₁₂)) =
    Arrow.mk (iter.F.map (homOfLE h₁₂))

Tactic:
dsimp [iterationFunctor]

Premises used: CategoryTheory.SmallObject.SuccStruct.iterationFunctor
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
rw : arrowMap (Iteration.F (Φ.iter i₂)) i₁ i₂ ⋯ ⋯ = Arrow.mk (iter.F.map (homOfLE h₁₂))
⊢ Arrow.mk (X :=
      Functor.obj (C := (↑(Set.Iic i₁) : Type w)) (Iteration.F (Φ.iter i₁))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i₁) i₁ ⋯))
      (Y :=
      Functor.obj (C := (↑(Set.Iic i₂) : Type w)) (Iteration.F (Φ.iter i₂))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i₂) i₂ ⋯))
      (Iteration.mapObj (Φ.iter i₁) (Φ.iter i₂) ⋯ ⋯ ⋯ ⋯) =
    Arrow.mk (iter.F.map (homOfLE h₁₂))

Tactic:
rw [Iteration.arrow_mk_mapObj]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ arrowMap (Iteration.F (Φ.iter i₂)) i₁ i₂ ⋯ ⋯ = Arrow.mk (iter.F.map (homOfLE h₁₂))

Tactic:
Arrow.ext (Iteration.congr_obj _ _ _ _ _)
    (Iteration.congr_obj _ _ _ _ _) (Iteration.congr_map _ _ _ _ _)

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.congr_obj, CategoryTheory.SmallObject.SuccStruct.Iteration.congr_map, CategoryTheory.Arrow.ext
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
j : J
iter : Φ.Iteration j
hj : i₂ ≤ j
⊢ arrowMap (Iteration.F (Φ.iter i₂)) i₁ i₂ ⋯ ⋯ = Arrow.mk (iter.F.map (homOfLE h₁₂))

Tactic:
exact Arrow.ext (Iteration.congr_obj _ _ _ _ _)
    (Iteration.congr_obj _ _ _ _ _) (Iteration.congr_map _ _ _ _ _)

Premises used: CategoryTheory.Arrow.ext
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
⊢ i ≤ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
refine : IsColimit ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J)))
⊢ IsColimit (J := (↑(Set.Iio i) : Type w)) (F :=
    Monotone.functor (f :=
        (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
              x1 < x2) (Set.principalSegIio i)) :
          (a : (↑(Set.Iio i) : Type w)) → J))
        ⋯ ⋙
      Φ.iterationFunctor J)
    (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))

Tactic:
refine (IsColimit.precomposeInvEquiv e _).1 ?_

Premises used: Equiv.toFun, CategoryTheory.Limits.IsColimit.precomposeInvEquiv
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
⊢ i ≤ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
refine :
  coconeOfLE (Iteration.F (Φ.iter i)) ⋯ ≅
    (Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))
⊢ IsColimit ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J)))

Tactic:
refine IsColimit.ofIsoColimit ((Φ.iter i).isColimit i hi (by simp)) ?_

Premises used: CategoryTheory.SmallObject.SuccStruct.iter, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.SmallObject.SuccStruct.Iteration.isColimit
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
refine :
  ∀ (j : (↑(Set.Iio i) : Type w)),
    CategoryStruct.comp (Y :=
        Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) ⋯)
          (coconeOfLE (Iteration.F (Φ.iter i)) ⋯))
        (NatTrans.app (Cocone.ι (coconeOfLE (Iteration.F (Φ.iter i)) ⋯)) j :
          Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) j ⟶
            Functor.obj.{w, v, w, u}
              (Functor.obj (Functor.const (↑(Set.Iio i) : Type w))
                (Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) ⋯)
                  (coconeOfLE (Iteration.F (Φ.iter i)) ⋯)))
              j)
        (Iso.hom (eqToIso ⋯)) =
      ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))).ι.app j
⊢ coconeOfLE (Iteration.F (Φ.iter i)) ⋯ ≅
    (Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))

Tactic:
refine Cocone.ext (eqToIso (Φ.iterationFunctor_obj i (Φ.iter i) (by simp)).symm) ?_

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.eqToIso
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
k : J
hk : k ∈ Set.Iio i
a :
  Arrow.mk (X :=
      Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk)) (Y :=
      ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))).pt)
      (CategoryStruct.comp (Y :=
        Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) ⋯)
          (coconeOfLE (Iteration.F (Φ.iter i)) ⋯))
        (NatTrans.app (Cocone.ι (coconeOfLE (Iteration.F (Φ.iter i)) ⋯))
            (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) :
          Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ⟶
            Functor.obj.{w, v, w, u}
              (Functor.obj (Functor.const (↑(Set.Iio i) : Type w))
                (Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) ⋯)
                  (coconeOfLE (Iteration.F (Φ.iter i)) ⋯)))
              (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
        (Iso.hom (eqToIso ⋯))) =
    Arrow.mk (X :=
      Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      (((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))).ι.app
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) ⋯)
        (coconeOfLE (Iteration.F (Φ.iter i)) ⋯))
      (NatTrans.app (Cocone.ι (coconeOfLE (Iteration.F (Φ.iter i)) ⋯))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) :
        Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ⟶
          Functor.obj.{w, v, w, u}
            (Functor.obj (Functor.const (↑(Set.Iio i) : Type w))
              (Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) ⋯)
                (coconeOfLE (Iteration.F (Φ.iter i)) ⋯)))
            (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      (Iso.hom (eqToIso ⋯)) =
    ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))).ι.app
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk)

Tactic:
apply Arrow.mk_injective

Premises used: CategoryTheory.Arrow.mk_injective
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
k : J
hk : k ∈ Set.Iio i
⊢ i ≤ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
i : J
hi : Order.IsSuccLimit i
e : Iso (C := Functor.{w, v, w, u} (↑(Set.Iio i) : Type w) C)
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio i)) :
        (a : (↑(Set.Iio i) : Type w)) → J))
      ⋯ ⋙
    Φ.iterationFunctor J)
  (restrictionLT (Iteration.F (Φ.iter i)) ⋯) :=
  NatIso.ofComponents (fun (x : (↑(Set.Iio i) : Type w)) ↦ eqToIso ⋯) ⋯
k : J
hk : k ∈ Set.Iio i
⊢ Arrow.mk (X :=
      Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk)) (Y :=
      ((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))).pt)
      (CategoryStruct.comp (Y :=
        Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) ⋯)
          (coconeOfLE (Iteration.F (Φ.iter i)) ⋯))
        (NatTrans.app (Cocone.ι (coconeOfLE (Iteration.F (Φ.iter i)) ⋯))
            (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) :
          Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ⟶
            Functor.obj.{w, v, w, u}
              (Functor.obj (Functor.const (↑(Set.Iio i) : Type w))
                (Cocone.pt (J := (↑(Set.Iio i) : Type w)) (F := restrictionLT (Iteration.F (Φ.iter i)) ⋯)
                  (coconeOfLE (Iteration.F (Φ.iter i)) ⋯)))
              (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
        (Iso.hom (eqToIso ⋯))) =
    Arrow.mk (X :=
      Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      (((Cocone.precompose e.inv).obj (PrincipalSeg.cocone (Set.principalSegIio i) (Φ.iterationFunctor J))).ι.app
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))

Tactic:
simp [Φ.arrowMk_iterationFunctor_map k i hk.le (Φ.iter i) (by simp), e]

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowMk_iterationFunctor_map, CategoryTheory.SmallObject.SuccStruct.iter, LT.lt.le