-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Map (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Abelian.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.Additive
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
inst_7 : HasExt.{w, v, u} C
inst_8 : HasExt.{w', v', u'} D
X Y : C
f : X ⟶ Y
⊢ Eq.{w' + 1} (α := Ext.{w', v', u'} (F.obj X) (F.obj Y) 0)
    (SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) 0 ⋯
      (CategoryStruct.comp (Y :=
        Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
          (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
            HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
            (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
          (Functor.obj (CochainComplex.singleFunctor C 0) X))
        (Iso.inv (Iso.app (F.mapCochainComplexSingleFunctor 0) X) :
          Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
            (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) X)
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
              (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
                HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
                (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
              (Functor.obj (CochainComplex.singleFunctor C 0) X)))
        (Functor.map
              (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
                HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
                (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
              (Functor.map (CochainComplex.singleFunctor C 0) f) ≫
            Iso.hom (Iso.app (F.mapCochainComplexSingleFunctor 0) Y) :
          Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
              (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
                HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
                (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
              (Functor.obj (CochainComplex.singleFunctor C 0) X))
            (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) Y))))
    (SmallShiftedHom.mk₀ (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) 0 mk₀._proof_1
      (Functor.map (CochainComplex.singleFunctor D 0) (F.map f)))
have e_f : Eq (α :=
  Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
    (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) X) (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) Y))
  (CategoryStruct.comp (Y :=
    Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
      (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
        HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
        (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
      (Functor.obj (CochainComplex.singleFunctor C 0) X))
    (Iso.inv (Iso.app (F.mapCochainComplexSingleFunctor 0) X) :
      Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
        (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) X)
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
          (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
            HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
            (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
          (Functor.obj (CochainComplex.singleFunctor C 0) X)))
    (Functor.map
          (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
            HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
            (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
          (Functor.map (CochainComplex.singleFunctor C 0) f) ≫
        Iso.hom (Iso.app (F.mapCochainComplexSingleFunctor 0) Y) :
      Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
          (LocalizerMorphism.functor (W₁ := HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (W₂ :=
            HomologicalComplex.quasiIso D (ComplexShape.up ℤ))
            (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)))
          (Functor.obj (CochainComplex.singleFunctor C 0) X))
        (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) Y)))
  (Functor.map (CochainComplex.singleFunctor D 0) (F.map f))
Tactic: congr