Pullbacks and pushouts in a monoidal category

For numerous simp lemmas of the form f ≫ g = h, we add accompanying simp lemmas of the form Q ◁ f ≫ Q ◁ g = Q ◁ h and f ▷ Q ≫ g ▷ Q = h ▷ Q. This file and Mathlib.CategoryTheory.Monoidal.Limits.HasLimits are needed to define a monoidal category structure in Mathlib.CategoryTheory.Monoidal.Arrow.

TODO

An attribute should be developed to automatically generate lemmas of this form.

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_desc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Q : C} : CategoryStruct.comp (whiskerLeft Q inl) (whiskerLeft Q (hP.desc h k w)) = whiskerLeft Q h

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_desc_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Q Z✝ : C} (h✝ : tensorObj Q W ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Q inl) (CategoryStruct.comp (whiskerLeft Q (hP.desc h k w)) h✝) = CategoryStruct.comp (whiskerLeft Q h) h✝

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_desc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Q : C} : CategoryStruct.comp (whiskerLeft Q inr) (whiskerLeft Q (hP.desc h k w)) = whiskerLeft Q k

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_desc_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Q Z✝ : C} (h✝ : tensorObj Q W ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Q inr) (CategoryStruct.comp (whiskerLeft Q (hP.desc h k w)) h✝) = CategoryStruct.comp (whiskerLeft Q k) h✝

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inl_desc_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Q : C} : CategoryStruct.comp (whiskerRight inl Q) (whiskerRight (hP.desc h k w) Q) = whiskerRight h Q

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inl_desc_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Q Z✝ : C} (h✝ : tensorObj W Q ⟶ Z✝) : CategoryStruct.comp (whiskerRight inl Q) (CategoryStruct.comp (whiskerRight (hP.desc h k w) Q) h✝) = CategoryStruct.comp (whiskerRight h Q) h✝

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inr_desc_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Q : C} : CategoryStruct.comp (whiskerRight inr Q) (whiskerRight (hP.desc h k w) Q) = whiskerRight k Q

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inr_desc_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Q Z✝ : C} (h✝ : tensorObj W Q ⟶ Z✝) : CategoryStruct.comp (whiskerRight inr Q) (CategoryStruct.comp (whiskerRight (hP.desc h k w) Q) h✝) = CategoryStruct.comp (whiskerRight k Q) h✝

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_w {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {Q : C} : CategoryStruct.comp (whiskerLeft Q f) (whiskerLeft Q inl) = CategoryStruct.comp (whiskerLeft Q g) (whiskerLeft Q inr)

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_w_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {Q Z✝ : C} (h : tensorObj Q P ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Q f) (CategoryStruct.comp (whiskerLeft Q inl) h) = CategoryStruct.comp (whiskerLeft Q g) (CategoryStruct.comp (whiskerLeft Q inr) h)

theorem CategoryTheory.MonoidalCategory.IsPushout.w_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {Q : C} : CategoryStruct.comp (whiskerRight f Q) (whiskerRight inl Q) = CategoryStruct.comp (whiskerRight g Q) (whiskerRight inr Q)

theorem CategoryTheory.MonoidalCategory.IsPushout.w_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) {Q Z✝ : C} (h : tensorObj P Q ⟶ Z✝) : CategoryStruct.comp (whiskerRight f Q) (CategoryStruct.comp (whiskerRight inl Q) h) = CategoryStruct.comp (whiskerRight g Q) (CategoryStruct.comp (whiskerRight inr Q) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_inv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q : C} : CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) (whiskerLeft Q hP.isoPushout.inv) = whiskerLeft Q inl

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_inv_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q Z✝ : C} (h : tensorObj Q P ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) (CategoryStruct.comp (whiskerLeft Q hP.isoPushout.inv) h) = CategoryStruct.comp (whiskerLeft Q inl) h

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_inv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q : C} : CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) (whiskerLeft Q hP.isoPushout.inv) = whiskerLeft Q inr

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_inv_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q Z✝ : C} (h : tensorObj Q P ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) (CategoryStruct.comp (whiskerLeft Q hP.isoPushout.inv) h) = CategoryStruct.comp (whiskerLeft Q inr) h

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q : C} : CategoryStruct.comp (whiskerLeft Q inl) (whiskerLeft Q hP.isoPushout.hom) = whiskerLeft Q (Limits.pushout.inl f g)

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q Z✝ : C} (h : tensorObj Q (Limits.pushout f g) ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Q inl) (CategoryStruct.comp (whiskerLeft Q hP.isoPushout.hom) h) = CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) h

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q : C} : CategoryStruct.comp (whiskerLeft Q inr) (whiskerLeft Q hP.isoPushout.hom) = whiskerLeft Q (Limits.pushout.inr f g)

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q Z✝ : C} (h : tensorObj Q (Limits.pushout f g) ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Q inr) (CategoryStruct.comp (whiskerLeft Q hP.isoPushout.hom) h) = CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) h

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_inv_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q : C} : CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q) (whiskerRight hP.isoPushout.inv Q) = whiskerRight inl Q

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_inv_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q Z✝ : C} (h : tensorObj P Q ⟶ Z✝) : CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q) (CategoryStruct.comp (whiskerRight hP.isoPushout.inv Q) h) = CategoryStruct.comp (whiskerRight inl Q) h

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_inv_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q : C} : CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q) (whiskerRight hP.isoPushout.inv Q) = whiskerRight inr Q

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_inv_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q Z✝ : C} (h : tensorObj P Q ⟶ Z✝) : CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q) (CategoryStruct.comp (whiskerRight hP.isoPushout.inv Q) h) = CategoryStruct.comp (whiskerRight inr Q) h

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_hom_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q : C} : CategoryStruct.comp (whiskerRight inl Q) (whiskerRight hP.isoPushout.hom Q) = whiskerRight (Limits.pushout.inl f g) Q

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inl_isoPushout_hom_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q Z✝ : C} (h : tensorObj (Limits.pushout f g) Q ⟶ Z✝) : CategoryStruct.comp (whiskerRight inl Q) (CategoryStruct.comp (whiskerRight hP.isoPushout.hom Q) h) = CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q) h

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_hom_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q : C} : CategoryStruct.comp (whiskerRight inr Q) (whiskerRight hP.isoPushout.hom Q) = whiskerRight (Limits.pushout.inr f g) Q

@[simp]

theorem CategoryTheory.MonoidalCategory.IsPushout.inr_isoPushout_hom_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : IsPushout f g inl inr) [Limits.HasPushout f g] {Q Z✝ : C} (h : tensorObj (Limits.pushout f g) Q ⟶ Z✝) : CategoryStruct.comp (whiskerRight inr Q) (CategoryStruct.comp (whiskerRight hP.isoPushout.hom Q) h) = CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q) h

theorem CategoryTheory.MonoidalCategory.Limits.pushout.whiskerLeft_condition {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {Q : C} : CategoryStruct.comp (whiskerLeft Q f) (whiskerLeft Q (Limits.pushout.inl f g)) = CategoryStruct.comp (whiskerLeft Q g) (whiskerLeft Q (Limits.pushout.inr f g))

theorem CategoryTheory.MonoidalCategory.Limits.pushout.whiskerLeft_condition_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {Q Z✝ : C} (h : tensorObj Q (Limits.pushout f g) ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Q f) (CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) h) = CategoryStruct.comp (whiskerLeft Q g) (CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) h)

theorem CategoryTheory.MonoidalCategory.Limits.pushout.condition_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {Q : C} : CategoryStruct.comp (whiskerRight f Q) (whiskerRight (Limits.pushout.inl f g) Q) = CategoryStruct.comp (whiskerRight g Q) (whiskerRight (Limits.pushout.inr f g) Q)

theorem CategoryTheory.MonoidalCategory.Limits.pushout.condition_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {Q Z✝ : C} (h : tensorObj (Limits.pushout f g) Q ⟶ Z✝) : CategoryStruct.comp (whiskerRight f Q) (CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q) h) = CategoryStruct.comp (whiskerRight g Q) (CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q) h)

theorem CategoryTheory.MonoidalCategory.Limits.pushout.associator_naturality_left_condition {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {A B X Y Z W : C} {f : A ⟶ B} {g : X ⟶ Y} {h : tensorObj Z W ⟶ X} : CategoryStruct.comp (whiskerRight (whiskerRight f Z) W) (CategoryStruct.comp (associator B Z W).hom (CategoryStruct.comp (whiskerLeft B h) (Limits.pushout.inl (whiskerRight f X) (whiskerLeft A g)))) = CategoryStruct.comp (associator A Z W).hom (CategoryStruct.comp (whiskerLeft A (CategoryStruct.comp h g)) (Limits.pushout.inr (whiskerRight f X) (whiskerLeft A g)))

theorem CategoryTheory.MonoidalCategory.Limits.pushout.associator_naturality_left_condition_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {A B X Y Z W : C} {f : A ⟶ B} {g : X ⟶ Y} {h : tensorObj Z W ⟶ X} {Z✝ : C} (h✝ : Limits.pushout (whiskerRight f X) (whiskerLeft A g) ⟶ Z✝) : CategoryStruct.comp (whiskerRight (whiskerRight f Z) W) (CategoryStruct.comp (associator B Z W).hom (CategoryStruct.comp (whiskerLeft B h) (CategoryStruct.comp (Limits.pushout.inl (whiskerRight f X) (whiskerLeft A g)) h✝))) = CategoryStruct.comp (associator A Z W).hom (CategoryStruct.comp (whiskerLeft A (CategoryStruct.comp h g)) (CategoryStruct.comp (Limits.pushout.inr (whiskerRight f X) (whiskerLeft A g)) h✝))

theorem CategoryTheory.MonoidalCategory.Limits.pushout.associator_inv_naturality_right_condition {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {A B X Y Z W : C} {f : A ⟶ B} {g : X ⟶ Y} {h : tensorObj Z W ⟶ A} : CategoryStruct.comp (whiskerLeft Z (whiskerLeft W g)) (CategoryStruct.comp (associator Z W Y).inv (CategoryStruct.comp (whiskerRight h Y) (Limits.pushout.inr (whiskerRight f X) (whiskerLeft A g)))) = CategoryStruct.comp (associator Z W X).inv (CategoryStruct.comp (whiskerRight (CategoryStruct.comp h f) X) (Limits.pushout.inl (whiskerRight f X) (whiskerLeft A g)))

theorem CategoryTheory.MonoidalCategory.Limits.pushout.associator_inv_naturality_right_condition_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {A B X Y Z W : C} {f : A ⟶ B} {g : X ⟶ Y} {h : tensorObj Z W ⟶ A} {Z✝ : C} (h✝ : Limits.pushout (whiskerRight f X) (whiskerLeft A g) ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Z (whiskerLeft W g)) (CategoryStruct.comp (associator Z W Y).inv (CategoryStruct.comp (whiskerRight h Y) (CategoryStruct.comp (Limits.pushout.inr (whiskerRight f X) (whiskerLeft A g)) h✝))) = CategoryStruct.comp (associator Z W X).inv (CategoryStruct.comp (whiskerRight (CategoryStruct.comp h f) X) (CategoryStruct.comp (Limits.pushout.inl (whiskerRight f X) (whiskerLeft A g)) h✝))

@[simp]

theorem CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inl_comp_pushoutSymmetry_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) (whiskerLeft Q (Limits.pushoutSymmetry f g).hom) = whiskerLeft Q (Limits.pushout.inr g f)

@[simp]

theorem CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inl_comp_pushoutSymmetry_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : tensorObj Q (Limits.pushout g f) ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl f g)) (CategoryStruct.comp (whiskerLeft Q (Limits.pushoutSymmetry f g).hom) h) = CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr g f)) h

@[simp]

theorem CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inr_comp_pushoutSymmetry_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) (whiskerLeft Q (Limits.pushoutSymmetry f g).hom) = whiskerLeft Q (Limits.pushout.inl g f)

@[simp]

theorem CategoryTheory.MonoidalCategory.Limits.whiskerLeft_inr_comp_pushoutSymmetry_hom_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : tensorObj Q (Limits.pushout g f) ⟶ Z✝) : CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inr f g)) (CategoryStruct.comp (whiskerLeft Q (Limits.pushoutSymmetry f g).hom) h) = CategoryStruct.comp (whiskerLeft Q (Limits.pushout.inl g f)) h

@[simp]

theorem CategoryTheory.MonoidalCategory.Limits.inl_comp_pushoutSymmetry_hom_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q) (whiskerRight (Limits.pushoutSymmetry f g).hom Q) = whiskerRight (Limits.pushout.inr g f) Q

@[simp]

theorem CategoryTheory.MonoidalCategory.Limits.inl_comp_pushoutSymmetry_hom_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : tensorObj (Limits.pushout g f) Q ⟶ Z✝) : CategoryStruct.comp (whiskerRight (Limits.pushout.inl f g) Q) (CategoryStruct.comp (whiskerRight (Limits.pushoutSymmetry f g).hom Q) h) = CategoryStruct.comp (whiskerRight (Limits.pushout.inr g f) Q) h

@[simp]

theorem CategoryTheory.MonoidalCategory.Limits.inr_comp_pushoutSymmetry_hom_whiskerRight {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q) (whiskerRight (Limits.pushoutSymmetry f g).hom Q) = whiskerRight (Limits.pushout.inl g f) Q

@[simp]

theorem CategoryTheory.MonoidalCategory.Limits.inr_comp_pushoutSymmetry_hom_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasPushouts C] {Q X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : tensorObj (Limits.pushout g f) Q ⟶ Z✝) : CategoryStruct.comp (whiskerRight (Limits.pushout.inr f g) Q) (CategoryStruct.comp (whiskerRight (Limits.pushoutSymmetry f g).hom Q) h) = CategoryStruct.comp (whiskerRight (Limits.pushout.inl g f) Q) h