mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type u_1
t₁ t₂ : TopologicalSpace Y
h₁ : IsGeneratedBy X Y
h₂ : IsGeneratedBy X Y
⊢ IsGeneratedBy X Y

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type u_1
t₁ t₂ : TopologicalSpace Y
h₁ : IsGeneratedBy X Y
h₂ : IsGeneratedBy X Y
⊢ IsGeneratedBy X Y
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case h
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this✝ : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G).sets
this : Ultrafilter.map X.str G = F
⊢ X.join G ∈ basic A ∧ X.str F = X.str F

Tactic:
]

Goal state after:
case h
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
this✝ : ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
G : Ultrafilter (Ultrafilter X.A)
h1 : C1 ⊆ (↑G).sets
this : Ultrafilter.map X.str G = F
⊢ X.join G ∈ basic A ∧ X.str F = X.str F
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
⊢ ∀ (F : Ultrafilter X.A), cl A ∈ F → X.str F ∈ cl A

Tactic:
]

Goal state after:
X : Compactum
A : Set X.A
⊢ ∀ (F : Ultrafilter X.A), cl A ∈ F → X.str F ∈ cl A
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ∀ (s : Set X.A), x ∈ s → IsOpen s → s ∈ ↑F
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : x ∉ A
⊢ False

Tactic:
]

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ∀ (s : Set X.A), x ∈ s → IsOpen s → s ∈ ↑F
A : Set X.A
hA : IsClosed A
h : A ∈ F
H : x ∉ A
⊢ False
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
A : Set X.A
cond : A ∉ F
hA : IsClosed A
h : A ∈ F
H : x ∉ A
⊢ False

Tactic:
]

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
A : Set X.A
cond : A ∉ F
hA : IsClosed A
h : A ∈ F
H : x ∉ A
⊢ False
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
h : ∀ (i : ι), J i → K i
x✝ : (i : ↑K) → X ↑i
y : (i : ι) → X i
hy : y ∈ C ∧ (precomp Subtype.val) y = x✝
⊢ (precomp (Set.inclusion h)) ((precomp Subtype.val) y) ∈ obj C J

Tactic:
]

Goal state after:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
h : ∀ (i : ι), J i → K i
x✝ : (i : ↑K) → X ↑i
y : (i : ι) → X i
hy : y ∈ C ∧ (precomp Subtype.val) y = x✝
⊢ (precomp (Set.inclusion h)) ((precomp Subtype.val) y) ∈ obj C J
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : ↑((π_app C fun x ↦ x ∈ {i}) a) = ↑((π_app C fun x ↦ x ∈ {i}) b)
⊢ ↑a i = ↑b i

Tactic:
]

Goal state after:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : ↑((π_app C fun x ↦ x ∈ {i}) a) = ↑((π_app C fun x ↦ x ∈ {i}) b)
⊢ ↑a i = ↑b i
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
J : (Finset ι)ᵒᵖ
⊢ IsCompact (obj C fun x ↦ x ∈ unop J)

Tactic:
]

Goal state after:
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
J : (Finset ι)ᵒᵖ
⊢ IsCompact (obj C fun x ↦ x ∈ unop J)
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
⊢ IsCompact C

Tactic:
]

Goal state after:
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
⊢ IsCompact C
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
]

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
]

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : ↑(map n i) '' sphere 0 1 ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1
⊢ cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
this : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ⋃ n, ⋃ j, closedCell n j = C

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
this : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
⊢ ⋃ n, ⋃ j, closedCell n j = C
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
x : ↑C
hx : (π_app C fun x ↦ x ∈ K) x ∈ {↑a (op K)}
⊢ (map C h) (↑a (op K)) ∈
    {(ConcreteCategory.hom (((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).map (homOfLE h).op)) (↑a (op K))}

Tactic:
]

Goal state after:
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
x : ↑C
hx : (π_app C fun x ↦ x ∈ K) x ∈ {↑a (op K)}
⊢ (map C h) (↑a (op K)) ∈
    {(ConcreteCategory.hom (((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).map (homOfLE h).op)) (↑a (op K))}
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
n : ℕ
i : cell C n
⊢ ↑(map n i) '' (sphere 0 1 ∪ ball 0 1) = ↑(map n i) '' closedBall 0 1

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C n
⊢ ↑(map n i) '' (sphere 0 1 ∪ ball 0 1) = ↑(map n i) '' closedBall 0 1
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ
a✝ : f ∈ ⊤
⊢ ∃ c, (c.sum fun i a ↦ a • spanFinBasis C s i) = f

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ
a✝ : f ∈ ⊤
⊢ ∃ c, (c.sum fun i a ↦ a • spanFinBasis C s i) = f
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u_1
C : Set (I → Bool)
x : ↑C
l : List (LocallyConstant ↑C ℤ)
⊢ l.prod x = l.prod x

Tactic:
]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom y)) (factors C s x)).prod = 1

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom y)) (factors C s x)).prod = 1
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
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
hJ : i ∉ J n
h : openCell n i ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
h' : openCell n i = ∅
⊢ False

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
hi : i ∈ I n
hJ : i ∉ J n
h : openCell n i ⊆ D ∪ ⋃ n, ⋃ j, openCell n ↑j
h' : openCell n i = ∅
⊢ False
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ↑x b = true
⊢ 1 = 1

Tactic:
]

Goal state after:
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
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ↑(map n j) '' closure (ball 0 1) ⊆ closure[t] (openCell n j)

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ↑(map n j) '' closure (ball 0 1) ⊆ closure[t] (openCell n j)
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
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ContinuousOn (↑(map n j)) (closedBall 0 1)

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ContinuousOn (↑(map n j)) (closedBall 0 1)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ¬↑x b = true
⊢ LocallyConstant.toFun 1 x - 0 = 1

Tactic:
]

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ¬↑x b = true
⊢ LocallyConstant.toFun 1 x - 0 = 1
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : ↑(map 0 x) ![] = ↑(map 0 y) ![]
⊢ x = y

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x y : cell C 0
h : ↑(map 0 x) ![] = ↑(map 0 y) ![]
⊢ x = y
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom y)) (factors C s x)).prod = 0

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom y)) (factors C s x)).prod = 0
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 : cell C 1
⊢ ↑(map 1 e) '' sphere 0 1 = ↑(map 1 e) '' {-1, 1}

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
⊢ ↑(map 1 e) '' sphere 0 1 = ↑(map 1 e) '' {-1, 1}
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Tactic:
]

Goal state after:
case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case e_s
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
f : Fin 1 → ℝ
⊢ const (Fin 1) (f default) 0 = 1 ∨ const (Fin 1) (f default) 0 = -1 ↔
    const (Fin 1) (f default) 0 = (-1) 0 ∨ const (Fin 1) (f default) = 1

Tactic:
]

Goal state after:
case e_s
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
f : Fin 1 → ℝ
⊢ const (Fin 1) (f default) 0 = 1 ∨ const (Fin 1) (f default) 0 = -1 ↔
    const (Fin 1) (f default) 0 = (-1) 0 ∨ const (Fin 1) (f default) = 1
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 : cell C 1
⊢ cellFrontier 1 e = ↑(map 1 e) '' {-1, 1}

Tactic:
rw [cellFrontier]
  congr 1
  ext f
  simp only [mem_sphere_iff_norm, sub_zero, Pi.norm_def, Finset.univ_unique, Fin.default_eq_zero,
    Fin.isValue, Finset.sup_singleton, coe_nnnorm, Real.norm_eq_abs, abs_eq (zero_le_one' ℝ),
    mem_insert_iff, mem_singleton_iff]
  rw [eq_const_of_unique (f := f), ← funext_iff_of_subsingleton (x := 0) (y := 0)]
  simp [const_apply, or_comm]

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

Goal state before:
pp: case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ true
hx : ↑x a = true
⊢ (LocallyConstant.evalMonoidHom y) (e (π C fun x ↦ x ∈ s) a) = 0

Tactic:
]

Goal state after:
case true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ true
hx : ↑x a = true
⊢ (LocallyConstant.evalMonoidHom y) (e (π C fun x ↦ x ∈ s) a) = 0
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ (∀ (n : ℕ) (j : cell C n), IsClosed[t] (C ∩ closedCell n j)) ∧ IsClosed[t] (C ∩ D)

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ (∀ (n : ℕ) (j : cell C n), IsClosed[t] (C ∩ closedCell n j)) ∧ IsClosed[t] (C ∩ D)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ true
hx : ↑x a = true
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case left
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n✝ : ℕ
j✝ : cell C n✝
⊢ IsClosed[t] (closedCell n✝ j✝)

Tactic:
]

Goal state after:
case left
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n✝ : ℕ
j✝ : cell C n✝
⊢ IsClosed[t] (closedCell n✝ j✝)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case left
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n✝ : ℕ
j✝ : cell C n✝
⊢ IsClosed[t] (C ∩ closedCell n✝ j✝)

Tactic:
rw [inter_eq_right.2 (closedCell_subset_complex _ _)]

Goal state after:
case left
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n✝ : ℕ
j✝ : cell C n✝
⊢ IsClosed[t] (closedCell n✝ j✝)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case right
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ IsClosed[t] D

Tactic:
]

Goal state after:
case right
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ IsClosed[t] D
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c • x = c • (e (π C fun x ↦ x ∈ s) a * x)
⊢ c m • (e (π C fun x ↦ x ∈ s) a * Products.eval (π C fun x ↦ x ∈ s) m) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c • x = c • (e (π C fun x ↦ x ∈ s) a * x)
⊢ c m • (e (π C fun x ↦ x ∈ s) a * Products.eval (π C fun x ↦ x ∈ s) m) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : ↑m < n
j : cell C m
⊢ cellFrontier m j ∪ openCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
]

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : ↑m < n
j : cell C m
⊢ cellFrontier m j ∪ openCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s)))

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s)))
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
⊢ false ≠ x i → J i

Tactic:
simpa only [ne_comm] using h i

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ Set.range (spanFinBasis C s) ⊆ ↑(Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s))))

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ Set.range (spanFinBasis C s) ⊆ ↑(Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s))))
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
n : ℕ∞
m : ℕ
hm' : ∀ m_1 ≤ m, ↑m_1 < n → ∀ (j : cell C m_1), cellFrontier m_1 j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
hm : ↑(m + 1) < n
j : cell C (m + 1)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (m + 1) j ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell m_1 j
l : ℕ
hl : l < m + 1
i : cell C l
x✝ : i ∈ I l
⊢ cellFrontier l i ∪ openCell l i ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' : ∀ m_1 ≤ m, ↑m_1 < n → ∀ (j : cell C m_1), cellFrontier m_1 j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
hm : ↑(m + 1) < n
j : cell C (m + 1)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (m + 1) j ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell m_1 j
l : ℕ
hl : l < m + 1
i : cell C l
x✝ : i ∈ I l
⊢ cellFrontier l i ∪ openCell l i ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
⊢ (factors C s x).prod ∈ ↑(Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s))))

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
⊢ (factors C s x).prod ∈ ↑(Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s))))