Lemmas that should possibly be in mathlib. Do not introduce new definitions here.

Over categories

theorem CategoryTheory.Over.homMk_comp {C : Type u_1} [Category.{u_2, u_1} C] {B : C} {U V W : Over B} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) (fg_comp : CategoryStruct.comp (CategoryStruct.comp f g) W.hom = U.hom) (f_comp : CategoryStruct.comp f V.hom = U.hom) (g_comp : CategoryStruct.comp g W.hom = V.hom) : homMk (CategoryStruct.comp f g) fg_comp = CategoryStruct.comp (homMk f f_comp) (homMk g g_comp)

This is useful when homMk (· ≫ ·) appears under Functor.map or a natural equivalence.

@[simp]

theorem CategoryTheory.Over.left_homMk {C : Type u_1} [Category.{u_2, u_1} C] {B : C} {U V : Over B} (f : U ⟶ V) (h : CategoryStruct.comp f.left V.hom = U.hom) : homMk f.left h = f

ChosenFiniteProducts.ofFiniteProducts

Simplify monoidal structure coming from HasFiniteProducts into prod.foo. See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cartesian.20closed.20Monoidal.20categories.2E

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.ofFiniteProducts_fst {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasFiniteProducts C] (X Y : C) : fst X Y = Limits.prod.fst

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.ofFiniteProducts_snd {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasFiniteProducts C] (X Y : C) : snd X Y = Limits.prod.snd

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.ofFiniteProducts_whiskerLeft {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasFiniteProducts C] {Y Z : C} (X : C) (f : Y ⟶ Z) : MonoidalCategoryStruct.whiskerLeft X f = Limits.prod.map (CategoryStruct.id X) f

@[simp]

theorem CategoryTheory.ChosenFiniteProducts.ofFiniteProducts_whiskerRight {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasFiniteProducts C] {X Y : C} (Z : C) (f : X ⟶ Y) : MonoidalCategoryStruct.whiskerRight f Z = Limits.prod.map f (CategoryStruct.id Z)