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