-- 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 : LocallyConstant (↑C : Type u) ℤ
hf :
  Eq (α := (a : (↑(C' C ho) : Type u)) → ℤ)
    (⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ } :
              (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
            f :
          LocallyConstant (↑(C' C ho) : Type u) ℤ) :
      (a : (↑(C' C ho) : Type u)) → ℤ)
    (⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ } :
              (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
            f :
          LocallyConstant (↑(C' C ho) : Type u) ℤ) :
      (a : (↑(C' C ho) : Type u)) → ℤ)
C₀C : (↑(C0 C ho) : Type u) → (↑C : Type u) :=
  fun (x : (↑(C0 C ho) : Type u)) ↦ Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (↑x : I → Bool) ⋯
h₀ : Continuous C₀C
C₁C : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u) → (↑C : Type u) :=
  fun (x : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) ↦
    Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) (SwapTrue o (↑x : I → Bool)) ⋯
h₁ : Continuous C₁C
x : I → Bool
hx_1 : x ∈ C
hx : x ∈ C0 C ho ∪ C1 C ho
refine_3 :
  ∀ (hx₀ : x ∈ C0 C ho),
    Eq (α := ℤ)
      ((((πs C o :
                  (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
                (LocallyConstant.piecewise' (C₀ := π C fun (x : I) ↦ ord I x < o) (C₁ := C0 C ho) (C₂ :=
                  π (C1 C ho) fun (x : I) ↦ ord I x < o) ⋯ ⋯ ⋯
                  (LocallyConstant.comap
                    { toFun := C₀C, continuous_toFun := h₀ : C((↑(C0 C ho) : Type u), (↑C : Type u)) } f)
                  (LocallyConstant.comap
                    { toFun := C₁C, continuous_toFun := h₁ :
                      C((↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u), (↑C : Type u)) }
                    f)
                  ⋯) :
              LocallyConstant (↑C : Type u) ℤ) :
            (a : (↑C : Type u)) → ℤ)
          (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx_1) :
        ℤ)
      ((f : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx_1) : ℤ)
refine_3₁ :
  ∀ (hx₁ : x ∈ C1 C ho),
    Eq (α := ℤ)
      ((((πs C o :
                  (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
                (LocallyConstant.piecewise' (C₀ := π C fun (x : I) ↦ ord I x < o) (C₁ := C0 C ho) (C₂ :=
                  π (C1 C ho) fun (x : I) ↦ ord I x < o) ⋯ ⋯ ⋯
                  (LocallyConstant.comap
                    { toFun := C₀C, continuous_toFun := h₀ : C((↑(C0 C ho) : Type u), (↑C : Type u)) } f)
                  (LocallyConstant.comap
                    { toFun := C₁C, continuous_toFun := h₁ :
                      C((↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u), (↑C : Type u)) }
                    f)
                  ⋯) :
              LocallyConstant (↑C : Type u) ℤ) :
            (a : (↑C : Type u)) → ℤ)
          (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx_1) :
        ℤ)
      ((f : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx_1) : ℤ)
⊢ Eq (α := ℤ)
    ((((πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
              (LocallyConstant.piecewise' (C₀ := π C fun (x : I) ↦ ord I x < o) (C₁ := C0 C ho) (C₂ :=
                π (C1 C ho) fun (x : I) ↦ ord I x < o) ⋯ ⋯ ⋯
                (LocallyConstant.comap
                  { toFun := C₀C, continuous_toFun := h₀ : C((↑(C0 C ho) : Type u), (↑C : Type u)) } f)
                (LocallyConstant.comap
                  { toFun := C₁C, continuous_toFun := h₁ :
                    C((↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u), (↑C : Type u)) }
                  f)
                ⋯) :
            LocallyConstant (↑C : Type u) ℤ) :
          (a : (↑C : Type u)) → ℤ)
        (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx_1) :
      ℤ)
    ((f : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx_1) : ℤ)

Tactic:
rcases hx with hx₀ | hx₁