Lemmas about functors out of product categories.

@[simp]

theorem CategoryTheory.Bifunctor.map_id {C : Type u₁} {D : Type u₂} {E : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] (F : Functor (C × D) E) (X : C) (Y : D) : F.map (Prod.mkHom (CategoryStruct.id X) (CategoryStruct.id Y)) = CategoryStruct.id (F.obj (X, Y))

@[simp]

theorem CategoryTheory.Bifunctor.map_id_comp {C : Type u₁} {D : Type u₂} {E : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] (F : Functor (C × D) E) (W : C) {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z) : F.map (Prod.mkHom (CategoryStruct.id W) (CategoryStruct.comp f g)) = CategoryStruct.comp (F.map (Prod.mkHom (CategoryStruct.id W) f)) (F.map (Prod.mkHom (CategoryStruct.id W) g))

@[simp]

theorem CategoryTheory.Bifunctor.map_comp_id {C : Type u₁} {D : Type u₂} {E : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] (F : Functor (C × D) E) (X Y Z : C) (W : D) (f : X ⟶ Y) (g : Y ⟶ Z) : F.map (Prod.mkHom (CategoryStruct.comp f g) (CategoryStruct.id W)) = CategoryStruct.comp (F.map (Prod.mkHom f (CategoryStruct.id W))) (F.map (Prod.mkHom g (CategoryStruct.id W)))

@[simp]

theorem CategoryTheory.Bifunctor.diagonal {C : Type u₁} {D : Type u₂} {E : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] (F : Functor (C × D) E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y') : CategoryStruct.comp (F.map (Prod.mkHom (CategoryStruct.id X) g)) (F.map (Prod.mkHom f (CategoryStruct.id Y'))) = F.map (Prod.mkHom f g)

@[simp]

theorem CategoryTheory.Bifunctor.diagonal' {C : Type u₁} {D : Type u₂} {E : Type u₃} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Category.{v₃, u₃} E] (F : Functor (C × D) E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y') : CategoryStruct.comp (F.map (Prod.mkHom f (CategoryStruct.id Y))) (F.map (Prod.mkHom (CategoryStruct.id X') g)) = F.map (Prod.mkHom f g)