-- 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
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Function.Exact (M :=
    (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₀)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯))
            (AddCommGrpCat.ofHom (precomp hS.extClass Y h)) ⋯).X₁ :
      Type w))
    (N :=
    (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₀)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯))
            (AddCommGrpCat.ofHom (precomp hS.extClass Y h)) ⋯).X₂ :
      Type w))
    (P :=
    (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₀)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯))
            (AddCommGrpCat.ofHom (precomp hS.extClass Y h)) ⋯).X₃ :
      Type w))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier)
          (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₀))
              (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) (AddCommGrpCat.ofHom (precomp hS.extClass Y h)) ⋯).f) :
      (a :
          (↑{ X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
                  X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
                  g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.X₁ :
            Type w)) →
        (↑{ X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
                X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
                g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.X₂ :
          Type w))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier)
          (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₀))
              (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) (AddCommGrpCat.ofHom (precomp hS.extClass Y h)) ⋯).g) :
      (a :
          (↑{ X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
                  X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
                  g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.X₂ :
            Type w)) →
        (↑{ X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
                X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
                g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.X₃ :
          Type w))
have comm₁₂ : (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CC :=
        AddCommGrpCat.carrier)
        (ShortComplex.mk (X₁ :=
            Functor.obj (C := (DerivedCategory C)ᵒᵖ)
              (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
              (Triangle.obj₂
                (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))))
            (Functor.map
              (Functor.shift (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y)) (M := ℤ) (↑n₀ : ℤ))
              (Triangle.mor₂
                (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))))
            (Functor.homologySequenceδ (Functor.obj preadditiveYoneda (Functor.obj (singleFunctor C 0) Y))
              (Functor.obj (Equivalence.functor (triangleOpEquivalence (DerivedCategory C))) (op hS.singleTriangle))
              (↑n₀ : ℤ) (↑n₁ : ℤ) sorry)
            sorry).f).comp
    (↑homAddEquiv : Ext S.X₂ Y n₀ →+ ShiftedHom ((singleFunctor C 0).obj S.X₂) ((singleFunctor C 0).obj Y) (↑n₀ : ℤ)) =
  AddMonoidHom.comp
    (↑homAddEquiv : Ext S.X₁ Y n₀ →+ ShiftedHom ((singleFunctor C 0).obj S.X₁) ((singleFunctor C 0).obj Y) (↑n₀ : ℤ))
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
      AddCommGrpCat.carrier)
      (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₂ Y n₀)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y sorry))
          (AddCommGrpCat.ofHom (precomp hS.extClass Y h)) sorry).f)
Tactic: apply Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv)
    (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv) (H := this)