-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
X Y Z : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (i : I₁) (i_1 : I₂),
    Eq.{v_3 + 1} (α :=
      HomologicalComplex.X.{v_3, u_3, u_5}
          (HomologicalComplex.X
            (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj X.X)
              (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (X.X i₂))
              (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (X.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
            i)
          i_1 ⟶
        HomologicalComplex.X.{v_3, u_3, u_5}
          (HomologicalComplex.X
            (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj Z.X)
              (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (Z.X i₂))
              (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (Z.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
            i)
          i_1)
      (HomologicalComplex.Hom.f
        (HomologicalComplex.Hom.f
          (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (f ≫ g).f) ⋯ ⋯) i)
        i_1)
      (HomologicalComplex.Hom.f
        (HomologicalComplex.Hom.f
          (CategoryStruct.comp (Y :=
            HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj Y.X)
              (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (Y.X i₂))
              (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (Y.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
            (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map f.f) ⋯ ⋯)
            (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map g.f) ⋯ ⋯))
          i)
        i_1)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, u_4, u_5} D c₁ c₂)
      (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj X.X)
        (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (X.X i₂))
        (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (X.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
      (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj Z.X)
        (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (Z.X i₂))
        (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (Z.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯))
    (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (f ≫ g).f) ⋯ ⋯)
    (CategoryStruct.comp (Y :=
      HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj Y.X)
        (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (Y.X i₂))
        (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (Y.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
      (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map f.f) ⋯ ⋯)
      (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map g.f) ⋯ ⋯))

Tactic:
ext