-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (ε :
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                (μ :
                    (X Y : C) →
                      CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶
                        F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) →
                  autoParam
                      (∀ {X Y : C} (f : X ⟶ Y) (X' : C),
                        CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (μ Y X') =
                          CategoryTheory.CategoryStruct.comp (μ X X')
                            (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X')))
                      CategoryTheory.Functor.LaxMonoidal.μ_natural_left._autoParam →
                    autoParam
                        (∀ {X Y : C} (X' : C) (f : X ⟶ Y),
                          CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (μ X' Y) =
                            CategoryTheory.CategoryStruct.comp (μ X' X)
                              (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f)))
                        CategoryTheory.Functor.LaxMonoidal.μ_natural_right._autoParam →
                      autoParam
                          (∀ (X Y Z : C),
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.whiskerRight (μ X Y) (F.obj Z))
                                (CategoryTheory.CategoryStruct.comp
                                  (μ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
                                  (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ Y Z))
                                  (μ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))))
                          CategoryTheory.Functor.LaxMonoidal.associativity._autoParam →
                        autoParam
                            (∀ (X : C),
                              (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight ε (F.obj X))
                                  (CategoryTheory.CategoryStruct.comp
                                    (μ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
                                    (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)))
                            CategoryTheory.Functor.LaxMonoidal.left_unitality._autoParam →
                          autoParam
                              (∀ (X : C),
                                (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) ε)
                                    (CategoryTheory.CategoryStruct.comp
                                      (μ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                      (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)))
                              CategoryTheory.Functor.LaxMonoidal.right_unitality._autoParam →
                            F.LaxMonoidal