{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        (r : S.X₂ ⟶ S.X₁) →
          (s : S.X₃ ⟶ S.X₂) →
            autoParam (CategoryTheory.CategoryStruct.comp S.f r = CategoryTheory.CategoryStruct.id S.X₁)
                CategoryTheory.ShortComplex.Splitting.f_r._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃)
                  CategoryTheory.ShortComplex.Splitting.s_g._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp r S.f + CategoryTheory.CategoryStruct.comp S.g s =
                      CategoryTheory.CategoryStruct.id S.X₂)
                    CategoryTheory.ShortComplex.Splitting.id._autoParam →
                  S.Splitting