Commit 2024-02-26 23:59 cda31e7e

View on Github →

refactor(CategoryTheory/Monoidal/Rigid): use monoidalComp in the proofs (#10326) Similar to #10078

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

added theorem CategoryTheory.MonoidalFunctor.map_whiskerLeft'

added theorem CategoryTheory.MonoidalFunctor.map_whiskerRight'

Modified Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean

added theorem CategoryTheory.ExactPairing.coevaluation_evaluation''

added theorem CategoryTheory.ExactPairing.evaluation_coevaluation''

deleted theorem CategoryTheory.tensorLeftHomEquiv_id_tensor_comp_evaluation

deleted theorem CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_id_tensor

deleted theorem CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_tensor_id

added theorem CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerLeft

added theorem CategoryTheory.tensorLeftHomEquiv_symm_coevaluation_comp_whiskerRight

deleted theorem CategoryTheory.tensorLeftHomEquiv_tensor_id_comp_evaluation

added theorem CategoryTheory.tensorLeftHomEquiv_whiskerLeft_comp_evaluation

added theorem CategoryTheory.tensorLeftHomEquiv_whiskerRight_comp_evaluation

deleted theorem CategoryTheory.tensorRightHomEquiv_id_tensor_comp_evaluation

deleted theorem CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_id_tensor

deleted theorem CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_tensor_id

added theorem CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerLeft

added theorem CategoryTheory.tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight

deleted theorem CategoryTheory.tensorRightHomEquiv_tensor_id_comp_evaluation

added theorem CategoryTheory.tensorRightHomEquiv_whiskerLeft_comp_evaluation

added theorem CategoryTheory.tensorRightHomEquiv_whiskerRight_comp_evaluation

Modified Mathlib/CategoryTheory/Monoidal/Rigid/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean