∀ {C₁ : Type u_5} {C₂ : Type u_7} {D : Type u_2} {I₁ : Type u_8} {I₂ : Type u_9} {J : Type u_3}
  [inst : CategoryTheory.Category.{u_4, u_5} C₁] [inst_1 : CategoryTheory.Category.{u_6, u_7} C₂]
  [inst_2 : CategoryTheory.Category.{u_1, u_2} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} (f₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂}
  {f₂ f₂' : K₂ ⟶ L₂} (h₂ : Homotopy f₂ f₂') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  (this : F.flip.Additive) (this_1 : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive),
  HomologicalComplex.mapBifunctorMapHomotopy.hom₂ f₁ h₂ F c =
      ((Homotopy.ofEq ⋯).trans
          ((((HomologicalComplex.mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight
                    (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
                (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
            (Homotopy.ofEq ⋯))).hom →
    ∀ (j : J),
      (HomologicalComplex.mapBifunctorMap f₁ f₂ F c).f j =
        (dNext j) (HomologicalComplex.mapBifunctorMapHomotopy.hom₂ f₁ h₂ F c) +
            (prevD j) (HomologicalComplex.mapBifunctorMapHomotopy.hom₂ f₁ h₂ F c) +
          (HomologicalComplex.mapBifunctorMap f₁ f₂' F c).f j