{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {M : C} →
              [inst_4 : CategoryTheory.MonObj M] →
                {X : D} →
                  {motive : CategoryTheory.ModObj M X → Sort u} →
                    ((smul : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj M X ⟶ X) →
                        (one_smul' :
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                                  CategoryTheory.MonObj.one X)
                                smul =
                              (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom) →
                          (mul_smul' :
                              CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                                    CategoryTheory.MonObj.mul X)
                                  smul =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul)
                                    smul)) →
                            motive { smul := smul, one_smul' := one_smul', mul_smul' := mul_smul' }) →
                      (t : CategoryTheory.ModObj M X) → motive t