-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
x₂ : Ext.{w, v, u} X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
this :
  (ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X ⋯))
      (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X ⋯)) ⋯).Exact
⊢ ∃ (x₁ : Ext.{w, v, u} X S.X₁ n), x₁.comp (mk₀ S.f) ⋯ = x₂
have this₁ : ∀
  (x₂ :
    (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X sorry))
            (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X sorry)) sorry).X₂ :
      Type w)),
  Eq (α :=
      (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n))
              (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X sorry)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X sorry)) sorry).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} X S.X₁ n))
                  (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X sorry)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X sorry)) sorry).g :
            (a :
                (↑{ X₁ := AddCommGrpCat.of (Ext X S.X₁ n), X₂ := AddCommGrpCat.of (Ext X S.X₂ n),
                        X₃ := AddCommGrpCat.of (Ext X S.X₃ n), f := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X sorry),
                        g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X sorry), zero := sorry }.X₂ :
                  Type w)) →
              (↑{ X₁ := AddCommGrpCat.of (Ext X S.X₁ n), X₂ := AddCommGrpCat.of (Ext X S.X₂ n),
                      X₃ := AddCommGrpCat.of (Ext X S.X₃ n), f := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X sorry),
                      g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X sorry), zero := sorry }.X₃ :
                Type w))
          x₂ :
        (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n))
                (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X sorry)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X sorry)) sorry).X₃ :
          Type w))
      (0 :
        (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n))
                (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X sorry)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X sorry)) sorry).X₃ :
          Type w)) →
    ∃ (x₁ :
      (↑(ShortComplex.mk (X₁ := AddCommGrpCat.of (Ext.{w, v, u} X S.X₁ n))
              (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X sorry)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X sorry)) sorry).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} X S.X₁ n))
                  (AddCommGrpCat.ofHom (postcomp (mk₀ S.f) X sorry)) (AddCommGrpCat.ofHom (postcomp (mk₀ S.g) X sorry)) sorry).f :
            (a :
                (↑{ X₁ := AddCommGrpCat.of (Ext X S.X₁ n), X₂ := AddCommGrpCat.of (Ext X S.X₂ n),
                        X₃ := AddCommGrpCat.of (Ext X S.X₃ n), f := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X sorry),
                        g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X sorry), zero := sorry }.X₁ :
                  Type w)) →
              (↑{ X₁ := AddCommGrpCat.of (Ext X S.X₁ n), X₂ := AddCommGrpCat.of (Ext X S.X₂ n),
                      X₃ := AddCommGrpCat.of (Ext X S.X₃ n), f := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X sorry),
                      g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X sorry), zero := sorry }.X₂ :
                Type w))
          x₁ =
        x₂
Tactic: rw [ShortComplex.ab_exact_iff] at this
Cleared hypotheses: this