# Documentation

Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

# Lemmas which are consequences of monoidal coherence #

These lemmas are all proved by coherence.

## Future work #

Investigate whether these lemmas are really needed, or if they can be replaced by use of the coherence tactic.

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor'_assoc {C : Type u_1} [] (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_assoc {C : Type u_1} [] (X : C) (Y : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor {C : Type u_1} [] (X : C) (Y : C) :
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv_assoc {C : Type u_1} [] (X : C) (Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj CategoryTheory.MonoidalCategory.tensorUnit' () Z) :
theorem CategoryTheory.MonoidalCategory.id_tensor_rightUnitor_inv {C : Type u_1} [] (X : C) (Y : C) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y CategoryTheory.MonoidalCategory.tensorUnit').hom
theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_id {C : Type u_1} [] (X : C) (Y : C) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator CategoryTheory.MonoidalCategory.tensorUnit' X Y).inv
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_assoc {C : Type u_1} [] (W : C) (X : C) (Y : C) (Z : C) {Z : C} :
=
theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom {C : Type u_1} [] (W : C) (X : C) (Y : C) (Z : C) :
@[simp]
theorem CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv_assoc {C : Type u_1} [] (X : C) (Y : C) {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv_assoc {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} {Z : C} :
=
theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} :
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_assoc {C : Type u_1} [] (W : C) (X : C) (Y : C) (Z : C) {Z : C} :
=
theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom {C : Type u_1} [] (W : C) (X : C) (Y : C) (Z : C) :