mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h.inr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i
l : ℕ
hln : l < n.succ
j : cell C l
hj : j ∈ J l
hxj : x ∈ cellFrontier l j ∪ openCell l j
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1

Tactic:
]

Goal state after:
case h.inr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i
l : ℕ
hln : l < n.succ
j : cell C l
hj : j ∈ J l
hxj : x ∈ cellFrontier l j ∪ openCell l j
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
y : I → Bool
hyC✝ : y ∈ C0 C ho ∪ C1 C ho
hyC : y ∈ C0 C ho
⊢ y ∈ C0 C ho

Tactic:
]

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
y : I → Bool
hyC✝ : y ∈ C0 C ho ∪ C1 C ho
hyC : y ∈ C0 C ho
⊢ y ∈ C0 C ho
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
x : ↑(π C fun x ↦ ord I x < o₂)
⊢ ((πs' C h) (Products.eval (π C fun x ↦ ord I x < o₁) l)) x =
    ((πs' C h) (Products.eval (π C fun x ↦ ord I x < o₁) ↑⟨l, gl⟩)) x

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ ((eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩).toFun ∘ ProjRestrict C fun x ↦ ord I x < o₁) =
    ⇑(eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩) ∘ ProjRestrict C fun x ↦ ord I x < o₁

Tactic:
]

Goal state after:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ ((eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩).toFun ∘ ProjRestrict C fun x ↦ ord I x < o₁) =
    ⇑(eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩) ∘ ProjRestrict C fun x ↦ ord I x < o₁
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case refine_3
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx✝ : x ∈ C
hx : x ∈ C0 C ho ∪ C1 C ho
⊢ ((πs C o)
        (LocallyConstant.piecewise' ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
          (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⋯))
      ⟨x, hx✝⟩ =
    f ⟨x, hx✝⟩

Tactic:
]

Goal state after:
case refine_3
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx✝ : x ∈ C
hx : x ∈ C0 C ho ∪ C1 C ho
⊢ ((πs C o)
        (LocallyConstant.piecewise' ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
          (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⋯))
      ⟨x, hx✝⟩ =
    f ⟨x, hx✝⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hlt : ∀ i ∈ ↑l, ord I i < o₁
⊢ ((πs' C h) (eval (π C fun x ↦ ord I x < o₁) l)).toFun = ⇑(eval (π C fun x ↦ ord I x < o₂) l)

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hlt : ∀ i ∈ ↑l, ord I i < o₁
⊢ ((πs' C h) (eval (π C fun x ↦ ord I x < o₁) l)).toFun = ⇑(eval (π C fun x ↦ ord I x < o₂) l)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
f : LocallyConstant ↑C ℤ
m : Products I
hm : m < l
⊢ eval C m = f ↔ eval C m = f

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
⊢ eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})

Tactic:
]

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
⊢ eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Injective ⇑(ConcreteCategory.hom (ModuleCat.ofHom (πs C o)))

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Function.Injective ⇑(ConcreteCategory.hom (ModuleCat.ofHom (πs C o)))
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case e_I
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I✝¹ : (n : ℕ) → Set (cell C n)
closed'✝¹ : IsClosed[t] E
hE : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
F : Set X
I✝ : (n : ℕ) → Set (cell C n)
closed'✝ : IsClosed[t] F
hF : D ∪ ⋃ n, ⋃ j, openCell n ↑j = F
h :
  (fun E ↦ E.carrier) { carrier := E, I := I✝¹, closed' := closed'✝¹, union' := hE } =
    (fun E ↦ E.carrier) { carrier := F, I := I✝, closed' := closed'✝, union' := hF }
⊢ E = F

Tactic:
]

Goal state after:
case e_I
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I✝¹ : (n : ℕ) → Set (cell C n)
closed'✝¹ : IsClosed[t] E
hE : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
F : Set X
I✝ : (n : ℕ) → Set (cell C n)
closed'✝ : IsClosed[t] F
hF : D ∪ ⋃ n, ⋃ j, openCell n ↑j = F
h :
  (fun E ↦ E.carrier) { carrier := E, I := I✝¹, closed' := closed'✝¹, union' := hE } =
    (fun E ↦ E.carrier) { carrier := F, I := I✝, closed' := closed'✝, union' := hF }
⊢ E = F
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₂) ℤ
m : Products I
hm : m < l
⊢ eval (π C fun x ↦ ord I x < o₂) m = f ↔ eval (π C fun x ↦ ord I x < o₂) m = f

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₂) ℤ
m : Products I
hm : m < l
⊢ eval (π C fun x ↦ ord I x < o₂) m = f ↔ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) m) = f

Tactic:
rw [eval_πs' C h (lt_ord_of_lt hm hl)]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
l : Products I
hl✝ : Products.isGood C l
hl : ∃ o' < o, Products.isGood (π C fun x ↦ ord I x < o') l
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1, ∃ (h_1 : Products.isGood (π C fun x ↦ ord I x < a) a_1), eval (π C fun x ↦ ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = eval C ⟨l, hl✝⟩

Tactic:
]

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
l : Products I
hl✝ : Products.isGood C l
hl : ∃ o' < o, Products.isGood (π C fun x ↦ ord I x < o') l
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1, ∃ (h_1 : Products.isGood (π C fun x ↦ ord I x < a) a_1), eval (π C fun x ↦ ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = eval C ⟨l, hl✝⟩
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ E.carrier = ↑E

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ E.carrier = ↑E
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
o' : Ordinal.{u}
h : o' < o
l : Products I
hl : Products.isGood (π C fun x ↦ ord I x < o') l
⊢ Products.isGood (π C fun x ↦ ord I x < o) l

Tactic:
]

Goal state after:
case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
o' : Ordinal.{u}
h : o' < o
l : Products I
hl : Products.isGood (π C fun x ↦ ord I x < o') l
⊢ Products.isGood (π C fun x ↦ ord I x < o) l
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
E : Subcomplex C
this : ⋃ n, ⋃ j, openCell n ↑j = ↑E
⊢ ⋃ n, ⋃ j, openCell n ↑j = ↑E

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
E : Subcomplex C
this : ⋃ n, ⋃ j, openCell n ↑j = ↑E
⊢ ⋃ n, ⋃ j, openCell n ↑j = ↑E
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ ∀
    (x₂ :
      ↑{ X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
            X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho) ℤ),
            f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
                X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho) ℤ),
                f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
                  X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho) ℤ),
                  f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.f)
            x₁ =
          x₂

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ ∀
    (x₂ :
      ↑{ X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
            X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho) ℤ),
            f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
                X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho) ℤ),
                f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
                  X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho) ℤ),
                  f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.f)
            x₁ =
          x₂
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
⊢ LinearIndependent (ι := ↑(range C)) ℤ ((fun p ↦ ↑p) ∘ (range_equiv C ho hsC).toFun) ↔
    LinearIndependent ℤ fun (p : ↑(⋃ e, smaller C ↑e)) ↦ ↑p

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
⊢ LinearIndependent (ι := ↑(range C)) ℤ ((fun p ↦ ↑p) ∘ (range_equiv C ho hsC).toFun) ↔
    LinearIndependent ℤ fun (p : ↑(⋃ e, smaller C ↑e)) ↦ ↑p
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun x ↦ ord I x < o₁) l
hl' : eval (π C fun x ↦ ord I x < o₁) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o₁) '' {m | m < l})
⊢ eval (π C fun x ↦ ord I x < o₁) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o₁) '' {m | m < l})

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : isGood (π C fun x ↦ ord I x < o₁) l
hl' : eval (π C fun x ↦ ord I x < o₁) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o₁) '' {m | m < l})
⊢ eval (π C fun x ↦ ord I x < o₁) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o₁) '' {m | m < l})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
this : C = ∅ ∨ C = {fun x ↦ false}
⊢ LinearIndependent ℤ (eval C)

Tactic:
]

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
this : C = ∅ ∨ C = {fun x ↦ false}
⊢ LinearIndependent ℤ (eval C)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndepOn ℤ id (⋃ e, smaller C ↑e)

Tactic:
]

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndepOn ℤ id (⋃ e, smaller C ↑e)
Module: Mathlib.Topology.Category.Profinite.Projective

Goal state before:
pp: X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
⊢ ∃ f', f' ≫ g = f

Tactic:
]

Goal state after:
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
⊢ ∃ f', f' ≫ g = f
Module: Mathlib.Topology.Category.Profinite.Projective

Goal state before:
pp: case h
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
this : ⇑(ConcreteCategory.hom g.hom) ∘ g' = id
⊢ ⇑(ConcreteCategory.hom f) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure

Tactic:
]

Goal state after:
case h
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
this : ⇑(ConcreteCategory.hom g.hom) ∘ g' = id
⊢ ⇑(ConcreteCategory.hom f) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
⊢ D ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
⊢ D ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent ℤ (SumEval C ho')

Tactic:
]

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
μ o : Ordinal.{u}
h : P I o
ho : o + 1 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C (o + 1)
ho' : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ LinearIndependent ℤ (SumEval C ho')
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case hDA
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
this : D ⊆ E
⊢ IsClosed[t] D

Tactic:
]

Goal state after:
case hDA
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
this : D ⊆ E
⊢ IsClosed[t] D
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case h
S : Profinite
C : { C // IsClopen C }
⊢ IsLocallyConstant fun a ↦ decide (a ∈ ↑C)

Tactic:
]

Goal state after:
case h
S : Profinite
C : { C // IsClopen C }
⊢ IsLocallyConstant fun a ↦ decide (a ∈ ↑C)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
a : I
ha : a ∈ ↑l
⊢ ¬term I ho = a

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (Products.eval (π C fun x ↦ ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
a : I
ha : a ∈ ↑l
⊢ ¬term I ho = a
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case hf
S : Profinite
a b : ↑S.toTop
h : (fun C ↦ decide (a ∈ ↑C)) = fun C ↦ decide (b ∈ ↑C)
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (a ∈ ↑⟨C, hC⟩) = true

Tactic:
]

Goal state after:
case hf
S : Profinite
a b : ↑S.toTop
h : (fun C ↦ decide (a ∈ ↑C)) = fun C ↦ decide (b ∈ ↑C)
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (a ∈ ↑⟨C, hC⟩) = true