∀ {X Y : Type u_1} [inst : Add X] [inst_1 : Add Y] (e : X ≃+ Y),
  CategoryTheory.CategoryStruct.comp (AddMagmaCat.ofHom e.symm.toAddHom) (AddMagmaCat.ofHom e.toAddHom) =
    CategoryTheory.CategoryStruct.id (AddMagmaCat.of Y)