-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
rw :
  ∀
    (x₂ :
      (↑{ X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
              X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
              X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
              g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ : ShortComplex (ModuleCat ℤ) }.X₂ :
        Type u)),
    Eq (α :=
        (↑{ X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
                X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
                X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
                g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ : ShortComplex (ModuleCat ℤ) }.X₃ :
          Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier)
                { X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
                    X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
                    X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
                    g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ : ShortComplex (ModuleCat ℤ) }.g :
              (a :
                  (↑{ X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
                          X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
                          X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
                          g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.X₂ :
                    Type u)) →
                (↑{ X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
                        X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
                        X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
                        g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.X₃ :
                  Type u))
            x₂ :
          (↑{ X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
                  X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
                  X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
                  g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ : ShortComplex (ModuleCat ℤ) }.X₃ :
            Type u))
        (0 :
          (↑{ X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
                  X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
                  X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
                  g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ : ShortComplex (ModuleCat ℤ) }.X₃ :
            Type u)) →
      ∃ (x₁ :
        (↑{ X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
                X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
                X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
                g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ : ShortComplex (ModuleCat ℤ) }.X₁ :
          Type u)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat ℤ) ↦ (↑x1 : Type u) →ₗ[ℤ] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier)
                { X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
                    X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
                    X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
                    g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ : ShortComplex (ModuleCat ℤ) }.f :
              (a :
                  (↑{ X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
                          X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
                          X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
                          g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.X₁ :
                    Type u)) →
                (↑{ X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
                        X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
                        X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
                        g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.X₂ :
                  Type u))
            x₁ =
          x₂
⊢ { X₁ := ModuleCat.of ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
      X₂ := ModuleCat.of ℤ (LocallyConstant (↑C : Type u) ℤ),
      X₃ := ModuleCat.of ℤ (LocallyConstant (↑(C' C ho) : Type u) ℤ), f := ModuleCat.ofHom (πs C o),
      g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ : ShortComplex (ModuleCat ℤ) }.Exact

Tactic:
rw [ShortComplex.moduleCat_exact_iff]

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff