∀ {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 : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor
        ((CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D).obj x)).inv =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D).map
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).inv)
      (CategoryTheory.CategoryStruct.comp
        {
          app := fun x_1 =>
            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x_1 x
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom,
          naturality := ⋯ }
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          ((CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D).obj x)
          (CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso C D).hom))