-- 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₁
K₂ K₂' : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
φ : K₂ ⟶ K₂'
⊢ ∀ (i₁ : I₁) (i₂ i₂' : I₂),
    c₂.Rel i₂ i₂' →
      Eq.{v_3 + 1} (α :=
        HomologicalComplex₂.toGradedObject.{v_3, u_3, u_4, u_5}
            (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
              (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
              (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
            (i₁, i₂) ⟶
          HomologicalComplex.X.{v_3, u_3, u_5}
            (HomologicalComplex.X
              (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂'.X)
                (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂'.X i₂))
                (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂'.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
              i₁)
            i₂')
        (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map φ.f (i₁, i₂) ≫
            HomologicalComplex.d
              (HomologicalComplex.X
                (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂'.X)
                  (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂'.X i₂))
                  (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂'.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
                i₁)
              i₂ i₂' :
          HomologicalComplex₂.toGradedObject.{v_3, u_3, u_4, u_5}
              (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
                (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
                (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
              (i₁, i₂) ⟶
            HomologicalComplex.X.{v_3, u_3, u_5}
              (HomologicalComplex.X
                (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂'.X)
                  (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂'.X i₂))
                  (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂'.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
                i₁)
              i₂')
        (HomologicalComplex.d
              (HomologicalComplex.X
                (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
                  (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
                  (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
                i₁)
              i₂ i₂' ≫
            ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map φ.f (i₁, i₂') :
          HomologicalComplex.X.{v_3, u_3, u_5}
              (HomologicalComplex.X
                (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
                  (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
                  (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
                i₁)
              i₂ ⟶
            HomologicalComplex₂.toGradedObject.{v_3, u_3, u_4, u_5}
              (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂'.X)
                (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂'.X i₂))
                (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂'.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
              (i₁, i₂'))
have dsimp : ∀ (i₁ : I₁) (i₂ i₂' : I₂),
  c₂.Rel i₂ i₂' →
    (F.obj (K₁.X i₁)).map (φ.f i₂) ≫ (F.obj (K₁.X i₁)).map (K₂'.d i₂ i₂') =
      (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (K₁.X i₁)).map (φ.f i₂')
Tactic: dsimp