∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) {Z : C}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j Y).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).hom
      (CategoryTheory.CategoryStruct.comp f h)