-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
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
⊢ 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) ⋯ ⋯))
have 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₂')) sorry sorry sorry sorry sorry)
          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₂')) sorry sorry sorry sorry sorry)
          i)
        i_1)
    (HomologicalComplex.Hom.f
      (HomologicalComplex.Hom.f
        (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (f ≫ g).f) sorry sorry) 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₂')) sorry sorry sorry sorry sorry)
          (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map f.f) sorry sorry)
          (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map g.f) sorry sorry))
        i)
      i_1)
Tactic: ext