-- 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
Y : C
n : ℕ
x₂ : Ext.{w, v, u} S.X₂ Y n
hx₂ : comp (mk₀ S.f) x₂ ⋯ = 0
this :
  ∀
    (x₂ :
      (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n)) (AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y ⋯))
              (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) ⋯).X₂ :
        Type w)),
    Eq (α :=
        (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n))
                (AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y ⋯)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) ⋯).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.g) Y ⋯)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) ⋯).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.g).precomp Y ⋯),
                          g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), 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.g).precomp Y ⋯),
                        g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.X₃ :
                  Type w))
            x₂ :
          (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n))
                  (AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y ⋯)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) ⋯).X₃ :
            Type w))
        (0 :
          (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n))
                  (AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y ⋯)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) ⋯).X₃ :
            Type w)) →
      ∃ (x₁ :
        (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} S.X₃ Y n))
                (AddCommGrpCat.ofHom (precomp (mk₀ S.g) Y ⋯)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) ⋯).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.g) Y ⋯)) (AddCommGrpCat.ofHom (precomp (mk₀ S.f) Y ⋯)) ⋯).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.g).precomp Y ⋯),
                          g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), 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.g).precomp Y ⋯),
                        g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.X₂ :
                  Type w))
            x₁ =
          x₂
⊢ ∃ (x₁ : Ext.{w, v, u} S.X₃ Y n), comp (mk₀ S.g) x₁ ⋯ = x₂

Tactic:
this x₂ hx₂

Premises used: CategoryTheory.Localization.SmallHom, CategoryTheory.Abelian.Ext.comp, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Abelian.Ext, CategoryTheory.Localization.SmallShiftedHom.comp, CategoryTheory.Localization.SmallShiftedHom