-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
      triangleOfSESδ ⋯ ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (Functor.map Q (Functor.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0) f.τ₁)) ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
have rw : Eq.{w + 1} (α :=
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
    (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
  (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
    CategoryStruct.comp (Y := Functor.obj (singleFunctor C 0) S₂.X₃)
      (Functor.map Q (Functor.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0) f.τ₃) :
        Quiver.Hom (V := DerivedCategory.{w, v, u} C)
          (Functor.obj Q (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) 0) S₁.X₃))
          (Functor.obj Q (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) 0) S₂.X₃)))
      (CategoryStruct.comp (Y :=
          Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁))
          (triangleOfSESδ sorry :
            Quiver.Hom (V := DerivedCategory.{w, v, u} C)
              (Functor.obj Q (X₃ (S₂.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))))
              (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
                (Functor.obj Q (X₁ (S₂.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))))))
          (Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁)) :
        Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₂.X₃)
          (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (Functor.obj (singleFunctor C 0) S₂.X₁))))
  (Functor.map (singleFunctor C 0) f.τ₃ ≫
    NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
      triangleOfSESδ sorry ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
          (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
Tactic: rw [reassoc_of% dsimp% ((triangleOfSES.map (h₁.map_of_exact _) (h₂.map_of_exact _))
      ((HomologicalComplex.single C (.up ℤ) 0).mapShortComplex.map f)).comm₃]