∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j),
  CategoryTheory.SmallObject.SuccStruct.arrowMap (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ) i₁ i₂ hi
      ⋯ =
    CategoryTheory.SmallObject.SuccStruct.arrowMap F i₁ i₂ hi hi₂