-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.mk : {C : Type u} →
  [𝒞 : CategoryTheory.Category.{v, u} C] →
    [toMonoidalCategoryStruct : CategoryTheory.MonoidalCategoryStruct C] →
      autoParam
          (∀ {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
            CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
              CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X₂)
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y₁ g))
          CategoryTheory.MonoidalCategory.tensorHom_def._autoParam →
        autoParam
            (∀ (X₁ X₂ : C),
              CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₁)
                  (CategoryTheory.CategoryStruct.id X₂) =
                CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂))
            CategoryTheory.MonoidalCategory.id_tensorHom_id._autoParam →
          autoParam
              (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
                CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
                    (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) =
                  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
                    (CategoryTheory.CategoryStruct.comp f₂ g₂))
              CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom._autoParam →
            autoParam
                (∀ (X Y : C),
                  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.CategoryStruct.id Y) =
                    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
                CategoryTheory.MonoidalCategory.whiskerLeft_id._autoParam →
              autoParam
                  (∀ (X Y : C),
                    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id X) Y =
                      CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
                  CategoryTheory.MonoidalCategory.id_whiskerRight._autoParam →
                autoParam
                    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
                      CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.tensorHom
                            (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
                          (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom =
                        CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
                          (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁
                            (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃)))
                    CategoryTheory.MonoidalCategory.associator_naturality._autoParam →
                  autoParam
                      (∀ {X Y : C} (f : X ⟶ Y),
                        CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
                              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
                            (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom f)
                      CategoryTheory.MonoidalCategory.leftUnitor_naturality._autoParam →
                    autoParam
                        (∀ {X Y : C} (f : X ⟶ Y),
                          CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerRight f
                                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                              (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
                              f)
                        CategoryTheory.MonoidalCategory.rightUnitor_naturality._autoParam →
                      autoParam
                          (∀ (W X Y Z : C),
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                                  (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom Z)
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.associator W
                                      (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
                                    (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.associator
                                    (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
                                (CategoryTheory.MonoidalCategoryStruct.associator W X
                                    (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom)
                          CategoryTheory.MonoidalCategory.pentagon._autoParam →
                        autoParam
                            (∀ (X Y : C),
                              CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.associator X
                                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).hom
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X
                                    (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) =
                                CategoryTheory.MonoidalCategoryStruct.whiskerRight
                                  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom Y)
                            CategoryTheory.MonoidalCategory.triangle._autoParam →
                          CategoryTheory.MonoidalCategory C