∀ {I : Type u_4} {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C]
  {X Y : CategoryTheory.GradedObject I C} (e : X ≅ Y) (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap e.inv p)
      (CategoryTheory.GradedObject.mapMap e.hom p) =
    CategoryTheory.CategoryStruct.id (Y.mapObj p)