∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting),
  CategoryTheory.CategoryStruct.comp S.g s.s =
    CategoryTheory.CategoryStruct.id S.X₂ - CategoryTheory.CategoryStruct.comp s.r S.f