-- 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 : HasDerivedCategory.{t, v, u} C
inst_8 : HasDerivedCategory.{t', v', u'} D
inst_9 : HasExt.{w, v, u} C
inst_10 : HasExt.{w', v', u'} D
X Y : C
n : ℕ
e : Ext.{w, v, u} X Y n
this :
  Eq.{t' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{t', v', u'} D) (M := ℤ) (obj (DerivedCategory.singleFunctor D 0) (F.obj X))
      (obj (DerivedCategory.singleFunctor D 0) (F.obj Y)) (↑n : ℤ))
    (hom.{t', w', v', u'} (mapExactFunctor F e))
    (ShiftedHom.comp (Y :=
      obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
        (Functor.comp (D := DerivedCategory.{t, v, u} C) DerivedCategory.Q F.mapDerivedCategory)
        (obj (CochainComplex.singleFunctor C 0) X))
      (ShiftedHom.mk₀ 0 ⋯
        (CategoryStruct.comp (Y :=
          obj DerivedCategory.Q
            (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 ℤ)))
              (obj (CochainComplex.singleFunctor C 0) X)))
          (map DerivedCategory.Q (Iso.inv (Iso.app (F.mapCochainComplexSingleFunctor 0) X)) :
            Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
              (obj DerivedCategory.Q (obj (F ⋙ CochainComplex.singleFunctor D 0) X))
              (obj DerivedCategory.Q
                (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 ℤ)))
                  (obj (CochainComplex.singleFunctor C 0) X))))
          (NatTrans.app (Iso.hom (Iso.symm F.mapDerivedCategoryFactors)) (obj (CochainComplex.singleFunctor C 0) X) :
            Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
              (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 ℤ)) ⋙
                  DerivedCategory.Q)
                (obj (CochainComplex.singleFunctor C 0) X))
              (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.comp (D := DerivedCategory.{t, v, u} C) DerivedCategory.Q F.mapDerivedCategory)
                (obj (CochainComplex.singleFunctor C 0) X)))))
      (ShiftedHom.comp (Y :=
        obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
          (obj DerivedCategory.Q (obj (CochainComplex.singleFunctor C 0) Y)))
        (ShiftedHom.map
          ((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q :
              (a :
                  SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
                    ((CochainComplex.singleFunctor C 0).obj X) ((CochainComplex.singleFunctor C 0).obj Y) (↑n : ℤ)) →
                ShiftedHom (DerivedCategory.Q.obj ((CochainComplex.singleFunctor C 0).obj X))
                  (DerivedCategory.Q.obj ((CochainComplex.singleFunctor C 0).obj Y)) (↑n : ℤ))
            e)
          F.mapDerivedCategory)
        (ShiftedHom.mk₀ 0 ⋯
          (NatTrans.app (Iso.inv (Iso.symm F.mapDerivedCategoryFactors)) (obj (CochainComplex.singleFunctor C 0) Y) ≫
            map DerivedCategory.Q (Iso.hom (Iso.app (F.mapCochainComplexSingleFunctor 0) Y))))
        ⋯)
      ⋯)
e_f :
  Eq.{t' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
      (obj DerivedCategory.Q (obj (F ⋙ CochainComplex.singleFunctor D 0) X))
      (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
        (Functor.comp (D := DerivedCategory.{t, v, u} C) DerivedCategory.Q F.mapDerivedCategory)
        (obj (CochainComplex.singleFunctor C 0) X)))
    (CategoryStruct.comp (Y :=
      obj DerivedCategory.Q
        (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 ℤ)))
          (obj (CochainComplex.singleFunctor C 0) X)))
      (map DerivedCategory.Q (Iso.inv (Iso.app (F.mapCochainComplexSingleFunctor 0) X)) :
        Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
          (obj DerivedCategory.Q (obj (F ⋙ CochainComplex.singleFunctor D 0) X))
          (obj DerivedCategory.Q
            (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 ℤ)))
              (obj (CochainComplex.singleFunctor C 0) X))))
      (NatTrans.app (Iso.hom (Iso.symm F.mapDerivedCategoryFactors)) (obj (CochainComplex.singleFunctor C 0) X) :
        Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
          (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 ℤ)) ⋙
              DerivedCategory.Q)
            (obj (CochainComplex.singleFunctor C 0) X))
          (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
            (Functor.comp (D := DerivedCategory.{t, v, u} C) DerivedCategory.Q F.mapDerivedCategory)
            (obj (CochainComplex.singleFunctor C 0) X))))
    (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) X)
⊢ Eq.{t' + 1} (α :=
    ShiftedHom (C := DerivedCategory.{t', v', u'} D) (M := ℤ) (obj (DerivedCategory.singleFunctor D 0) (F.obj X))
      (obj (DerivedCategory.singleFunctor D 0) (F.obj Y)) (↑n : ℤ))
    (ShiftedHom.comp (Y :=
      obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
        (Functor.comp (D := DerivedCategory.{t, v, u} C) DerivedCategory.Q F.mapDerivedCategory)
        (obj (CochainComplex.singleFunctor C 0) X))
      (ShiftedHom.mk₀ 0 ⋯
        (CategoryStruct.comp (Y :=
          obj DerivedCategory.Q
            (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 ℤ)))
              (obj (CochainComplex.singleFunctor C 0) X)))
          (map DerivedCategory.Q (Iso.inv (Iso.app (F.mapCochainComplexSingleFunctor 0) X)) :
            Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
              (obj DerivedCategory.Q (obj (F ⋙ CochainComplex.singleFunctor D 0) X))
              (obj DerivedCategory.Q
                (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 ℤ)))
                  (obj (CochainComplex.singleFunctor C 0) X))))
          (NatTrans.app (Iso.hom (Iso.symm F.mapDerivedCategoryFactors)) (obj (CochainComplex.singleFunctor C 0) X) :
            Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
              (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 ℤ)) ⋙
                  DerivedCategory.Q)
                (obj (CochainComplex.singleFunctor C 0) X))
              (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ))
                (Functor.comp (D := DerivedCategory.{t, v, u} C) DerivedCategory.Q F.mapDerivedCategory)
                (obj (CochainComplex.singleFunctor C 0) X)))))
      (ShiftedHom.comp (Y :=
        obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
          (obj DerivedCategory.Q (obj (CochainComplex.singleFunctor C 0) Y)))
        (ShiftedHom.map
          ((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q :
              (a :
                  SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
                    ((CochainComplex.singleFunctor C 0).obj X) ((CochainComplex.singleFunctor C 0).obj Y) (↑n : ℤ)) →
                ShiftedHom (DerivedCategory.Q.obj ((CochainComplex.singleFunctor C 0).obj X))
                  (DerivedCategory.Q.obj ((CochainComplex.singleFunctor C 0).obj Y)) (↑n : ℤ))
            e)
          F.mapDerivedCategory)
        (ShiftedHom.mk₀ 0 ⋯
          (NatTrans.app (Iso.inv (Iso.symm F.mapDerivedCategoryFactors)) (obj (CochainComplex.singleFunctor C 0) Y) ≫
            map DerivedCategory.Q (Iso.hom (Iso.app (F.mapCochainComplexSingleFunctor 0) Y))))
        ⋯)
      ⋯)
    (ShiftedHom.comp (Y :=
      obj (Functor.comp (D := DerivedCategory.{t, v, u} C) (DerivedCategory.singleFunctor C 0) F.mapDerivedCategory) X)
      (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) X))
      (ShiftedHom.comp (ShiftedHom.map e.hom F.mapDerivedCategory)
        (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) Y)) ⋯)
      ⋯)
have e_g : Eq.{t' + 1} (α :=
  ShiftedHom (C := DerivedCategory.{t', v', u'} D) (M := ℤ)
    (obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
      (obj DerivedCategory.Q (obj (CochainComplex.singleFunctor C 0) Y)))
    (obj DerivedCategory.Q (obj (F ⋙ CochainComplex.singleFunctor D 0) Y)) 0)
  (ShiftedHom.mk₀ 0 sorry
    (NatTrans.app (Iso.inv (Iso.symm F.mapDerivedCategoryFactors)) (obj (CochainComplex.singleFunctor C 0) Y) ≫
      map DerivedCategory.Q (Iso.hom (Iso.app (F.mapCochainComplexSingleFunctor 0) Y))))
  (ShiftedHom.mk₀ 0 sorry (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) Y))
Tactic: congr 2