-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
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
⊢ { 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
have 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry }.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 := sorry }.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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry }.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 := sorry }.X₂ :
                Type u))
          x₁ =
        x₂
Tactic: rw [ShortComplex.moduleCat_exact_iff]