∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : Type u_1} [inst_2 : CategoryTheory.SmallCategory J] {K : CategoryTheory.Functor J C} (X : C) ⦃X_1 Y : J⦄
  (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((K.comp (CategoryTheory.Limits.prod.functor.obj X)).map f)
      CategoryTheory.Limits.prod.snd =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (K.map f)