feat(CategoryTheory/Monoidal/Mon_): add simp lemmas (leanprover-commu…

…nity#10905)

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -469,6 +469,7 @@ theorem mul_rightUnitor {M : Mon_ C} :
   simp only [Category.assoc, Category.id_comp]
 #align Mon_.mul_right_unitor Mon_.mul_rightUnitor
 
+@[simps tensorObj_X tensorHom_hom]
 instance monMonoidalStruct : MonoidalCategoryStruct (Mon_ C) :=
   let tensorObj (M N : Mon_ C) : Mon_ C :=
     { X := M.X ⊗ N.X
@@ -497,14 +498,39 @@ instance monMonoidalStruct : MonoidalCategoryStruct (Mon_ C) :=
     leftUnitor := fun M ↦ isoOfIso (λ_ M.X) one_leftUnitor mul_leftUnitor
     rightUnitor := fun M ↦ isoOfIso (ρ_ M.X) one_rightUnitor mul_rightUnitor }
 
-instance monMonoidal : MonoidalCategory (Mon_ C) := .ofTensorHom
-  (tensor_id := by intros; ext; apply tensor_id)
-  (tensor_comp := by intros; ext; apply tensor_comp)
-  (associator_naturality := by intros; ext; dsimp; apply associator_naturality)
-  (leftUnitor_naturality := by intros; ext; dsimp; apply leftUnitor_naturality)
-  (rightUnitor_naturality := by intros; ext; dsimp; apply rightUnitor_naturality)
-  (pentagon := by intros; ext; dsimp; apply pentagon)
-  (triangle := by intros; ext; dsimp; apply triangle)
+@[simp]
+theorem tensorUnit_X : (𝟙_ (Mon_ C)).X = 𝟙_ C := rfl
+
+@[simp]
+theorem whiskerLeft_hom {X Y : Mon_ C} (f : X ⟶ Y) (Z : Mon_ C) :
+    (f ▷ Z).hom = f.hom ▷ Z.X := by
+  rw [← tensorHom_id]; rfl
+
+@[simp]
+theorem whiskerRight_hom (X : Mon_ C) {Y Z : Mon_ C} (f : Y ⟶ Z) :
+    (X ◁ f).hom = X.X ◁ f.hom := by
+  rw [← id_tensorHom]; rfl
+
+@[simp]
+theorem leftUnitor_hom_hom (X : Mon_ C) : (λ_ X).hom.hom = (λ_ X.X).hom := rfl
+
+@[simp]
+theorem leftUnitor_inv_hom (X : Mon_ C) : (λ_ X).inv.hom = (λ_ X.X).inv := rfl
+
+@[simp]
+theorem rightUnitor_hom_hom (X : Mon_ C) : (ρ_ X).hom.hom = (ρ_ X.X).hom := rfl
+
+@[simp]
+theorem rightUnitor_inv_hom (X : Mon_ C) : (ρ_ X).inv.hom = (ρ_ X.X).inv := rfl
+
+@[simp]
+theorem associator_hom_hom (X Y Z : Mon_ C) : (α_ X Y Z).hom.hom = (α_ X.X Y.X Z.X).hom := rfl
+
+@[simp]
+theorem associator_inv_hom (X Y Z : Mon_ C) : (α_ X Y Z).inv.hom = (α_ X.X Y.X Z.X).inv := rfl
+
+instance monMonoidal : MonoidalCategory (Mon_ C) where
+  tensorHom_def := by intros; ext; simp [tensorHom_def]
 #align Mon_.Mon_monoidal Mon_.monMonoidal
 
 end Mon_