∀ {C : Type u₁} [inst : CategoryTheory.Category.{v_1, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v_2, u₂} D] (F : CategoryTheory.Functor C D) {X Y Z : C} (f : Y ⟶ X) (g : Z ⟶ Y)
  {W : D} (h : W ⟶ F.obj Z),
  CategoryTheory.CategoryStruct.comp h (F.map (CategoryTheory.CategoryStruct.comp g f)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h (F.map g)) (F.map f)