∀ {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₂)
  (f_r :
    autoParam (CategoryTheory.CategoryStruct.comp S.f r = CategoryTheory.CategoryStruct.id S.X₁)
      CategoryTheory.ShortComplex.Splitting.f_r._autoParam)
  (s_g :
    autoParam (CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃)
      CategoryTheory.ShortComplex.Splitting.s_g._autoParam)
  (id :
    autoParam
      (CategoryTheory.CategoryStruct.comp r S.f + CategoryTheory.CategoryStruct.comp S.g s =
        CategoryTheory.CategoryStruct.id S.X₂)
      CategoryTheory.ShortComplex.Splitting.id._autoParam)
  (r_1 : S.X₂ ⟶ S.X₁) (s_1 : S.X₃ ⟶ S.X₂)
  (f_r_1 :
    autoParam (CategoryTheory.CategoryStruct.comp S.f r_1 = CategoryTheory.CategoryStruct.id S.X₁)
      CategoryTheory.ShortComplex.Splitting.f_r._autoParam)
  (s_g_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 S.g = CategoryTheory.CategoryStruct.id S.X₃)
      CategoryTheory.ShortComplex.Splitting.s_g._autoParam)
  (id_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp r_1 S.f + CategoryTheory.CategoryStruct.comp S.g s_1 =
        CategoryTheory.CategoryStruct.id S.X₂)
      CategoryTheory.ShortComplex.Splitting.id._autoParam),
  ({ r := r, s := s, f_r := f_r, s_g := s_g, id := id } =
      { r := r_1, s := s_1, f_r := f_r_1, s_g := s_g_1, id := id_1 }) =
    (r = r_1 ∧ s = s_1)