awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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) ⋯
⊢ ∃ (y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
    (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) y =
      f
have h₀ : Continuous C₀C
Tactic: have h₀ : Continuous C₀C := Continuous.subtype_mk continuous_induced_dom _
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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)) ⋯
⊢ ∃ (y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
    (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) y =
      f
have h₁ : Continuous C₁C
Tactic: have h₁ : Continuous C₁C := Continuous.subtype_mk
    ((continuous_swapTrue o).comp continuous_subtype_val) _
-- 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
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 : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
    (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) y =
      f
have refine_1 : (π C fun (x : I) ↦ ord I x < o) ⊆ C0 C ho ∪ π (C1 C ho) fun (x : I) ↦ ord I x < o
Tactic: refine ⟨LocallyConstant.piecewise' ?_ (isClosed_C0 C hC ho)
      (isClosed_proj _ o (isClosed_C1 C hC ho)) (f.comap ⟨C₀C, h₀⟩) (f.comap ⟨C₁C, h₁⟩) ?_, ?_⟩
-- 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
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_1 : (π C fun (x : I) ↦ ord I x < o) ⊆ C0 C ho ∪ π (C1 C ho) fun (x : I) ↦ ord I x < o
⊢ ∃ (y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
    (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) y =
      f
have refine_2 : ∀ (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 sorry) :
      ℤ)
    ((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 sorry) :
      ℤ)
Tactic: refine ⟨LocallyConstant.piecewise' ?_ (isClosed_C0 C hC ho)
      (isClosed_proj _ o (isClosed_C1 C hC ho)) (f.comap ⟨C₀C, h₀⟩) (f.comap ⟨C₁C, h₁⟩) ?_, ?_⟩
-- 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
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_1 : (π C fun (x : I) ↦ ord I x < o) ⊆ C0 C ho ∪ π (C1 C ho) fun (x : I) ↦ ord I x < o
refine_2 :
  ∀ (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 ⋯) :
        ℤ)
⊢ ∃ (y : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ),
    (πs C o : (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) y =
      f
have refine_3 : (π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) sorry sorry sorry
      (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)
      sorry) =
  f
Tactic: refine ⟨LocallyConstant.piecewise' ?_ (isClosed_C0 C hC ho)
      (isClosed_proj _ o (isClosed_C1 C hC ho)) (f.comap ⟨C₀C, h₀⟩) (f.comap ⟨C₁C, h₁⟩) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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 : y ∈ C
⊢ Proj (fun (x : I) ↦ ord I x < o) y ∈ C0 C ho ∨
    Proj (fun (x : I) ↦ ord I x < o) y ∈ π (C1 C ho) fun (x : I) ↦ ord I x < o
have hyC₁ : y ∈ C0 C ho ∪ C1 C ho
Tactic: rw [← union_C0C1_eq C ho] at hyC
Cleared hypotheses: hyC
-- 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
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 : y ∈ C0 C ho ∪ C1 C ho
⊢ Proj (fun (x : I) ↦ ord I x < o) y ∈ C0 C ho ∨
    Proj (fun (x : I) ↦ ord I x < o) y ∈ π (C1 C ho) fun (x : I) ↦ ord I x < o
have refine_1 : ∀ (hyC : y ∈ C0 C ho), Proj (fun (x : I) ↦ ord I x < o) y ∈ C0 C ho
Tactic: refine hyC.imp (fun hyC ↦ ?_) (fun hyC ↦ ⟨y, hyC, rfl⟩)
-- 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
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
⊢ (π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
have 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) sorry sorry sorry
                (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)
                sorry) :
            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: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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
⊢ 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) : ℤ)
have hx₁ : x ∈ C0 C ho ∪ C1 C ho
Tactic: rw [← union_C0C1_eq C ho] at hx
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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
⊢ 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) : ℤ)
have hx₀' : (↑(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₀
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
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
⊢ 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) : ℤ)
have 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
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⟩