-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
inst_3 : HasDerivedCategory.{w', v, u} C
Y : C
n₀ : ℕ
x : Ext.{w, v, u} S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
rw :
  Eq.{w' + 1} (α :=
    (↑(Functor.obj (C := (DerivedCategory.{w', v, u} C)ᵒᵖ)
          (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₁ : ℤ))
          (Triangle.obj₁
            (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory.{w', v, u} C)))
              (op hS.singleTriangle)))) :
      Type w'))
    (Triangle.mor₃ hS.singleTriangle ≫
      Functor.map (shiftFunctor (DerivedCategory.{w', v, u} C) (A := ℤ) 1) x.hom ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' (DerivedCategory.{w', v, u} C) (↑n₀ : ℤ) 1 (↑n₁ : ℤ) ⋯))
          (Functor.obj (singleFunctor C 0) Y))
    (hS.singleδ ≫
      Functor.map (shiftFunctor (DerivedCategory.{w', v, u} C) (A := ℤ) (↑1 : ℤ)) x.hom ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' (DerivedCategory.{w', v, u} C) (↑n₀ : ℤ) (↑1 : ℤ) (↑n₁ : ℤ) ⋯))
          (Functor.obj (singleFunctor C 0) Y))
⊢ Eq (α :=
    (↑(Functor.obj (C := (DerivedCategory.{w', v, u} C)ᵒᵖ)
          (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₁ : ℤ))
          (Triangle.obj₁
            (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory.{w', v, u} C)))
              (op hS.singleTriangle)))) :
      Type w'))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj (C := (DerivedCategory.{w', v, u} C)ᵒᵖ)
              (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
              (Triangle.obj₃
                (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory.{w', v, u} C)))
                  (op hS.singleTriangle))))
            (Functor.homologySequenceδ (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y))
              (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory.{w', v, u} C)))
                (op hS.singleTriangle))
              (↑n₀ : ℤ) (↑n₁ : ℤ) ⋯) :
          (a :
              (↑(((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift (↑n₀ : ℤ)).obj
                    ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₃) :
                Type w')) →
            (↑(((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).shift (↑n₁ : ℤ)).obj
                  ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)).obj₁) :
              Type w'))
        x.hom :
      (↑(Functor.obj (C := (DerivedCategory.{w', v, u} C)ᵒᵖ)
            (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₁ : ℤ))
            (Triangle.obj₁
              (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory.{w', v, u} C)))
                (op hS.singleTriangle)))) :
        Type w'))
    ((comp hS.extClass x h).hom :
      ShiftedHom (C := DerivedCategory.{w', v, u} C) (M := ℤ) (Functor.obj (singleFunctor C 0) S.X₃)
        (Functor.obj (singleFunctor C 0) Y) (↑n₁ : ℤ))

Tactic:
rw [preadditiveYoneda_homologySequenceδ_apply,
    comp_hom, hS.extClass_hom, ShiftedHom.comp]

Premises used: CategoryTheory.ShortComplex.ShortExact.extClass_hom, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, CategoryTheory.ShiftedHom.comp, CategoryTheory.Abelian.Ext.comp_hom