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 (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 (CategoryStruct.id W, CategoryStruct.comp f g) = CategoryStruct.comp (F.map (CategoryStruct.id W, f)) (F.map (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 (CategoryStruct.comp f g, CategoryStruct.id W) = CategoryStruct.comp (F.map (f, CategoryStruct.id W)) (F.map (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 (CategoryStruct.id X, g)) (F.map (f, CategoryStruct.id Y')) = F.map (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 (f, CategoryStruct.id Y)) (F.map (CategoryStruct.id X', g)) = F.map (f, g)