∀ (C : Type u_3) [inst : CategoryTheory.Category.{u_1, u_3} C] (D : Type u_4)
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] {x x_1 : C} (f : x ⟶ x_1) ⦃X Y : CategoryTheory.Functor C D⦄
  (f_1 : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ({ obj := fun F => F.obj x, map := fun {X Y} α => α.app x, map_id := ⋯, map_comp := ⋯ }.map f_1) (Y.map f) =
    CategoryTheory.CategoryStruct.comp (X.map f)
      ({ obj := fun F => F.obj x_1, map := fun {X Y} α => α.app x_1, map_id := ⋯, map_comp := ⋯ }.map f_1)