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