∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C))
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
  { X₁ := (DerivedCategory.homologyFunctor C n₀).obj T.obj₂, X₂ := (DerivedCategory.homologyFunctor C n₀).obj T.obj₃,
      X₃ := (DerivedCategory.homologyFunctor C n₁).obj T.obj₁, f := (DerivedCategory.homologyFunctor C n₀).map T.mor₂,
      g := DerivedCategory.HomologySequence.δ T n₀ n₁ h, zero := ⋯ }.Exact