∀ {X Y : Type u_1} [inst : Monoid X] [inst_1 : Monoid Y] (e : X ≃* Y),
  CategoryTheory.CategoryStruct.comp (MonCat.ofHom e.symm.toMonoidHom) (MonCat.ofHom e.toMonoidHom) =
    CategoryTheory.CategoryStruct.id (MonCat.of Y)