∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (h₁ : S₁.ShortExact)
  (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂), (DerivedCategory.triangleOfSES.map h₁ h₂ f).hom₁ = DerivedCategory.Q.map f.τ₁