-- 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
f :
  (↑{ 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))
          f :
        (↑{ 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₁ =
        f

Tactic:
CC_exact C hC hsC ho

Premises used: Profinite.NobelingProof.CC_exact