-- 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 : x ∈ C
hx₁ : x ∈ C1 C ho
hx₁' :
  (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) : I → Bool) ∈
    π (C1 C ho) fun (x : I) ↦ ord I x < o
refine_3 :
  Eq (α := ℤ)
    ((f : (a : (↑C : Type u)) → ℤ)
        (({
                toFun := 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)) ⋯,
                continuous_toFun := h₁ : C((↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u), (↑C : Type u)) } :
              (a : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) → (↑C : Type u))
            (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π (C1 C ho) fun (x : I) ↦ ord I x < o)
              (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) :
                I → Bool)
              hx₁') :
          (↑C : Type u)) :
      ℤ)
    ((f : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx) : ℤ)
⊢ 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) :
      ℤ)
    ((f : (a : (↑C : Type u)) → ℤ) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx) : ℤ)

Tactic:
simp only [C₁C, πs_apply_apply, LocallyConstant.coe_comap,
        Function.comp_apply, hx₁', LocallyConstant.piecewise'_apply_right]

Premises used: LocallyConstant.coe_comap, Profinite.NobelingProof.πs_apply_apply, Function.comp_apply, LocallyConstant.piecewise'_apply_right