[Merged by Bors] - refactor(CategoryTheory/Monoidal): split the naturality condition of monoidal functors

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -186,15 +186,15 @@ theorem associativity (X Y Z : Type u) :
 -- In fact, it's strong monoidal, but we don't yet have a typeclass for that.
 /-- The free R-module functor is lax monoidal. -/
 @[simps]
-instance : LaxMonoidal.{u} (free R).obj where
+instance : LaxMonoidal.{u} (free R).obj := .ofTensorHom
   -- Send `R` to `PUnit →₀ R`
-  ε := ε R
+  (ε := ε R)
   -- Send `(α →₀ R) ⊗ (β →₀ R)` to `α × β →₀ R`
-  μ X Y := (μ R X Y).hom
-  μ_natural {_} {_} {_} {_} f g := μ_natural R f g
-  left_unitality := left_unitality R
-  right_unitality := right_unitality R
-  associativity := associativity R
+  (μ := fun X Y => (μ R X Y).hom)
+  (μ_natural := fun {_} {_} {_} {_} f g ↦ μ_natural R f g)
+  (left_unitality := left_unitality R)
+  (right_unitality := right_unitality R)
+  (associativity := associativity R)
 
 instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by
   refine' ⟨⟨Finsupp.lapply PUnit.unit, ⟨_, _⟩⟩⟩

Mathlib/CategoryTheory/Bicategory/SingleObj.lean

@@ -86,7 +86,12 @@ def endMonoidalStarFunctor : MonoidalFunctor (EndMonoidal (MonoidalSingleObj.sta
   map f := f
   ε := 𝟙 _
   μ X Y := 𝟙 _
-  μ_natural f g := by
+  -- The proof will be automated after merging #6307.
+  μ_natural_left f g := by
+    simp_rw [Category.id_comp, Category.comp_id]
+    -- Should we provide further simp lemmas so this goal becomes visible?
+    exact (tensor_id_comp_id_tensor _ _).symm
+  μ_natural_right f g := by
     simp_rw [Category.id_comp, Category.comp_id]
     -- Should we provide further simp lemmas so this goal becomes visible?
     exact (tensor_id_comp_id_tensor _ _).symm

Mathlib/CategoryTheory/Monoidal/Braided.lean

@@ -421,6 +421,18 @@ theorem tensor_μ_natural {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ :
   simp only [assoc]
 #align category_theory.tensor_μ_natural CategoryTheory.tensor_μ_natural
 
+@[reassoc]
+theorem tensor_μ_natural_left {X₁ X₂ Y₁ Y₂ : C} (f₁: X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (Z₁ Z₂ : C) :
+    ((f₁ ⊗ f₂) ⊗ 𝟙 (Z₁ ⊗ Z₂)) ≫ tensor_μ C (Y₁, Y₂) (Z₁, Z₂) =
+      tensor_μ C (X₁, X₂) (Z₁, Z₂) ≫ ((f₁ ⊗ 𝟙 Z₁) ⊗ (f₂ ⊗ 𝟙 Z₂)) := by
+  convert tensor_μ_natural C f₁ f₂ (𝟙 Z₁) (𝟙 Z₂) using 1; simp
+
+@[reassoc]
+theorem tensor_μ_natural_right (Z₁ Z₂ : C) {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) :
+    (𝟙 (Z₁ ⊗ Z₂) ⊗ (f₁ ⊗ f₂)) ≫ tensor_μ C (Z₁, Z₂) (Y₁, Y₂) =
+      tensor_μ C (Z₁, Z₂) (X₁, X₂) ≫ ((𝟙 Z₁ ⊗ f₁) ⊗ (𝟙 Z₂ ⊗ f₂)) := by
+  convert tensor_μ_natural C (𝟙 Z₁) (𝟙 Z₂) f₁ f₂ using 1; simp
+
 theorem tensor_left_unitality (X₁ X₂ : C) :
     (λ_ (X₁ ⊗ X₂)).hom =
       ((λ_ (𝟙_ C)).inv ⊗ 𝟙 (X₁ ⊗ X₂)) ≫
@@ -566,8 +578,9 @@ theorem tensor_associativity (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) :
 def tensorMonoidal : MonoidalFunctor (C × C) C :=
   { tensor C with
     ε := (λ_ (𝟙_ C)).inv
-    μ := fun X Y => tensor_μ C X Y
-    μ_natural := fun f g => tensor_μ_natural C f.1 f.2 g.1 g.2
+    μ := tensor_μ C
+    μ_natural_left := fun f Z => tensor_μ_natural_left C f.1 f.2 Z.1 Z.2
+    μ_natural_right := fun Z f => tensor_μ_natural_right C Z.1 Z.2 f.1 f.2
     associativity := fun X Y Z => tensor_associativity C X.1 X.2 Y.1 Y.2 Z.1 Z.2
     left_unitality := fun ⟨X₁, X₂⟩ => tensor_left_unitality C X₁ X₂
     right_unitality := fun ⟨X₁, X₂⟩ => tensor_right_unitality C X₁ X₂

Mathlib/CategoryTheory/Monoidal/End.lean

@@ -97,11 +97,19 @@ def tensoringRightMonoidal [MonoidalCategory.{v} C] : MonoidalFunctor C (C ⥤ C
   { tensoringRight C with
     ε := (rightUnitorNatIso C).inv
     μ := fun X Y => { app := fun Z => (α_ Z X Y).hom }
-    μ_natural := fun f g => by
+    -- The proof will be automated after merging #6307.
+    μ_natural_left := fun f X => by
       ext Z
       dsimp
-      simp only [← id_tensor_comp_tensor_id g f, id_tensor_comp, ← tensor_id, Category.assoc,
+      simp only [← id_tensor_comp_tensor_id f (𝟙 X), id_tensor_comp, ← tensor_id, Category.assoc,
         associator_naturality, associator_naturality_assoc]
+      simp only [tensor_id, Category.id_comp]
+    μ_natural_right := fun X g => by
+      ext Z
+      dsimp
+      simp only [← id_tensor_comp_tensor_id (𝟙 X) g, id_tensor_comp, ← tensor_id, Category.assoc,
+        associator_naturality, associator_naturality_assoc]
+      simp only [tensor_id, Category.comp_id]
     associativity := fun X Y Z => by
       ext W
       simp [pentagon]

Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

@@ -341,13 +341,17 @@ def project : MonoidalFunctor (F C) D where
   map_comp := by rintro _ _ _ ⟨_⟩ ⟨_⟩; rfl
   ε := 𝟙 _
   μ X Y := 𝟙 _
-  μ_natural := @fun _ _ _ _ f g => by
+  μ_natural_left := fun f _ => by
     induction' f using Quotient.recOn
-    · induction' g using Quotient.recOn
-      · dsimp
-        simp
-        rfl
-      · rfl
+    · dsimp
+      simp
+      rfl
+    · rfl
+  μ_natural_right := fun _ f => by
+    induction' f using Quotient.recOn
+    · dsimp
+      simp
+      rfl
     · rfl
 #align category_theory.free_monoidal_category.project CategoryTheory.FreeMonoidalCategory.project
 

Mathlib/CategoryTheory/Monoidal/Functor.lean

@@ -69,9 +69,13 @@ structure LaxMonoidalFunctor extends C ⥤ D where
   ε : 𝟙_ D ⟶ obj (𝟙_ C)
   /-- tensorator -/
   μ : ∀ X Y : C, obj X ⊗ obj Y ⟶ obj (X ⊗ Y)
-  μ_natural :
-    ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
-      (map f ⊗ map g) ≫ μ Y Y' = μ X X' ≫ map (f ⊗ g) := by
+  μ_natural_left :
+    ∀ {X Y : C} (f : X ⟶ Y) (X' : C),
+      (map f ⊗ 𝟙 (obj X')) ≫ μ Y X' = μ X X' ≫ map (f ⊗ 𝟙 X') := by
+    aesop_cat
+  μ_natural_right :
+    ∀ {X Y : C} (X' : C) (f : X ⟶ Y) ,
+      (𝟙 (obj X') ⊗ map f) ≫ μ X' Y = μ X' X ≫ map (𝟙 X' ⊗ f) := by
     aesop_cat
   /-- associativity of the tensorator -/
   associativity :
@@ -93,7 +97,8 @@ structure LaxMonoidalFunctor extends C ⥤ D where
 initialize_simps_projections LaxMonoidalFunctor (+toFunctor, -obj, -map)
 
 --Porting note: was `[simp, reassoc.1]`
-attribute [reassoc (attr := simp)] LaxMonoidalFunctor.μ_natural
+attribute [reassoc (attr := simp)] LaxMonoidalFunctor.μ_natural_left
+attribute [reassoc (attr := simp)] LaxMonoidalFunctor.μ_natural_right
 
 attribute [simp] LaxMonoidalFunctor.left_unitality
 
@@ -109,6 +114,59 @@ section
 
 variable {C D}
 
+@[reassoc (attr := simp)]
+theorem  LaxMonoidalFunctor.μ_natural (F : LaxMonoidalFunctor C D) {X Y X' Y' : C}
+    (f : X ⟶ Y) (g : X' ⟶ Y') :
+      (F.map f ⊗ F.map g) ≫ F.μ Y Y' = F.μ X X' ≫ F.map (f ⊗ g) := by
+  rw [← tensor_id_comp_id_tensor_assoc]
+  rw [F.μ_natural_right, F.μ_natural_left_assoc]
+  rw [← F.map_comp, tensor_id_comp_id_tensor]
+
+/--
+A constructor for lax monoidal functors whose axioms are described by `tensorHom` instead of
+`whiskerLeft` and `whiskerRight`.
+-/
+@[simps]
+def LaxMonoidalFunctor.ofTensorHom (F : C ⥤ D)
+    /- unit morphism -/
+    (ε : 𝟙_ D ⟶ F.obj (𝟙_ C))
+    /- tensorator -/
+    (μ : ∀ X Y : C, F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y))
+    (μ_natural :
+      ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
+        (F.map f ⊗ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ g) := by
+      aesop_cat)
+    /- associativity of the tensorator -/
+    (associativity :
+      ∀ X Y Z : C,
+        (μ X Y ⊗ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
+          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z) := by
+      aesop_cat)
+    /- unitality -/
+    (left_unitality :
+      ∀ X : C, (λ_ (F.obj X)).hom = (ε ⊗ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom :=
+        by aesop_cat)
+    (right_unitality :
+      ∀ X : C, (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom :=
+        by aesop_cat) :
+        LaxMonoidalFunctor C D where
+  obj := F.obj
+  map := F.map
+  map_id := F.map_id
+  map_comp := F.map_comp
+  ε := ε
+  μ := μ
+  μ_natural_left := fun f X' => by
+    simp_rw [← F.map_id, μ_natural]
+  μ_natural_right := fun X' f => by
+    simp_rw [← F.map_id, μ_natural]
+  associativity := fun X Y Z => by
+    simp_rw [associativity]
+  left_unitality := fun X => by
+    simp_rw [left_unitality]
+  right_unitality := fun X => by
+    simp_rw [right_unitality]
+
 --Porting note: was `[simp, reassoc.1]`
 @[reassoc (attr := simp)]
 theorem LaxMonoidalFunctor.left_unitality_inv (F : LaxMonoidalFunctor C D) (X : C) :
@@ -320,10 +378,12 @@ def comp : LaxMonoidalFunctor.{v₁, v₃} C E :=
   { F.toFunctor ⋙ G.toFunctor with
     ε := G.ε ≫ G.map F.ε
     μ := fun X Y => G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y)
-    μ_natural := @fun _ _ _ _ f g => by
-      simp only [Functor.comp_map, assoc]
-      rw [← Category.assoc, LaxMonoidalFunctor.μ_natural, Category.assoc, ← map_comp, ← map_comp,
-        ← LaxMonoidalFunctor.μ_natural]
+    μ_natural_left := by
+      intro X Y f X'
+      simp_rw [comp_obj, F.comp_map, μ_natural_left_assoc, assoc, ← G.map_comp, μ_natural_left]
+    μ_natural_right := by
+      intro X Y f X'
+      simp_rw [comp_obj, F.comp_map, μ_natural_right_assoc, assoc, ← G.map_comp, μ_natural_right]
     associativity := fun X Y Z => by
       dsimp
       rw [id_tensor_comp]
@@ -482,17 +542,18 @@ end MonoidalFunctor
 /-- If we have a right adjoint functor `G` to a monoidal functor `F`, then `G` has a lax monoidal
 structure as well.
 -/
-@[simps]
+@[simp]
 noncomputable def monoidalAdjoint (F : MonoidalFunctor C D) {G : D ⥤ C} (h : F.toFunctor ⊣ G) :
-    LaxMonoidalFunctor D C where
-  toFunctor := G
-  ε := h.homEquiv _ _ (inv F.ε)
-  μ X Y := h.homEquiv _ (X ⊗ Y) (inv (F.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y))
-  μ_natural := @fun X Y X' Y' f g => by
+    LaxMonoidalFunctor D C := LaxMonoidalFunctor.ofTensorHom
+  (F := G)
+  (ε := h.homEquiv _ _ (inv F.ε))
+  (μ := fun X Y ↦
+    h.homEquiv _ (X ⊗ Y) (inv (F.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y)))
+  (μ_natural := @fun X Y X' Y' f g => by
     rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_right, Equiv.apply_eq_iff_eq, assoc,
       IsIso.eq_inv_comp, ← F.toLaxMonoidalFunctor.μ_natural_assoc, IsIso.hom_inv_id_assoc, ←
-      tensor_comp, Adjunction.counit_naturality, Adjunction.counit_naturality, tensor_comp]
-  associativity X Y Z := by
+      tensor_comp, Adjunction.counit_naturality, Adjunction.counit_naturality, tensor_comp])
+  (associativity := fun X Y Z ↦ by
     dsimp only
     rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ←
       h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, Equiv.apply_eq_iff_eq, ←
@@ -505,21 +566,21 @@ noncomputable def monoidalAdjoint (F : MonoidalFunctor C D) {G : D ⥤ C} (h : F
       tensor_comp_assoc, id_comp, id_comp, h.homEquiv_unit, h.homEquiv_unit, Functor.map_comp,
       assoc, assoc, h.counit_naturality, h.left_triangle_components_assoc, Functor.map_comp,
       assoc, h.counit_naturality, h.left_triangle_components_assoc]
-    simp
-  left_unitality X := by
+    simp)
+  (left_unitality := fun X ↦ by
     rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← Equiv.symm_apply_eq,
       h.homEquiv_counit, F.map_leftUnitor, h.homEquiv_unit, assoc, assoc, assoc, F.map_tensor,
       assoc, assoc, IsIso.hom_inv_id_assoc, ← tensor_comp_assoc, Functor.map_id, id_comp,
       Functor.map_comp, assoc, h.counit_naturality, h.left_triangle_components_assoc, ←
       leftUnitor_naturality, ← tensor_comp_assoc, id_comp, comp_id]
-    simp
-  right_unitality X := by
+    simp)
+  (right_unitality := fun X ↦  by
     rw [← h.homEquiv_naturality_right, ← h.homEquiv_naturality_left, ← Equiv.symm_apply_eq,
       h.homEquiv_counit, F.map_rightUnitor, assoc, assoc, ← rightUnitor_naturality, ←
       tensor_comp_assoc, comp_id, id_comp, h.homEquiv_unit, F.map_tensor, assoc, assoc, assoc,
       IsIso.hom_inv_id_assoc, Functor.map_comp, Functor.map_id, ← tensor_comp_assoc, assoc,
       h.counit_naturality, h.left_triangle_components_assoc, id_comp]
-    simp
+    simp)
 #align category_theory.monoidal_adjoint CategoryTheory.monoidalAdjoint
 
 /-- If a monoidal functor `F` is an equivalence of categories then its inverse is also monoidal. -/

Mathlib/CategoryTheory/Monoidal/Functorial.lean

@@ -55,11 +55,14 @@ class LaxMonoidal (F : C → D) [Functorial.{v₁, v₂} F] where
   ε : 𝟙_ D ⟶ F (𝟙_ C)
   /-- tensorator -/
   μ : ∀ X Y : C, F X ⊗ F Y ⟶ F (X ⊗ Y)
-  /-- naturality -/
-  μ_natural :
-    ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
-      (map F f ⊗ map F g) ≫ μ Y Y' = μ X X' ≫ map F (f ⊗ g) := by
-   aesop_cat
+  μ_natural_left :
+    ∀ {X Y : C} (f : X ⟶ Y) (X' : C),
+      (map F f ⊗ 𝟙 (F X')) ≫ μ Y X' = μ X X' ≫ map F (f ⊗ 𝟙 X') := by
+    aesop_cat
+  μ_natural_right :
+    ∀ {X Y : C} (X' : C) (f : X ⟶ Y) ,
+      (𝟙 (F X') ⊗ map F f) ≫ μ X' Y = μ X' X ≫ map F (𝟙 X' ⊗ f) := by
+    aesop_cat
   /-- associativity of the tensorator -/
   associativity :
     ∀ X Y Z : C,
@@ -74,9 +77,39 @@ class LaxMonoidal (F : C → D) [Functorial.{v₁, v₂} F] where
     aesop_cat
 #align category_theory.lax_monoidal CategoryTheory.LaxMonoidal
 
-attribute [simp] LaxMonoidal.μ_natural
-
-attribute [simp] LaxMonoidal.μ_natural
+/-- An unbundled description of lax monoidal functors. -/
+abbrev LaxMonoidal.ofTensorHom (F : C → D) [Functorial.{v₁, v₂} F]
+    /- unit morphism -/
+    (ε : 𝟙_ D ⟶ F (𝟙_ C))
+    /- tensorator -/
+    (μ : ∀ X Y : C, F X ⊗ F Y ⟶ F (X ⊗ Y))
+    /- naturality -/
+    (μ_natural :
+      ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
+        (map F f ⊗ map F g) ≫ μ Y Y' = μ X X' ≫ map F (f ⊗ g) := by
+    aesop_cat)
+    /- associativity of the tensorator -/
+    (associativity :
+      ∀ X Y Z : C,
+        (μ X Y ⊗ 𝟙 (F Z)) ≫ μ (X ⊗ Y) Z ≫ map F (α_ X Y Z).hom =
+          (α_ (F X) (F Y) (F Z)).hom ≫ (𝟙 (F X) ⊗ μ Y Z) ≫ μ X (Y ⊗ Z) := by
+      aesop_cat)
+    /- left unitality -/
+    (left_unitality : ∀ X : C, (λ_ (F X)).hom = (ε ⊗ 𝟙 (F X)) ≫ μ (𝟙_ C) X ≫ map F (λ_ X).hom := by
+      aesop_cat)
+    /- right unitality -/
+    (right_unitality : ∀ X : C, (ρ_ (F X)).hom = (𝟙 (F X) ⊗ ε) ≫ μ X (𝟙_ C) ≫ map F (ρ_ X).hom := by
+      aesop_cat) :
+      LaxMonoidal.{v₁, v₂} F where
+  ε := ε
+  μ := μ
+  μ_natural_left f X := by intros; simpa using μ_natural f (𝟙 X)
+  μ_natural_right X f := by intros; simpa using μ_natural (𝟙 X) f
+  associativity X Y Z := by intros; simpa using associativity X Y Z
+  left_unitality X := by intros; simpa using left_unitality X
+  right_unitality X := by intros; simpa using right_unitality X
+
+attribute [simp, nolint simpNF] LaxMonoidal.μ_natural_left LaxMonoidal.μ_natural_right
 
 -- The unitality axioms cannot be used as simp lemmas because they require
 -- higher-order matching to figure out the `F` and `X` from `F X`.

Mathlib/CategoryTheory/Monoidal/Limits.lean

@@ -47,24 +47,24 @@ theorem limitFunctorial_map {F G : J ⥤ C} (α : F ⟶ G) :
 variable [MonoidalCategory.{v} C]
 
 @[simps]
-instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where
-  ε :=
+instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F := .ofTensorHom
+  (ε :=
     limit.lift _
       { pt := _
-        π := { app := fun j => 𝟙 _ } }
-  μ F G :=
+        π := { app := fun j => 𝟙 _ } })
+  (μ := fun F G =>
     limit.lift (F ⊗ G)
       { pt := limit F ⊗ limit G
         π :=
           { app := fun j => limit.π F j ⊗ limit.π G j
             naturality := fun j j' f => by
               dsimp
-              simp only [Category.id_comp, ← tensor_comp, limit.w] } }
-  μ_natural f g := by
+              simp only [Category.id_comp, ← tensor_comp, limit.w] } })
+  (μ_natural:= fun f g => by
     ext; dsimp
     simp only [limit.lift_π, Cones.postcompose_obj_π, Monoidal.tensorHom_app, limit.lift_map,
-      NatTrans.comp_app, Category.assoc, ← tensor_comp, limMap_π]
-  associativity X Y Z := by
+      NatTrans.comp_app, Category.assoc, ← tensor_comp, limMap_π])
+  (associativity := fun X Y Z => by
     ext j; dsimp
     simp only [limit.lift_π, Cones.postcompose_obj_π, Monoidal.associator_hom_app, limit.lift_map,
       NatTrans.comp_app, Category.assoc]
@@ -78,8 +78,8 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where
     slice_rhs 2 3 =>
       rw [← id_tensor_comp, limit.lift_π]
       dsimp
-    dsimp; simp
-  left_unitality X := by
+    dsimp; simp)
+  (left_unitality := fun X => by
     ext j; dsimp
     simp only [limit.lift_map, Category.assoc, limit.lift_π, Cones.postcompose_obj_pt,
       Cones.postcompose_obj_π, NatTrans.comp_app, Functor.const_obj_obj, Monoidal.tensorObj_obj,
@@ -90,8 +90,8 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where
       erw [limit.lift_π]
       dsimp
     slice_rhs 2 3 => rw [leftUnitor_naturality]
-    simp
-  right_unitality X := by
+    simp)
+  (right_unitality := fun X => by
     ext j; dsimp
     simp only [limit.lift_map, Category.assoc, limit.lift_π, Cones.postcompose_obj_pt,
       Cones.postcompose_obj_π, NatTrans.comp_app, Functor.const_obj_obj, Monoidal.tensorObj_obj,
@@ -102,7 +102,7 @@ instance limitLaxMonoidal : LaxMonoidal fun F : J ⥤ C => limit F where
       erw [limit.lift_π]
       dsimp
     slice_rhs 2 3 => rw [rightUnitor_naturality]
-    simp
+    simp)
 #align category_theory.limits.limit_lax_monoidal CategoryTheory.Limits.limitLaxMonoidal
 
 /-- The limit functor `F ↦ limit F` bundled as a lax monoidal functor. -/