-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.mk : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        {F : CategoryTheory.Functor D D'} →
          {C : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
                  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] →
                    (μₗ :
                        (c : C) →
                          (d : D) →
                            CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d) ⟶
                              F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)) →
                      autoParam
                          (∀ {c c' : C} (f : c ⟶ c') (d : D),
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d))
                                (μₗ c' d) =
                              CategoryTheory.CategoryStruct.comp (μₗ c d)
                                (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d)))
                          CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left._autoParam →
                        autoParam
                            (∀ (c : C) {d d' : D} (f : d ⟶ d'),
                              CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f))
                                  (μₗ c d') =
                                CategoryTheory.CategoryStruct.comp (μₗ c d)
                                  (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f)))
                            CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right._autoParam →
                          autoParam
                              (∀ (c c' : C) (d : D),
                                CategoryTheory.CategoryStruct.comp
                                    (μₗ (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d)
                                    (F.map
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c'
                                          d).hom) =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c'
                                        (F.obj d)).hom
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
                                        (μₗ c' d))
                                      (μₗ c (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d))))
                              CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity._autoParam →
                            autoParam
                                (∀ (d : D),
                                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso
                                        (F.obj d)).hom =
                                    CategoryTheory.CategoryStruct.comp
                                      (μₗ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d)
                                      (F.map
                                        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom))
                                CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality._autoParam →
                              F.LaxLeftLinear C