∀ {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₁₂]
  (i₁₂ i₁₂' : I₁₂) (i : I₁ × I₂) (h : c₁.π c₂ c₁₂ i = i₁₂) {Z : C}
  (h_1 : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ h)
      (CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') h_1) =
    CategoryTheory.CategoryStruct.comp (K.d₁ c₁₂ i.1 i.2 i₁₂') h_1