-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (goal)
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₂
⊢ 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)
have 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))
          sorry ⋙
        Φ.iterationFunctor J)
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁))
    (Y := Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) sorry) (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))
            sorry ⋙
          Φ.iterationFunctor J)
        f ≫
      Iso.hom
        ((fun (x : (↑(Set.Iio i) : Type w)) ↦
            (eqToIso sorry :
              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))
                      sorry ⋙
                    Φ.iterationFunctor J)
                  x ≅
                Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) sorry) 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))
          sorry ⋙
        Φ.iterationFunctor J)
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁))
    (Y := Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) sorry) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂))
    (Iso.hom
        ((fun (x : (↑(Set.Iio i) : Type w)) ↦
            (eqToIso sorry :
              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))
                      sorry ⋙
                    Φ.iterationFunctor J)
                  x ≅
                Functor.obj (restrictionLT (Iteration.F (Φ.iter i)) sorry) x))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁)) ≫
      Functor.map (restrictionLT (Iteration.F (Φ.iter i)) sorry) f)
Tactic: apply Arrow.mk_injective