∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.toSkeletonFunctor C).map f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.fromSkeletonToSkeletonIso X).hom
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.fromSkeletonToSkeletonIso Y).inv)