∀ {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]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : D} [inst_5 : CategoryTheory.ModObj A M]
  [inst_6 : CategoryTheory.ModObj A N] (f : M ⟶ N)
  (smul_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
          CategoryTheory.ModObj.smul)
      CategoryTheory.Mod_.Hom.mk''._auto_1),
  (CategoryTheory.Mod_.Hom.mk'' f smul_hom).hom = f