-- 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
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂
⊢ Arrow.mk (X :=
      Functor.obj
        (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)
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁))
      (Y :=
      Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂))
      (Functor.map
          (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)
          f ≫
        Iso.hom
          ((fun (x : (↑(Set.Iio i) : Type w)) ↦
              (eqToIso ⋯ :
                Functor.obj
                    (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)
                    x ≅
                  Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) x))
            (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂))) =
    Arrow.mk (X :=
      Functor.obj
        (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)
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁))
      (Y :=
      Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂))
      (Iso.hom
          ((fun (x : (↑(Set.Iio i) : Type w)) ↦
              (eqToIso ⋯ :
                Functor.obj
                    (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)
                    x ≅
                  Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) ⋯) x))
            (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁)) ≫
        Functor.map (restrictionLT (Iteration.F (Φ.iter i)) ⋯) f)

Tactic:
simpa using Φ.arrowMk_iterationFunctor_map k₁ k₂ (leOfHom f) (Φ.iter i) h₂.le

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