∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : C} (h_1 : (DerivedCategory.homologyFunctor C n₁).obj T.obj₁ ⟶ Z),
      CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctor C n₀).map T.mor₂)
          (CategoryTheory.CategoryStruct.comp (DerivedCategory.HomologySequence.δ T n₀ n₁ h) h_1) =
        CategoryTheory.CategoryStruct.comp 0 h_1