∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C] (U U' : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj U U') ≪≫
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor
            (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).symm).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) U U').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor U ≪≫
              (CategoryTheory.MonoidalCategoryStruct.rightUnitor U).symm).hom
          U')
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator U (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
              U').hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U
              (CategoryTheory.MonoidalCategoryStruct.leftUnitor U' ≪≫
                  (CategoryTheory.MonoidalCategoryStruct.rightUnitor U').symm).hom)
            (CategoryTheory.MonoidalCategoryStruct.associator U U'
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)))