∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : Cᴹᵒᵖ),
  (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator Y.unmop
                { unmop := CategoryTheory.MonoidalCategoryStruct.tensorUnit C }.unmop X.unmop).symm.mop.hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
            (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y.unmop).mop.hom.unmop X.unmop).mop).unmop =
    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y.unmop
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.unmop).mop.hom.unmop).mop.unmop