refactor(CategoryTheory/Monoidal): make ofTensorHom the default constructor

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -197,24 +197,24 @@ end MonoidalCategory
 
 open MonoidalCategory
 
-instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) := MonoidalCategory.ofTensorHom
+instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) where
   -- data
-  (tensorObj := MonoidalCategory.tensorObj)
-  (tensorHom := @tensorHom _ _)
-  (whiskerLeft := @whiskerLeft _ _)
-  (whiskerRight := @whiskerRight _ _)
-  (tensorUnit' := ModuleCat.of R R)
-  (associator := associator)
-  (leftUnitor := leftUnitor)
-  (rightUnitor := rightUnitor)
+  tensorObj := MonoidalCategory.tensorObj
+  tensorHom := @tensorHom _ _
+  whiskerLeft := @whiskerLeft _ _
+  whiskerRight := @whiskerRight _ _
+  tensorUnit' := ModuleCat.of R R
+  associator := associator
+  leftUnitor := leftUnitor
+  rightUnitor := rightUnitor
   -- properties
-  (tensor_id := fun M N ↦ tensor_id M N)
-  (tensor_comp := fun f g h ↦ MonoidalCategory.tensor_comp f g h)
-  (associator_naturality := fun f g h ↦ MonoidalCategory.associator_naturality f g h)
-  (leftUnitor_naturality := fun f ↦ MonoidalCategory.leftUnitor_naturality f)
-  (rightUnitor_naturality := fun f ↦ rightUnitor_naturality f)
-  (pentagon := fun M N K L ↦ pentagon M N K L)
-  (triangle := fun M N ↦ triangle M N)
+  tensor_id := fun M N ↦ tensor_id M N
+  tensor_comp := fun f g h ↦ MonoidalCategory.tensor_comp f g h
+  associator_naturality := fun f g h ↦ MonoidalCategory.associator_naturality f g h
+  leftUnitor_naturality := fun f ↦ MonoidalCategory.leftUnitor_naturality f
+  rightUnitor_naturality := fun f ↦ rightUnitor_naturality f
+  pentagon := fun M N K L ↦ pentagon M N K L
+  triangle := fun M N ↦ triangle M N
 #align Module.monoidal_category ModuleCat.monoidalCategory
 
 /-- Remind ourselves that the monoidal unit, being just `R`, is still a commutative ring. -/

Mathlib/CategoryTheory/Bicategory/End.lean

@@ -41,6 +41,7 @@ instance (X : C) : MonoidalCategory (EndMonoidal X) where
   tensorObj f g := f ≫ g
   whiskerLeft {f g h} η := f ◁ η
   whiskerRight {f g} η h := η ▷ h
+  tensorHom {X₁ Y₁ X₂ Y₂} f g := (f ▷ X₂) ≫ (Y₁ ◁ g)
   tensorUnit' := 𝟙 _
   associator f g h := α_ f g h
   leftUnitor f := λ_ f

Mathlib/CategoryTheory/Monoidal/Category.lean

@@ -33,11 +33,7 @@ These are products of an object and a morphism (the terminology "whiskering"
 is borrowed from 2-category theory). The tensor product of morphisms `tensorHom` can be defined
 in terms of the whiskerings. There are two possible such definitions, which are related by
 the exchange property of the whiskerings. These two definitions are accessed by `tensorHom_def`
-and `tensorHom_def'`. By default, `tensorHom` is defined so that `tensorHom_def` holds
-definitionally.
-
-If you want to provide `tensorHom` and define `whiskerLeft` and `whiskerRight` in terms of it,
-you can use the alternative constructor `CategoryTheory.MonoidalCategory.ofTensorHom`.
+and `tensorHom_def'`.
 
 The whiskerings are useful when considering simp-normal forms of morphisms in monoidal categories.
 
@@ -73,16 +69,21 @@ See <https://stacks.math.columbia.edu/tag/0FFK>.
 class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] where
   /-- curried tensor product of objects -/
   tensorObj : C → C → C
+  /-- Tensor product of identity maps is the identity: `(𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)` -/
+  tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)
   /-- left whiskering for morphisms -/
-  whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂
+  -- By default, it is defined in terms of tensorHom.
+  whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂ :=
+    tensorHom (𝟙 X) f
+  whiskerLeft_def (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂)  :
+    whiskerLeft X f = tensorHom (𝟙 X) f := by
+      aesop_cat
   /-- right whiskering for morphisms -/
-  whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y
-  /-- Tensor product of identity maps is the identity: `(𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)` -/
-  -- By default, it is defined in terms of whiskerings.
-  tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g: X₂ ⟶ Y₂) : (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂) :=
-    whiskerRight f X₂ ≫ whiskerLeft Y₁ g
-  tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g: X₂ ⟶ Y₂) :
-    tensorHom f g = whiskerRight f X₂ ≫ whiskerLeft Y₁ g := by
+  -- By default, it is defined in terms of tensorHom.
+  whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y :=
+    tensorHom f (𝟙 Y)
+  whiskerRight_def {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C)  :
+    whiskerRight f Y = tensorHom f (𝟙 Y) := by
       aesop_cat
   /-- Tensor product of identity maps is the identity: `(𝟙 X₁ ⊗ 𝟙 X₂) = 𝟙 (X₁ ⊗ X₂)` -/
   tensor_id : ∀ X₁ X₂ : C, tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂) := by aesop_cat
@@ -100,10 +101,6 @@ class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] where
   tensorUnit' : C
   /-- The associator isomorphism `(X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)` -/
   associator : ∀ X Y Z : C, tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
-  whiskerLeft_id : ∀ (X Y : C), whiskerLeft X (𝟙 Y) = 𝟙 (tensorObj X Y) := by
-    aesop_cat
-  id_whiskerRight : ∀ (X Y : C), whiskerRight (𝟙 X) Y = 𝟙 (tensorObj X Y) := by
-    aesop_cat
   /-- Naturality of the associator isomorphism: `(f₁ ⊗ f₂) ⊗ f₃ ≃ f₁ ⊗ (f₂ ⊗ f₃)` -/
   associator_naturality :
     ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
@@ -147,9 +144,6 @@ class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] where
     aesop_cat
 #align category_theory.monoidal_category CategoryTheory.MonoidalCategory
 
-attribute [reassoc] MonoidalCategory.tensorHom_def
-attribute [reassoc, simp] MonoidalCategory.whiskerLeft_id
-attribute [reassoc, simp] MonoidalCategory.id_whiskerRight
 attribute [simp] MonoidalCategory.tensor_id
 attribute [reassoc] MonoidalCategory.tensor_comp
 attribute [simp] MonoidalCategory.tensor_comp
@@ -194,6 +188,17 @@ scoped notation "ρ_" => rightUnitor
 
 variable {C : Type u} [𝒞 : Category.{v} C] [MonoidalCategory C]
 
+@[reassoc]
+theorem tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g: X₂ ⟶ Y₂) :
+    f ⊗ g = (f ▷ X₂) ≫ (Y₁ ◁ g) := by
+  rw [whiskerRight_def, whiskerLeft_def, ←tensor_comp, comp_id, id_comp]
+
+@[reassoc, simp]
+theorem whiskerLeft_id (X Y : C) : X ◁ 𝟙 Y = 𝟙 (X ⊗ Y) := by rw [whiskerLeft_def, tensor_id]
+
+@[reassoc, simp]
+theorem id_whiskerRight (X Y : C) : 𝟙 X ▷ Y = 𝟙 (X ⊗ Y) := by rw [whiskerRight_def, tensor_id]
+
 theorem id_tensorHom (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) :
     (𝟙 X) ⊗ f = X ◁ f := by
   simp [tensorHom_def]
@@ -437,70 +442,6 @@ theorem tensor_inv_hom_id' {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y)
   rw [← tensor_comp, IsIso.inv_hom_id, comp_tensor_id]
 #align category_theory.monoidal_category.tensor_inv_hom_id' CategoryTheory.MonoidalCategory.tensor_inv_hom_id'
 
-/--
-A constructor for monoidal categories that requires `tensorHom` instead of `whiskerLeft` and
-`whiskerRight`.
--/
-def ofTensorHom
-    (tensorObj : C → C → C)
-    (tensorHom : ∀ {X₁ Y₁ X₂ Y₂ : C}, (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂))
-    (whiskerLeft : ∀ (X : C) {Y₁ Y₂ : C}  (_f : Y₁ ⟶ Y₂), tensorObj X Y₁ ⟶ tensorObj X Y₂ :=
-      fun X _ _ f ↦ tensorHom (𝟙 X) f)
-    (whiskerRight : ∀ {X₁ X₂ : C} (_f : X₁ ⟶ X₂) (Y : C), tensorObj X₁ Y ⟶ tensorObj X₂ Y :=
-      fun f Y ↦ tensorHom f (𝟙 Y))
-    (tensor_id : ∀ X₁ X₂ : C, tensorHom (𝟙 X₁) (𝟙 X₂) = 𝟙 (tensorObj X₁ X₂) := by
-      aesop_cat)
-    (id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂), tensorHom (𝟙 X) f = whiskerLeft X f := by
-      aesop_cat)
-    (tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C), tensorHom f (𝟙 Y) = whiskerRight f Y := by
-      aesop_cat)
-    (tensor_comp :
-      ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
-        tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂ := by
-          aesop_cat)
-    (tensorUnit' : C)
-    (associator : ∀ X Y Z : C, tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z))
-    (associator_naturality :
-      ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
-        tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
-          (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) := by
-            aesop_cat)
-    (leftUnitor : ∀ X : C, tensorObj tensorUnit' X ≅ X)
-    (leftUnitor_naturality :
-      ∀ {X Y : C} (f : X ⟶ Y),
-        tensorHom (𝟙 tensorUnit') f ≫ (leftUnitor Y).hom = (leftUnitor X).hom ≫ f := by
-          aesop_cat)
-    (rightUnitor : ∀ X : C, tensorObj X tensorUnit' ≅ X)
-    (rightUnitor_naturality :
-      ∀ {X Y : C} (f : X ⟶ Y),
-        tensorHom f (𝟙 tensorUnit') ≫ (rightUnitor Y).hom = (rightUnitor X).hom ≫ f := by
-          aesop_cat)
-    (pentagon :
-      ∀ W X Y Z : C,
-        tensorHom (associator W X Y).hom (𝟙 Z) ≫
-            (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
-          (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom := by
-            aesop_cat)
-    (triangle :
-      ∀ X Y : C,
-        (associator X tensorUnit' Y).hom ≫ tensorHom (𝟙 X) (leftUnitor Y).hom =
-          tensorHom (rightUnitor X).hom (𝟙 Y) := by
-            aesop_cat) :
-      MonoidalCategory C where
-  tensorObj := tensorObj
-  tensorHom := tensorHom
-  whiskerLeft X _ _ f := whiskerLeft X f
-  whiskerRight f X := whiskerRight f X
-  tensorHom_def := by intros; simp [← id_tensorHom, ←tensorHom_id, ← tensor_comp]
-  tensorUnit' := tensorUnit'
-  leftUnitor := leftUnitor
-  rightUnitor := rightUnitor
-  associator := associator
-  whiskerLeft_id := by intros; simp [← id_tensorHom, ← tensor_id]
-  id_whiskerRight := by intros; simp [← tensorHom_id, tensor_id]
-  pentagon := by intros; simp [← id_tensorHom, ← tensorHom_id, pentagon]
-  triangle := by intros; simp [← id_tensorHom, ← tensorHom_id, triangle]
-
 end
 
 section
@@ -719,8 +660,9 @@ instance prodMonoidal : MonoidalCategory (C₁ × C₂) where
   tensorObj X Y := (X.1 ⊗ Y.1, X.2 ⊗ Y.2)
   tensorHom f g := (f.1 ⊗ g.1, f.2 ⊗ g.2)
   whiskerLeft X _ _ f := (whiskerLeft X.1 f.1, whiskerLeft X.2 f.2)
+  whiskerLeft_def := by simp [whiskerLeft_def]
   whiskerRight f X := (whiskerRight f.1 X.1, whiskerRight f.2 X.2)
-  tensorHom_def := by simp [tensorHom_def]
+  whiskerRight_def := by simp [whiskerRight_def]
   tensorUnit' := (𝟙_ C₁, 𝟙_ C₂)
   associator X Y Z := (α_ X.1 Y.1 Z.1).prod (α_ X.2 Y.2 Z.2)
   leftUnitor := fun ⟨X₁, X₂⟩ => (λ_ X₁).prod (λ_ X₂)

Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

@@ -159,28 +159,6 @@ instance : MonoidalCategory (F C) where
     Quotient.map₂ Hom.tensor <| by
       intro _ _ h _ _ h'
       exact HomEquiv.tensor h h'
-  whiskerLeft := fun X _ _ f =>
-    Quotient.map (fun f' => Hom.tensor (Hom.id X) f')
-      (fun _ _ h => HomEquiv.tensor (HomEquiv.refl (Hom.id X)) h) f
-  whiskerRight := fun f Y =>
-    Quotient.map (fun f' => Hom.tensor f' (Hom.id Y))
-      (fun _ _ h => HomEquiv.tensor h (HomEquiv.refl (Hom.id Y))) f
-  tensorHom_def := by
-    rintro W X Y Z ⟨f⟩ ⟨g⟩
-    apply Quotient.sound
-    calc Hom.tensor f g
-      _ ≈ Hom.tensor (Hom.comp f (Hom.id X)) (Hom.comp (Hom.id Y) g) := by
-        apply HomEquiv.tensor (HomEquiv.comp_id f).symm (HomEquiv.id_comp g).symm
-      _ ≈ Hom.comp (Hom.tensor f (Hom.id Y)) (Hom.tensor (Hom.id X) g) := by
-        apply HomEquiv.tensor_comp
-  whiskerLeft_id := by
-    rintro X Y
-    apply Quotient.sound
-    apply HomEquiv.tensor_id
-  id_whiskerRight := by
-    intro X Y
-    apply Quotient.sound
-    apply HomEquiv.tensor_id
   tensor_id X Y := Quotient.sound tensor_id
   tensor_comp := @fun X₁ Y₁ Z₁ X₂ Y₂ Z₂ => by
     rintro ⟨f₁⟩ ⟨f₂⟩ ⟨g₁⟩ ⟨g₂⟩

Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

@@ -85,8 +85,9 @@ instance functorCategoryMonoidal : MonoidalCategory (C ⥤ D) where
   tensorObj F G := tensorObj F G
   tensorHom α β := tensorHom α β
   whiskerLeft F _ _ α := FunctorCategory.whiskerLeft F α
+  whiskerLeft_def F _ _ α := by ext; simp [whiskerLeft_def]
   whiskerRight α F := FunctorCategory.whiskerRight α F
-  tensorHom_def := by intros; ext; simp [tensorHom_def]
+  whiskerRight_def α F := by ext; simp [whiskerRight_def]
   tensorUnit' := (CategoryTheory.Functor.const C).obj (𝟙_ D)
   leftUnitor F := NatIso.ofComponents fun X => λ_ (F.obj X)
   rightUnitor F := NatIso.ofComponents fun X => ρ_ (F.obj X)

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -475,15 +475,15 @@ theorem mul_rightUnitor {M : Mon_ C} :
   simp only [Category.assoc, Category.id_comp]
 #align Mon_.mul_right_unitor Mon_.mul_rightUnitor
 
-instance monMonoidal : MonoidalCategory (Mon_ C) := .ofTensorHom
-  (tensorObj := fun M N ↦
+instance monMonoidal : MonoidalCategory (Mon_ C) where
+  tensorObj := fun M N ↦
     { X := M.X ⊗ N.X
       one := (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)
       mul := tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)
       one_mul := Mon_tensor_one_mul M N
       mul_one := Mon_tensor_mul_one M N
-      mul_assoc := Mon_tensor_mul_assoc M N })
-  (tensorHom := fun f g ↦
+      mul_assoc := Mon_tensor_mul_assoc M N }
+  tensorHom := fun f g ↦
     { hom := f.hom ⊗ g.hom
       one_hom := by
         dsimp
@@ -492,18 +492,18 @@ instance monMonoidal : MonoidalCategory (Mon_ C) := .ofTensorHom
         dsimp
         slice_rhs 1 2 => rw [tensor_μ_natural]
         slice_lhs 2 3 => rw [← tensor_comp, Hom.mul_hom f, Hom.mul_hom g, tensor_comp]
-        simp only [Category.assoc] })
-  (tensor_id := by intros; ext; apply tensor_id)
-  (tensor_comp := by intros; ext; apply tensor_comp)
-  (tensorUnit' := trivial C)
-  (associator := fun M N P ↦ isoOfIso (α_ M.X N.X P.X) one_associator mul_associator)
-  (associator_naturality := by intros; ext; dsimp; apply associator_naturality)
-  (leftUnitor := fun M ↦ isoOfIso (λ_ M.X) one_leftUnitor mul_leftUnitor)
-  (leftUnitor_naturality := by intros; ext; dsimp; apply leftUnitor_naturality)
-  (rightUnitor := fun M ↦ isoOfIso (ρ_ M.X) one_rightUnitor mul_rightUnitor)
-  (rightUnitor_naturality := by intros; ext; dsimp; apply rightUnitor_naturality)
-  (pentagon := by intros; ext; dsimp; apply pentagon)
-  (triangle := by intros; ext; dsimp; apply triangle)
+        simp only [Category.assoc] }
+  tensor_id := by intros; ext; apply tensor_id
+  tensor_comp := by intros; ext; apply tensor_comp
+  tensorUnit' := trivial C
+  associator := fun M N P ↦ isoOfIso (α_ M.X N.X P.X) one_associator mul_associator
+  associator_naturality := by intros; ext; dsimp; apply associator_naturality
+  leftUnitor := fun M ↦ isoOfIso (λ_ M.X) one_leftUnitor mul_leftUnitor
+  leftUnitor_naturality := by intros; ext; dsimp; apply leftUnitor_naturality
+  rightUnitor := fun M ↦ isoOfIso (ρ_ M.X) one_rightUnitor mul_rightUnitor
+  rightUnitor_naturality := by intros; ext; dsimp; apply rightUnitor_naturality
+  pentagon := by intros; ext; dsimp; apply pentagon
+  triangle := by intros; ext; dsimp; apply triangle
 #align Mon_.Mon_monoidal Mon_.monMonoidal
 
 end Mon_

Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean

@@ -331,20 +331,20 @@ end MonoidalOfChosenFiniteProducts
 open MonoidalOfChosenFiniteProducts
 
 /-- A category with a terminal object and binary products has a natural monoidal structure. -/
-def monoidalOfChosenFiniteProducts : MonoidalCategory C := .ofTensorHom
-  (tensorUnit' := 𝒯.cone.pt)
-  (tensorObj := tensorObj ℬ)
-  (tensorHom := tensorHom ℬ)
-  (tensor_id := tensor_id ℬ)
-  (tensor_comp := tensor_comp ℬ)
-  (associator := BinaryFan.associatorOfLimitCone ℬ)
-  (leftUnitor := fun X ↦ BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X).isLimit)
-  (rightUnitor := fun X ↦ BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit)
-  (pentagon := pentagon ℬ)
-  (triangle := triangle 𝒯 ℬ)
-  (leftUnitor_naturality := leftUnitor_naturality 𝒯 ℬ)
-  (rightUnitor_naturality := rightUnitor_naturality 𝒯 ℬ)
-  (associator_naturality := associator_naturality ℬ)
+def monoidalOfChosenFiniteProducts : MonoidalCategory C where
+  tensorUnit' := 𝒯.cone.pt
+  tensorObj := tensorObj ℬ
+  tensorHom := tensorHom ℬ
+  tensor_id := tensor_id ℬ
+  tensor_comp := tensor_comp ℬ
+  associator := BinaryFan.associatorOfLimitCone ℬ
+  leftUnitor := fun X ↦ BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X).isLimit
+  rightUnitor := fun X ↦ BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit
+  pentagon := pentagon ℬ
+  triangle := triangle 𝒯 ℬ
+  leftUnitor_naturality := leftUnitor_naturality 𝒯 ℬ
+  rightUnitor_naturality := rightUnitor_naturality 𝒯 ℬ
+  associator_naturality := associator_naturality ℬ
 #align category_theory.monoidal_of_chosen_finite_products CategoryTheory.monoidalOfChosenFiniteProducts
 
 namespace MonoidalOfChosenFiniteProducts

Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

@@ -45,17 +45,16 @@ open CategoryTheory.Limits
 section
 
 /-- A category with a terminal object and binary products has a natural monoidal structure. -/
-def monoidalOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : MonoidalCategory C :=
-  .ofTensorHom
-    (tensorUnit' := ⊤_ C)
-    (tensorObj := fun X Y ↦ X ⨯ Y)
-    (tensorHom := fun f g ↦ Limits.prod.map f g)
-    (associator := prod.associator)
-    (leftUnitor := fun P ↦ prod.leftUnitor P)
-    (rightUnitor := fun P ↦ prod.rightUnitor P)
-    (pentagon := prod.pentagon)
-    (triangle := prod.triangle)
-    (associator_naturality := @prod.associator_naturality _ _ _)
+def monoidalOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : MonoidalCategory C where
+  tensorUnit' := ⊤_ C
+  tensorObj := fun X Y ↦ X ⨯ Y
+  tensorHom := fun f g ↦ Limits.prod.map f g
+  associator := prod.associator
+  leftUnitor := fun P ↦ prod.leftUnitor P
+  rightUnitor := fun P ↦ prod.rightUnitor P
+  pentagon := prod.pentagon
+  triangle := prod.triangle
+  associator_naturality := @prod.associator_naturality _ _ _
 #align category_theory.monoidal_of_has_finite_products CategoryTheory.monoidalOfHasFiniteProducts
 
 end
@@ -137,17 +136,16 @@ end
 section
 
 /-- A category with an initial object and binary coproducts has a natural monoidal structure. -/
-def monoidalOfHasFiniteCoproducts [HasInitial C] [HasBinaryCoproducts C] : MonoidalCategory C :=
-  .ofTensorHom
-    (tensorUnit' := ⊥_ C)
-    (tensorObj := fun X Y ↦ X ⨿ Y)
-    (tensorHom := fun f g ↦ Limits.coprod.map f g)
-    (associator := coprod.associator)
-    (leftUnitor := coprod.leftUnitor)
-    (rightUnitor := coprod.rightUnitor)
-    (pentagon := coprod.pentagon)
-    (triangle := coprod.triangle)
-    (associator_naturality := @coprod.associator_naturality _ _ _)
+def monoidalOfHasFiniteCoproducts [HasInitial C] [HasBinaryCoproducts C] : MonoidalCategory C where
+  tensorUnit' := ⊥_ C
+  tensorObj := fun X Y ↦ X ⨿ Y
+  tensorHom := fun f g ↦ Limits.coprod.map f g
+  associator := coprod.associator
+  leftUnitor := coprod.leftUnitor
+  rightUnitor := coprod.rightUnitor
+  pentagon := coprod.pentagon
+  triangle := coprod.triangle
+  associator_naturality := @coprod.associator_naturality _ _ _
 #align category_theory.monoidal_of_has_finite_coproducts CategoryTheory.monoidalOfHasFiniteCoproducts
 
 end