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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
h : o ≤ ord I i → false = x i
⊢ Proj (fun (x : I) ↦ ord I x < o) x i = x i

Tactic:
simp only [Proj, ite_eq_left_iff, not_lt]

Premises used: ite_eq_left_iff, Profinite.NobelingProof.Proj, not_lt
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi : o ≤ ord I i
h : ∀ (hi : o < ord I i), false = x i
h₁ : ∀ (hi : o = ord I i), false = x i
⊢ false = x i

Tactic:
rcases hi.lt_or_eq with hi | hi

Premises used: LE.le.lt_or_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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi_1 : o ≤ ord I i
hi : o < ord I i
⊢ x i = true → ord I i < Order.succ o

Tactic:
specialize hsC x hx.1 i

Premises used: And.left
-- 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi_1 : o ≤ ord I i
hi : o < ord I i
hsC : x i = true → ord I i < Order.succ o
⊢ ¬ord I i < Order.succ o → ¬x i = true

Tactic:
rw [← not_imp_not] at hsC

Premises used: not_imp_not
-- 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi_1 : o ≤ ord I i
hi : o < ord I i
hsC : ¬ord I i < Order.succ o → ¬x i = true
⊢ o < ord I i → x i = false

Tactic:
simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC

Premises used: not_lt, Bool.not_eq_true, Order.succ_le_iff
-- 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi_1 : o ≤ ord I i
hi : o < ord I i
hsC : o < ord I i → x i = false
⊢ false = x i

Tactic:
(hsC hi).symm

Premises used: 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi_1 : o ≤ ord I i
hi : o < ord I i
hsC : o < ord I i → x i = false
⊢ false = x i

Tactic:
exact (hsC hi).symm

Premises used: 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi_1 : o ≤ ord I i
hi : o = ord I i
⊢ x ∈ C ∧ x (term I ho) = false

Tactic:
simp only [C0, Set.mem_inter_iff, Set.mem_setOf_eq] at hx

Premises used: Profinite.NobelingProof.C0, Set.mem_inter_iff, Set.mem_setOf_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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
i : I
hi_1 : o ≤ ord I i
hi : o = ord I i
hx : x ∈ C ∧ x (term I ho) = false
⊢ term I ho = i

Tactic:
rw [eq_comm, ord_term ho] at hi

Premises used: Profinite.NobelingProof.ord_term, eq_comm
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
i : I
hi_1 : o ≤ ord I i
hi : o = ord I i
hx : x ∈ C ∧ x (term I ho) = false
hi₁ : term I ho = i
⊢ x ∈ C ∧ x (term I ho) = false

Tactic:
rw [eq_comm, ord_term ho] at hi

Premises used: Profinite.NobelingProof.ord_term, eq_comm
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
i : I
hi_1 : o ≤ ord I i
hi : term I ho = i
hx : x ∈ C ∧ x (term I ho) = false
h : x (term I ho) = x i
h₁ h₂ : x i = x i
⊢ false = x i

Tactic:
rw [← hx.2, hi]

Premises used: And.right
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
h : ∀ (i : I), SwapTrue o (Proj (fun (x : I) ↦ ord I x < o) x) i = x i
⊢ SwapTrue o (Proj (fun (x : I) ↦ ord I x < o) x) = x

Tactic:
ext i
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
pos : ∀ (hi : ord I i = o), true = x i
pos₁ : ∀ (hi : ¬ord I i = o) (h : ord I i < o), x i = x i
neg : ∀ (hi : ¬ord I i = o) (h : ¬ord I i < o), false = x i
⊢ (if ord I i = o then true else if ord I i < o then x i else false) = x i

Tactic:
split_ifs with hi h
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ord I i = o
⊢ term I ho = i

Tactic:
rw [ord_term ho] at hi

Premises used: Profinite.NobelingProof.ord_term
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : term I ho = i
pos : x (term I ho) = x i
pos₁ pos₂ : x i = x i
⊢ true = x i

Tactic:
rw [← hx.2, hi]

Premises used: And.right
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ord I i < o
⊢ x i = x i

Tactic:
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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ¬ord I i < o
⊢ o ≤ ord I i

Tactic:
simp only [not_lt] at h

Premises used: not_lt
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
⊢ o < ord I i

Tactic:
have h' : o < ord I i := lt_of_le_of_ne h (Ne.symm hi)
-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
⊢ x i = true → ord I i < Order.succ o

Tactic:
specialize hsC x hx.1 i

Premises used: And.left
-- 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
hsC : x i = true → ord I i < Order.succ o
⊢ ¬ord I i < Order.succ o → ¬x i = true

Tactic:
rw [← not_imp_not] at hsC

Premises used: not_imp_not
-- 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
hsC : ¬ord I i < Order.succ o → ¬x i = true
⊢ o < ord I i → x i = false

Tactic:
simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC

Premises used: not_lt, Bool.not_eq_true, Order.succ_le_iff
-- 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
hsC : o < ord I i → x i = false
⊢ false = x i

Tactic:
(hsC h').symm

Premises used: 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}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
hsC : o < ord I i → x i = false
⊢ false = x i

Tactic:
exact (hsC h').symm

Premises used: 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 :
  HSub.hSub (α := LocallyConstant (↑(C' C ho) : Type u) ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ)
      ((LocallyConstant.comapₗ ℤ
              { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ : C((↑(C' C ho) : Type u), (↑C : Type u)) } :
            (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          f :
        LocallyConstant (↑(C' C ho) : Type u) ℤ)
      ((LocallyConstant.comapₗ ℤ
              { toFun := CC'₀ C ho, continuous_toFun := ⋯ : C((↑(C' C ho) : Type u), (↑C : Type u)) } :
            (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          f :
        LocallyConstant (↑(C' C ho) : Type u) ℤ) =
    0
⊢ 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)) → ℤ)

Tactic:
simp only [sub_eq_zero, ← LocallyConstant.coe_inj] at hf

Premises used: sub_eq_zero, LocallyConstant.coe_inj
-- 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) ⋯
⊢ Continuous C₀C

Tactic:
have h₀ : Continuous C₀C := Continuous.subtype_mk continuous_induced_dom _
-- 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)) ⋯
⊢ Continuous C₁C

Tactic:
have h₁ : Continuous C₁C := Continuous.subtype_mk
    ((continuous_swapTrue o).comp continuous_subtype_val) _
-- 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 : 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

Tactic:
⟨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₁⟩) ?_, ?_⟩

Premises used: LocallyConstant.comap, ContinuousMap.mk, Profinite.NobelingProof.isClosed_C0, Profinite.NobelingProof.isClosed_proj, Exists.intro, LocallyConstant.piecewise', Profinite.NobelingProof.isClosed_C1
-- 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_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 ⋯) :
        ℤ)
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) ⋯ ⋯ ⋯
        (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
⊢ ∃ (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

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₁⟩) ?_, ?_⟩
-- 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 : y ∈ C
⊢ y ∈ C0 C ho ∪ C1 C ho

Tactic:
rw [← union_C0C1_eq C ho] at hyC

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
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

Tactic:
hyC.imp (fun hyC ↦ ?_) (fun hyC ↦ ⟨y, hyC, rfl⟩)

Premises used: And.intro, Exists.intro, Or.imp, 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
y : I → Bool
hyC : y ∈ C0 C ho ∪ C1 C ho
refine_1 : ∀ (hyC : y ∈ C0 C ho), Proj (fun (x : I) ↦ ord I x < o) y ∈ C0 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

Tactic:
refine hyC.imp (fun hyC ↦ ?_) (fun hyC ↦ ⟨y, hyC, rfl⟩)

Premises used: Or.imp