∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)),
  S.Exact →
    ∀ [CategoryTheory.Mono S.f] (i : ι) [inst_3 : S.X₁.HasHomology i] [inst_4 : S.X₂.HasHomology i]
      [inst_5 : S.X₃.HasHomology i],
      { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := HomologicalComplex.cyclesMap S.f i,
          g := HomologicalComplex.cyclesMap S.g i, zero := ⋯ }.Exact