-- Mathlib.CategoryTheory.Monoidal.Functor
/-- A constructor for lax monoidal functors whose axioms are described by `tensorHom` instead of
`whiskerLeft` and `whiskerRight`.
 -/
CategoryTheory.Functor.LaxMonoidal.ofTensorHom : {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 X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
                        CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (μ Y Y') =
                          CategoryTheory.CategoryStruct.comp (μ X X')
                            (F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)))
                      _auto_46✝ →
                    autoParam
                        (∀ (X Y Z : C),
                          CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.tensorHom (μ X Y)
                                (CategoryTheory.CategoryStruct.id (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.tensorHom
                                  (CategoryTheory.CategoryStruct.id (F.obj X)) (μ Y Z))
                                (μ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))))
                        _auto_48✝ →
                      autoParam
                          (∀ (X : C),
                            (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.tensorHom ε
                                  (CategoryTheory.CategoryStruct.id (F.obj X)))
                                (CategoryTheory.CategoryStruct.comp
                                  (μ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
                                  (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)))
                          _auto_50✝ →
                        autoParam
                            (∀ (X : C),
                              (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.tensorHom
                                    (CategoryTheory.CategoryStruct.id (F.obj X)) ε)
                                  (CategoryTheory.CategoryStruct.comp
                                    (μ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                    (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)))
                            _auto_52✝ →
                          F.LaxMonoidal