∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  {c₁₂ : ComplexShape I₁₂} [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {A : C} {i₁₂ : I₁₂} (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)) (i₁ : I₁) (i₂ : I₂)
  (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi)
      (CategoryTheory.CategoryStruct.comp (K.totalDesc f) h) =
    CategoryTheory.CategoryStruct.comp (f i₁ i₂ hi) h