-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Ab (goal)
Goal:
S : ShortComplex Ab
x₂ : (↑S.X₂ : Type u)
h :
  (Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          x₂) →
    (Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) ↔
      Membership.mem (γ := Set (↑S.X₂ : Type u))
        (Set.range (ι := (↑S.X₁ : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f) :
            (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)))
        x₂)
⊢ (Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) →
      ∃ (x₁ : (↑S.X₁ : Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f :
              (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
            x₁ =
          x₂) ↔
    (Eq (α := (↑S.X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.g :
              (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
            x₂ :
          (↑S.X₃ : Type u))
        (0 : (↑S.X₃ : Type u)) ↔
      Membership.mem (γ := Set (↑S.X₂ : Type u))
        (Set.range (ι := (↑S.X₁ : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) S.f) :
            (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)))
        x₂)
have h₁ : (Eq (α := (↑S.X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.g :
            (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
          x₂ :
        (↑S.X₃ : Type u))
      (0 : (↑S.X₃ : Type u)) ↔
    Membership.mem (γ := Set (↑S.X₂ : Type u))
      (Set.range (ι := (↑S.X₁ : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.f) :
          (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u)))
      x₂) →
  Eq (α := (↑S.X₃ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.g :
            (a : (↑S.X₂ : Type u)) → (↑S.X₃ : Type u))
          x₂ :
        (↑S.X₃ : Type u))
      (0 : (↑S.X₃ : Type u)) →
    ∃ (x₁ : (↑S.X₁ : Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) S.f :
            (a : (↑S.X₁ : Type u)) → (↑S.X₂ : Type u))
          x₁ =
        x₂
Tactic: constructor