∀ (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.MonoidalLeftAction C D] (X Y : C),
  CategoryTheory.CategoryStruct.comp
      (Quiver.Hom.mop
        { app := fun x => (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso X Y x).hom,
          naturality := ⋯ })
      (Quiver.Hom.mop
        { app := fun x => (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso X Y x).inv,
          naturality := ⋯ }) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop C D).obj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))