∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.RightHomologyData) (H₂ : S₂.RightHomologyData) (h₀ : S₁.X₁ ⟶ S₂.X₁)
  (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  CategoryTheory.CategoryStruct.comp H₁.p
      (H₁.descQ (CategoryTheory.CategoryStruct.comp S₁.g (CategoryTheory.CategoryStruct.comp h₂ H₂.p)) ⋯) =
    CategoryTheory.CategoryStruct.comp (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ H₂.p