-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.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.MonoidalRightAction C D] →
                  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] →
                    (μᵣ :
                        (d : D) →
                          (c : C) →
                            CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c ⟶
                              F.obj (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)) →
                      autoParam
                          (∀ (d : D) {c c' : C} (f : c ⟶ c'),
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f)
                                (μᵣ d c') =
                              CategoryTheory.CategoryStruct.comp (μᵣ d c)
                                (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f)))
                          CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_right._autoParam →
                        autoParam
                            (∀ {d d' : D} (f : d ⟶ d') (c : C),
                              CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c)
                                  (μᵣ d' c) =
                                CategoryTheory.CategoryStruct.comp (μᵣ d c)
                                  (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)))
                            CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_left._autoParam →
                          autoParam
                              (∀ (d : D) (c c' : C),
                                CategoryTheory.CategoryStruct.comp
                                    (μᵣ d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c'))
                                    (F.map
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c
                                          c').hom) =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d)
                                        c c').hom
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (μᵣ d c)
                                        c')
                                      (μᵣ (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)
                                        c')))
                              CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity._autoParam →
                            autoParam
                                (∀ (d : D),
                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                        (F.obj d)).hom =
                                    CategoryTheory.CategoryStruct.comp
                                      (μᵣ d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                      (F.map
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                            d).hom))
                                CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality._autoParam →
                              F.LaxRightLinear C