∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (y : ℤ) [inst_8 : K₁.HasMapBifunctor K₂ F] (n₁ n₂ n : ℤ) (h : n₁ + n₂ = n)
  (m₂ m : ℤ) (hm₂ : m₂ = n₂ + y) (hm : m = n + y) {Z : D}
  (h_1 : ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).obj (K₁.mapBifunctor K₂ F)).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (K₁.ιMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F n₁ n₂ n h)
      (CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctorShift₂Iso K₂ F y).hom.f n) h_1) =
    CategoryTheory.CategoryStruct.comp
      ((n₁ * y).negOnePow •
        CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X n₁)).map (K₂.shiftFunctorObjXIso y n₂ m₂ hm₂).hom)
          (CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯)
            ((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso y n m hm).inv))
      h_1