∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (h : CategoryTheory.ShiftMkCore C A) (n : A) (X : C),
  (h.add n 0).inv.app X = CategoryTheory.CategoryStruct.comp (h.zero.hom.app ((h.F n).obj X)) (CategoryTheory.eqToHom ⋯)