∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y Z : C} (x : X ⟶ Y) (x_1 : Y ⟶ Z),
  {
      hom :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.fromSkeletonToSkeletonIso X).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x x_1)
            (CategoryTheory.fromSkeletonToSkeletonIso Z).inv) } =
    CategoryTheory.CategoryStruct.comp
      {
        hom :=
          CategoryTheory.CategoryStruct.comp (CategoryTheory.fromSkeletonToSkeletonIso X).hom
            (CategoryTheory.CategoryStruct.comp x (CategoryTheory.fromSkeletonToSkeletonIso Y).inv) }
      {
        hom :=
          CategoryTheory.CategoryStruct.comp (CategoryTheory.fromSkeletonToSkeletonIso Y).hom
            (CategoryTheory.CategoryStruct.comp x_1 (CategoryTheory.fromSkeletonToSkeletonIso Z).inv) }