{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (actionObj : C → D → D) →
            (actionHomLeft : {c c' : C} → (c ⟶ c') → (d : D) → actionObj c d ⟶ actionObj c' d) →
              (actionHomRight : (c : C) → {d d' : D} → (d ⟶ d') → (actionObj c d ⟶ actionObj c d')) →
                (actionHom : {c c' : C} → {d d' : D} → (c ⟶ c') → (d ⟶ d') → (actionObj c d ⟶ actionObj c' d')) →
                  (actionAssocIso :
                      (c c' : C) →
                        (d : D) →
                          actionObj (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d ≅
                            actionObj c (actionObj c' d)) →
                    (actionUnitIso : (d : D) → actionObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d ≅ d) →
                      autoParam
                          (∀ {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d'),
                            actionHom f g =
                              CategoryTheory.CategoryStruct.comp (actionHomLeft f d) (actionHomRight c' g))
                          CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def._autoParam →
                        autoParam
                            (∀ (c : C) (d : D),
                              actionHomRight c (CategoryTheory.CategoryStruct.id d) =
                                CategoryTheory.CategoryStruct.id (actionObj c d))
                            CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id._autoParam →
                          autoParam
                              (∀ (c : C) (d : D),
                                actionHomLeft (CategoryTheory.CategoryStruct.id c) d =
                                  CategoryTheory.CategoryStruct.id (actionObj c d))
                              CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft._autoParam →
                            autoParam
                                (∀ {c c' c'' : C} {d d' d'' : D} (f₁ : c ⟶ c') (f₂ : c' ⟶ c'') (g₁ : d ⟶ d')
                                  (g₂ : d' ⟶ d''),
                                  actionHom (CategoryTheory.CategoryStruct.comp f₁ f₂)
                                      (CategoryTheory.CategoryStruct.comp g₁ g₂) =
                                    CategoryTheory.CategoryStruct.comp (actionHom f₁ g₁) (actionHom f₂ g₂))
                                CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp._autoParam →
                              autoParam
                                  (∀ {c₁ c₂ c₃ c₄ : C} {d₁ d₂ : D} (f : c₁ ⟶ c₂) (g : c₃ ⟶ c₄) (h : d₁ ⟶ d₂),
                                    CategoryTheory.CategoryStruct.comp
                                        (actionHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
                                        (actionAssocIso c₂ c₄ d₂).hom =
                                      CategoryTheory.CategoryStruct.comp (actionAssocIso c₁ c₃ d₁).hom
                                        (actionHom f (actionHom g h)))
                                  CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality._autoParam →
                                autoParam
                                    (∀ {d d' : D} (f : d ⟶ d'),
                                      CategoryTheory.CategoryStruct.comp (actionUnitIso d).hom f =
                                        CategoryTheory.CategoryStruct.comp
                                          (actionHomRight (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
                                          (actionUnitIso d').hom)
                                    CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality._autoParam →
                                  autoParam
                                      (∀ (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D),
                                        actionHomLeft (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c f) d =
                                          CategoryTheory.CategoryStruct.comp (actionAssocIso c c' d).hom
                                            (CategoryTheory.CategoryStruct.comp (actionHomRight c (actionHomLeft f d))
                                              (actionAssocIso c c'' d).inv))
                                      CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft._autoParam →
                                    autoParam
                                        (∀ {c c' : C} (c'' : C) (f : c ⟶ c') (d : D),
                                          actionHomLeft (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c'') d =
                                            CategoryTheory.CategoryStruct.comp (actionAssocIso c c'' d).hom
                                              (CategoryTheory.CategoryStruct.comp (actionHomLeft f (actionObj c'' d))
                                                (actionAssocIso c' c'' d).inv))
                                        CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerRight_actionHomLeft._autoParam →
                                      autoParam
                                          (∀ (c₁ c₂ c₃ : C) (d : D),
                                            CategoryTheory.CategoryStruct.comp
                                                (actionHomLeft
                                                  (CategoryTheory.MonoidalCategoryStruct.associator c₁ c₂ c₃).hom d)
                                                (CategoryTheory.CategoryStruct.comp
                                                  (actionAssocIso c₁
                                                      (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₃) d).hom
                                                  (actionHomRight c₁ (actionAssocIso c₂ c₃ d).hom)) =
                                              CategoryTheory.CategoryStruct.comp
                                                (actionAssocIso (CategoryTheory.MonoidalCategoryStruct.tensorObj c₁ c₂)
                                                    c₃ d).hom
                                                (actionAssocIso c₁ c₂ (actionObj c₃ d)).hom)
                                          CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom._autoParam →
                                        autoParam
                                            (∀ (c : C) (d : D),
                                              actionHomLeft (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom d =
                                                CategoryTheory.CategoryStruct.comp
                                                  (actionAssocIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) c
                                                      d).hom
                                                  (actionUnitIso (actionObj c d)).hom)
                                            CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom._autoParam →
                                          autoParam
                                              (∀ (c : C) (d : D),
                                                actionHomLeft (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom
                                                    d =
                                                  CategoryTheory.CategoryStruct.comp
                                                    (actionAssocIso c
                                                        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d).hom
                                                    (actionHomRight c (actionUnitIso d).hom))
                                              CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom._autoParam →
                                            CategoryTheory.MonoidalCategory.MonoidalLeftAction C D