awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
y : I → Bool
hyC_1 : y ∈ C0 C ho ∪ C1 C ho
hyC refine_1 refine_1₁ refine_1₂ refine_1₃ : y ∈ C0 C ho
⊢ Proj (fun (x : I) ↦ ord I x < o) y ∈ C0 C ho

Tactic:
rwa [C0_projOrd C hsC ho hyC]

Premises used: Profinite.NobelingProof.C0_projOrd
-- 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 ∈ C0 C ho ∩ π (C1 C ho) fun (x : I) ↦ ord I x < o
⊢ Eq (α := ℤ)
    ((LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ : C((↑(C0 C ho) : Type u), (↑C : Type u)) } f :
          (a : (↑(C0 C ho) : Type u)) → ℤ)
        (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C0 C ho) x ⋯) :
      ℤ)
    ((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 :
          (a : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)) → ℤ)
        (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π (C1 C ho) fun (x : I) ↦ ord I x < o) x ⋯) :
      ℤ)

Tactic:
simpa only [h₀, h₁, LocallyConstant.coe_comap] using (congrFun hf ⟨x, hx⟩).symm

Premises used: LocallyConstant.coe_comap, Subtype.mk, congrFun, Eq.symm
-- 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
refine_3 :
  ∀ (x : I → Bool) (hx : x ∈ C),
    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) : ℤ)
⊢ (π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)
        ⋯) =
    f

Tactic:
ext ⟨x, hx⟩
-- 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
⊢ x ∈ C0 C ho ∪ C1 C ho

Tactic:
rw [← union_C0C1_eq C ho] at hx

Premises used: Profinite.NobelingProof.union_C0C1_eq
-- 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 ∈ C0 C ho
⊢ (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) : I → Bool) = x

Tactic:
simpa only [ProjRestrict, Set.MapsTo.val_restrict_apply] using C0_projOrd C hsC ho hx₀

Premises used: Set.MapsTo.val_restrict_apply, Profinite.NobelingProof.ProjRestrict, Profinite.NobelingProof.C0_projOrd
-- 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 ∈ C0 C ho
⊢ (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) : I → Bool) = x

Tactic:
have hx₀' : ProjRestrict C (ord I · < o) ⟨x, hx⟩ = x := by
        simpa only [ProjRestrict, Set.MapsTo.val_restrict_apply] using C0_projOrd C hsC ho hx₀
-- 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 ∈ C0 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) = x
⊢ 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, hx₀', hx₀, LocallyConstant.piecewise'_apply_left,
        LocallyConstant.coe_comap, ContinuousMap.coe_mk, Function.comp_apply]

Premises used: LocallyConstant.coe_comap, LocallyConstant.piecewise'_apply_left, Profinite.NobelingProof.πs_apply_apply, ContinuousMap.coe_mk, Function.comp_apply
-- 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
⊢ (↑(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

Tactic:
simpa only [ProjRestrict, Set.MapsTo.val_restrict_apply] using ⟨x, hx₁, rfl⟩

Premises used: Set.MapsTo.val_restrict_apply, Profinite.NobelingProof.ProjRestrict
-- 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
⊢ (↑(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

Tactic:
have hx₁' : (ProjRestrict C (ord I · < o) ⟨x, hx⟩).val ∈ π (C1 C ho) (ord I · < o) := by
        simpa only [ProjRestrict, Set.MapsTo.val_restrict_apply] using ⟨x, hx₁, rfl⟩
-- 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 :
  ({
          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₁') =
    Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx
⊢ 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) : ℤ)

Tactic:
congr
-- 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 :
  SwapTrue o
      (↑(ProjRestrict C (fun (x : I) ↦ ord I x < o) (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx)) : I → Bool) =
    x
⊢ ({
          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₁') =
    Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ C) x hx

Tactic:
simp only [ContinuousMap.coe_mk, Subtype.mk.injEq]

Premises used: ContinuousMap.coe_mk, Subtype.mk.injEq