∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (X : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] (X_1 : C),
  CategoryTheory.CategoryStruct.comp
      ({
            app := fun x =>
              CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
                (CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.prod.functor.obj X).obj x)),
            naturality := ⋯ }.app
        X_1)
      ((CategoryTheory.Limits.prod.functor.obj X).map
        ({
              app := fun x =>
                CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
                  (CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.prod.functor.obj X).obj x)),
              naturality := ⋯ }.app
          X_1)) =
    CategoryTheory.CategoryStruct.comp
      ({
            app := fun x =>
              CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
                (CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.prod.functor.obj X).obj x)),
            naturality := ⋯ }.app
        X_1)
      ({
            app := fun x =>
              CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
                (CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.prod.functor.obj X).obj x)),
            naturality := ⋯ }.app
        ((CategoryTheory.Limits.prod.functor.obj X).obj X_1))