-- Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst_1 : (X Y : C) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{w, v, u, u_1} C FC (CC := CC)
inst_3 :
  HasForget₂.{w, v, u, u_1, w, w + 1, w} C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)
inst_4 : Preadditive.{v, u} C
inst_5 :
  Functor.Additive.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
inst_6 :
  Functor.PreservesHomology.{v, u, w, w + 1}
    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
      (CD := AddCommGrpCat.carrier))
S : ShortComplex.{v, u} C
inst_7 : S.HasHomology
rw :
  (∀
      (x₂ :
        (↑(X₂
              (S.map
                (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                  (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)))) :
          Type w)),
      Eq (α :=
          (↑(X₃
                (S.map
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)))) :
            Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  AddCommGrpCat.carrier) (X :=
                  X₂
                    (S.map
                      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                        (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))))
                  (g
                    (S.map
                      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                        (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)))) :
                (a : (↑(S.map (forget₂ C Ab)).X₂ : Type w)) → (↑(S.map (forget₂ C Ab)).X₃ : Type w))
              x₂ :
            (↑(X₃
                  (S.map
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                      (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)))) :
              Type w))
          (0 :
            (↑(X₃
                  (S.map
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                      (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)))) :
              Type w)) →
        ∃ (x₁ :
          (↑(X₁
                (S.map
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)))) :
            Type w)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  AddCommGrpCat.carrier) (X :=
                  X₁
                    (S.map
                      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                        (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))))
                  (f
                    (S.map
                      (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                        (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier)))) :
                (a : (↑(S.map (forget₂ C Ab)).X₁ : Type w)) → (↑(S.map (forget₂ C Ab)).X₂ : Type w))
              x₁ =
            x₂) ↔
    ∀
      (x₂ :
        (↑(Functor.obj.{v, w, u, w + 1}
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
              S.X₂) :
          Type w)),
      Eq (α :=
          (↑(Functor.obj.{v, w, u, w + 1}
                (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                  (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                S.X₃) :
            Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  AddCommGrpCat.carrier) (X :=
                  Functor.obj.{v, w, u, w + 1}
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                      (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                    S.X₂)
                  (Functor.map
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                      (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                    S.g) :
                (a : (↑((forget₂ C Ab).obj S.X₂) : Type w)) → (↑((forget₂ C Ab).obj S.X₃) : Type w))
              x₂ :
            (↑(Functor.obj.{v, w, u, w + 1}
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                  S.X₃) :
              Type w))
          (0 :
            (↑(Functor.obj.{v, w, u, w + 1}
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                  S.X₃) :
              Type w)) →
        ∃ (x₁ :
          (↑(Functor.obj.{v, w, u, w + 1}
                (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                  (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                S.X₁) :
            Type w)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  AddCommGrpCat.carrier) (X :=
                  Functor.obj.{v, w, u, w + 1}
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                      (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                    S.X₁)
                  (Functor.map
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                      (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                    S.f) :
                (a : (↑((forget₂ C Ab).obj S.X₁) : Type w)) → (↑((forget₂ C Ab).obj S.X₂) : Type w))
              x₁ =
            x₂
⊢ S.Exact ↔
    ∀
      (x₂ :
        (↑(Functor.obj.{v, w, u, w + 1}
              (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
              S.X₂) :
          Type w)),
      Eq (α :=
          (↑(Functor.obj.{v, w, u, w + 1}
                (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                  (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                S.X₃) :
            Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  AddCommGrpCat.carrier) (X :=
                  Functor.obj.{v, w, u, w + 1}
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                      (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                    S.X₂)
                  (Functor.map
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                      (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                    S.g) :
                (a : (↑((forget₂ C Ab).obj S.X₂) : Type w)) → (↑((forget₂ C Ab).obj S.X₃) : Type w))
              x₂ :
            (↑(Functor.obj.{v, w, u, w + 1}
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                  S.X₃) :
              Type w))
          (0 :
            (↑(Functor.obj.{v, w, u, w + 1}
                  (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                    (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                  S.X₃) :
              Type w)) →
        ∃ (x₁ :
          (↑(Functor.obj.{v, w, u, w + 1}
                (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                  (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                S.X₁) :
            Type w)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  AddCommGrpCat.carrier) (X :=
                  Functor.obj.{v, w, u, w + 1}
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                      (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                    S.X₁)
                  (Functor.map
                    (forget₂ C (FC := FC) (CC := CC) Ab (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦
                      (↑x1 : Type w) →+ (↑x2 : Type w)) (CD := AddCommGrpCat.carrier))
                    S.f) :
                (a : (↑((forget₂ C Ab).obj S.X₁) : Type w)) → (↑((forget₂ C Ab).obj S.X₂) : Type w))
              x₁ =
            x₂

Tactic:
rw [S.exact_iff_exact_map_forget₂, ab_exact_iff]

Premises used: CategoryTheory.ShortComplex.ab_exact_iff, CategoryTheory.ShortComplex.exact_iff_exact_map_forget₂