-- 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.Hom.f
              (HomologicalComplex.d
                (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.Hom.f
              (HomologicalComplex.d
                (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.map (K₁.d i₁ i₁')).app (K₂'.X i₂) =
      (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (φ.f i₂)
Tactic: dsimp