-- Module: Mathlib.Algebra.Homology.ShortComplex.Ab
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₂)
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₂
⊢ (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₂)

Tactic:
constructor