-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.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) →
                            F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d) ⟶
                              CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d)) →
                      autoParam
                          (∀ {c c' : C} (f : c ⟶ c') (d : D),
                            CategoryTheory.CategoryStruct.comp
                                (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d))
                                (δₗ c' d) =
                              CategoryTheory.CategoryStruct.comp (δₗ c d)
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f (F.obj d)))
                          CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_left._autoParam →
                        autoParam
                            (∀ (c : C) {d d' : D} (f : d ⟶ d'),
                              CategoryTheory.CategoryStruct.comp
                                  (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f))
                                  (δₗ c d') =
                                CategoryTheory.CategoryStruct.comp (δₗ c d)
                                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f)))
                            CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_right._autoParam →
                          autoParam
                              (∀ (c c' : C) (d : D),
                                CategoryTheory.CategoryStruct.comp
                                    (δₗ (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d)
                                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c'
                                        (F.obj d)).hom =
                                  CategoryTheory.CategoryStruct.comp
                                    (F.map
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c'
                                          d).hom)
                                    (CategoryTheory.CategoryStruct.comp
                                      (δₗ c (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d))
                                      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
                                        (δₗ c' d))))
                              CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity._autoParam →
                            autoParam
                                (∀ (d : D),
                                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso
                                        (F.obj d)).inv =
                                    CategoryTheory.CategoryStruct.comp
                                      (F.map
                                        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).inv)
                                      (δₗ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d))
                                CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv._autoParam →
                              F.OplaxLeftLinear C