-- 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
inst_4 : HasDerivedCategory.{t, v, u} C
inst_5 : HasDerivedCategory.{t', v', u'} D
S : ShortComplex.{v, u} C
hS : S.ShortExact
F : Functor.{v, v', u, u'} C D
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
pf : HasZeroObject.{v, u} C
pf_1 : IsRightCancelAdd ℤ
pf_2 : IsRightCancelAdd ℤ
pf_3 : F.PreservesZeroMorphisms
pf_4 :
  Functor.PreservesZeroMorphisms (D := CochainComplex.{v, u, 0} C ℤ) (HomologicalComplex.single C (ComplexShape.up ℤ) 0)
pf_5 :
  Functor.PreservesZeroMorphisms (C := CochainComplex.{v, u, 0} C ℤ) (D := CochainComplex.{v', u', 0} D ℤ)
    (F.mapHomologicalComplex (ComplexShape.up ℤ))
h1 :
  ShortExact (C := CochainComplex.{v', u', 0} D ℤ)
    (ShortComplex.map (C := CochainComplex.{v, u, 0} C ℤ) (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))
      (F.mapHomologicalComplex (ComplexShape.up ℤ)))
pf_6 : HasZeroObject.{v', u'} D
pf_7 :
  Functor.PreservesZeroMorphisms (D := CochainComplex.{v', u', 0} D ℤ)
    (HomologicalComplex.single D (ComplexShape.up ℤ) 0)
h2 :
  ShortExact (C := CochainComplex.{v', u', 0} D ℤ)
    (ShortComplex.map (S.map F) (HomologicalComplex.single D (ComplexShape.up ℤ) 0))
⊢ Eq.{t' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{t', v', u'} D) (Functor.obj (singleFunctor D 0) (F.obj S.X₃))
      (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
        (Functor.obj (singleFunctor D 0) (F.obj S.X₁))))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory (Functor.obj (singleFunctor C 0) S.X₃))
      (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) S.X₃)
      (Functor.map F.mapDerivedCategory (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) 0) S.X₃)) ≫
        NatTrans.app (Iso.hom F.mapDerivedCategoryFactors)
            (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) 0) S.X₃) ≫
          triangleOfSESδ h1 ≫
            CategoryStruct.comp (Y :=
              Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                (Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
                  (Functor.obj (singleFunctor C 0) S.X₁)))
              (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                (NatTrans.app (Iso.inv F.mapDerivedCategoryFactors)
                  (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) 0) S.X₁)))
              (CategoryStruct.comp (Y :=
                Functor.obj (C := DerivedCategory.{t, v, u} C) F.mapDerivedCategory
                  (Functor.obj (shiftFunctor (DerivedCategory.{t, v, u} C) (A := ℤ) 1)
                    (Functor.obj (singleFunctor C 0) S.X₁)))
                (NatTrans.app (Iso.inv (Functor.commShiftIso F.mapDerivedCategory 1))
                  (Functor.obj (singleFunctor C 0) S.X₁))
                (NatTrans.app (Iso.hom (Functor.commShiftIso F.mapDerivedCategory 1))
                    (Functor.obj (singleFunctor C 0) S.X₁) ≫
                  Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                      (Functor.map F.mapDerivedCategory (𝟙 (Functor.obj (singleFunctor C 0) S.X₁))) ≫
                    Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
                      (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) S.X₁)))))
    (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors D) 0) (F.obj S.X₃)) ≫
      triangleOfSESδ h2 ≫
        Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (𝟙 (Functor.obj (singleFunctor D 0) (F.obj S.X₁))))
have rw : Eq.{t' + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{t', v', u'} D) (Functor.obj (singleFunctor D 0) (F.obj S.X₃))
    (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
      (Functor.obj (singleFunctor D 0) (F.obj S.X₁))))
  (Functor.map Q
      (CategoryStruct.comp (Y :=
        Functor.obj (C := CochainComplex.{v, u, 0} C ℤ) (F.mapHomologicalComplex (ComplexShape.up ℤ))
          (Functor.obj (CochainComplex.singleFunctor C 0) S.X₃))
        (NatTrans.app (Iso.inv (F.mapCochainComplexSingleFunctor 0)) S.X₃ :
          Quiver.Hom (V := HomologicalComplex.{v', u', 0} D (ComplexShape.up ℤ))
            (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) S.X₃)
            (Functor.obj
              (Functor.comp (D := CochainComplex.{v, u, 0} C ℤ) (CochainComplex.singleFunctor C 0)
                (F.mapHomologicalComplex (ComplexShape.up ℤ)))
              S.X₃))
        (NatTrans.app (Iso.hom (F.mapCochainComplexSingleFunctor 0)) S.X₃ :
          Quiver.Hom (V := CochainComplex.{v', u', 0} D ℤ)
            (Functor.obj
              (Functor.comp (D := CochainComplex.{v, u, 0} C ℤ) (CochainComplex.singleFunctor C 0)
                (F.mapHomologicalComplex (ComplexShape.up ℤ)))
              S.X₃)
            (Functor.obj (F ⋙ CochainComplex.singleFunctor D 0) S.X₃))) ≫
    triangleOfSESδ h2)
  (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors D) 0) (F.obj S.X₃)) ≫
    triangleOfSESδ h2 ≫
      Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
        (𝟙 (Functor.obj (singleFunctor D 0) (F.obj S.X₁))))
Tactic: rw [Functor.map_id, Category.id_comp,
    Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app_assoc,
    Iso.inv_hom_id_app_assoc, Functor.map_id, Functor.map_id, Category.id_comp,
    ← Functor.map_comp,
    F.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app,
    dsimp% triangleOfSESδ_naturality h1 h2
      (S.mapNatTrans (F.mapCochainComplexSingleFunctor 0).hom),
    ← Functor.map_comp_assoc]