-- 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)) →
    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₂
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₂ ∉
        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)) →
      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₂
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₂
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₂ ∉
        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)) →
      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₂
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₂
h₅ 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₂ ∉
        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)) →
      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₂

Tactic:
tauto