∀ {C : Type u_4} {D : Type u_1} [inst : CategoryTheory.Category.{u_3, u_4} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{u_2, u_1} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (X Y : C),
  CategoryTheory.CategoryStruct.comp
      { app := fun x => (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x X Y).inv,
        naturality := ⋯ }
      { app := fun x => (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x X Y).hom,
        naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj
        ((CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D).obj X)
        ((CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D).obj Y))