-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (goal)
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₁
⊢ 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₁ : ℤ))
have 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₁ : ℤ) sorry))
        (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₁ : ℤ) sorry))
        (Functor.obj (singleFunctor C 0) Y))
Tactic: rw [preadditiveYoneda_homologySequenceδ_apply,
    comp_hom, hS.extClass_hom, ShiftedHom.comp]