-- 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
⊢ Eq.{t' + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{t', v', u'} D) (Functor.obj (F ⋙ singleFunctor D 0) S.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
        (Functor.obj (F ⋙ singleFunctor D 0) S.X₁)))
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.comp (D := DerivedCategory.{t, v, u} C) (singleFunctor C 0) F.mapDerivedCategory) S.X₃)
      (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) S.X₃)
      (ShiftedHom.map hS.singleδ F.mapDerivedCategory ≫
        Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) S.X₁)))
    (singleδ ⋯)
have dsimp : 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₃)
      (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 F.mapDerivedCategory
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S.X₃ ≫
              triangleOfSESδ sorry ≫
                Functor.map (shiftFunctor (DerivedCategory.{t, v, u} C) (A := ℤ) 1)
                  (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso 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)
          (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) S.X₁))) :
    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₁))))
  (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso D)) 0) (F.obj S.X₃) ≫
      CategoryStruct.comp (Y :=
        Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (Functor.obj (singleFunctor D 0) (F.obj S.X₁)))
        (triangleOfSESδ sorry :
          Quiver.Hom (V := DerivedCategory.{t', v', u'} D)
            (Functor.obj Q (X₃ (ShortComplex.map (S.map F) (HomologicalComplex.single D (ComplexShape.up ℤ) 0))))
            (Functor.obj (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
              (Functor.obj Q (X₁ (ShortComplex.map (S.map F) (HomologicalComplex.single D (ComplexShape.up ℤ) 0))))))
        (Functor.map (shiftFunctor (DerivedCategory.{t', v', u'} D) (A := ℤ) 1)
          (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso D)) 0) (F.obj S.X₁))) :
    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₁))))
Tactic: dsimp [ShiftedHom.map, ShortComplex.ShortExact.singleδ]