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