-- 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₂
a :
  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)
⊢ Eq (α :=
    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₁) ⟶
      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₂)))
    (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:
apply Arrow.mk_injective

Premises used: CategoryTheory.Arrow.mk_injective