mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ IsClosed[t] E

Tactic:
by

Goal state after:
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
⊢ Set.range (eval C) = Set.range (Sum.elim (fun l ↦ Products.eval C ↑l) fun l ↦ Products.eval C ↑l)

Tactic:
by

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✝¹ : T2Space X
C : Set X
inst✝ : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ∅ ∪ ⋃ n, ⋃ j, openCell n ↑j = E

Tactic:
by

Goal state after:
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}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ SumEval C ho ∘ Sum.inl = ⇑(ConcreteCategory.hom (ModuleCat.ofHom (πs C o))) ∘ eval (π C fun x ↦ ord I x < o)

Tactic:
by

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

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
⊢ SwapTrue o x (term I ho) = true

Tactic:
by

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✝¹ : T2Space X
C : Set X
h : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
inst✝ : CWComplex E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ∅ ∪ ⋃ n, ⋃ j, openCell n ↑j = E

Tactic:
by

Goal state after:
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}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ ∀ x ∈ C' C ho, x (term I ho) = false

Tactic:
by

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
E : Subcomplex C
⊢ ↑E ⊆ C

Tactic:
by

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

Goal state before:
pp: I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
⊢ ↑l = term I ho :: ↑l.Tail

Tactic:
by

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
E : Subcomplex C
⊢ D ⊆ ↑E

Tactic:
by

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

Goal state before:
pp: I : Type u
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
⊢ l = ⟨term I ho :: ↑l.Tail, hlc⟩

Tactic:
by

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✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ ∀ (n_1 : ℕ) (i : ↑{x | ↑n_1 < n}), closedCell n_1 ↑i ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
by

Goal state after:
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
inst✝ : Inhabited I
l : ↑(MaxProducts C ho)
hm : term I ho ∈ ↑↑l
this : ord I (↑↑l).head! ≤ o
⊢ ord I (term I ho) ≤ ord I (↑↑l).head!

Tactic:
by

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✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ D ∪ ⋃ n_1, ⋃ j, openCell n_1 ↑j = D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ ↑(skeletonLT C 0) = D

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ ↑(skeletonLT C ⊤) = C

Tactic:
by

Goal state after:
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
inst✝ : Inhabited I
l : ↑(MaxProducts C ho)
⊢ (↑↑l).head! = term I ho

Tactic:
by

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

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
C : Set (I → Bool)
l : List I
a : I
hla : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: l)
⊢ eval C ⟨a :: l, hla⟩ = e C a * eval C ⟨l, ⋯⟩

Tactic:
by

Goal state after:
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
⊢ ↑(skeletonLT C m) ⊆ ↑(skeletonLT C n)

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
⊢ m + 1 ≤ n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: ⊢ ∀ {X Y : UniformSpaceCat} (f : X.Hom Y), { hom' := ⟨↑f.hom' ∘ ↑{ hom' := ⟨id, ⋯⟩ }.hom', ⋯⟩ } = f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: ⊢ ∀ {X Y : UniformSpaceCat} (f : X.Hom Y), { hom' := ⟨↑{ hom' := ⟨id, ⋯⟩ }.hom' ∘ ↑f.hom', ⋯⟩ } = f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: ⊢ ∀ {W X Y Z : UniformSpaceCat} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z),
    { hom' := ⟨↑h.hom' ∘ ↑{ hom' := ⟨↑g.hom' ∘ ↑f.hom', ⋯⟩ }.hom', ⋯⟩ } =
      { hom' := ⟨↑{ hom' := ⟨↑h.hom' ∘ ↑g.hom', ⋯⟩ }.hom' ∘ ↑f.hom', ⋯⟩ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: x✝ : UniformSpaceCat
⊢ ⇑(ConcreteCategory.hom (ConcreteCategory.ofHom ⟨Completion.map ⇑(𝟙 x✝).hom', ⋯⟩).hom) =
    ⇑(ConcreteCategory.hom (𝟙 (CpltSepUniformSpace.of (Completion x✝.carrier))).hom)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X✝ Y✝ Z✝ : UniformSpaceCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ⇑(ConcreteCategory.hom (ConcreteCategory.ofHom ⟨Completion.map ⇑(f ≫ g).hom', ⋯⟩).hom) =
    ⇑(ConcreteCategory.hom
        (ConcreteCategory.ofHom ⟨Completion.map ⇑f.hom', ⋯⟩ ≫ ConcreteCategory.ofHom ⟨Completion.map ⇑g.hom', ⋯⟩).hom)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
⊢ (extensionHom (X.completionHom ≫ f)).hom = f

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ ↑n < ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X : UniformSpaceCat
Y : CpltSepUniformSpace
f : completionFunctor.obj X ⟶ Y
⊢ ((fun f ↦ extensionHom f) ((fun f ↦ X.completionHom ≫ f.hom) f)).hom = f.hom

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ closedCell n j ⊆ ↑(skeletonLT C (↑n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ (fun f ↦ X.completionHom ≫ f.hom) ((fun f ↦ extensionHom f) f) = f

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j✝ : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j✝ ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
i : ℕ
iltn : i < n
j : cell C i
left✝ : j ∈ I i
xmem : x ∈ closedCell i j
⊢ ↑i < ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ { toFun := fun f ↦ X'.completionHom ≫ f.hom, invFun := fun f ↦ extensionHom f, left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    completionFunctor.map f ≫
      { toFun := fun f ↦ X.completionHom ≫ f.hom, invFun := fun f ↦ extensionHom f, left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ cellFrontier n j ⊆ ↑(skeletonLT C ↑n)

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
⊢ ↑(skeletonLT C ↑n) ∪ ⋃ j, closedCell n j = ↑(skeletonLT C (↑n + 1))

Tactic:
by

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
⊢ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j = ↑(skeletonLT C n)

Tactic:
by

Goal state after:
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
⊢ ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ ⋃ n, ↑(skeletonLT C ↑n) = C

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ ⋃ n, ↑(skeleton C ↑n) = C

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
x : X
⊢ x ∈ skeletonLT C n ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m < n), ∃ j, x ∈ openCell m j

Tactic:
by

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
x : X
⊢ x ∈ skeletonLT C n ↔ ∃ m, ∃ (_ : ↑m < n), ∃ j, x ∈ openCell m j

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
x : X
this : ∀ (m : ℕ), ↑m < n + 1 ↔ ↑m ≤ n
⊢ (x ∈ D ∨ ∃ m, ∃ (_ : ↑m < n + 1), ∃ j, x ∈ openCell m j) ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j

Tactic:
by

Goal state after:
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
⊢ (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
x : X
⊢ x ∈ skeleton C n ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j

Tactic:
by

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
x : X
⊢ x ∈ skeleton C n ↔ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ openCell m j

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ Disjoint (↑(skeletonLT C n)) (openCell m j)

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ ↑(skeletonLT C n) ∩ cellFrontier m j ⊆ ↑(skeletonLT C n) ∩ cellFrontier m j

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ ↑(skeletonLT C n) ∩ closedCell m j = ↑(skeletonLT C n) ∩ cellFrontier m j

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
⊢ IsCompactSystem S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
hp : IsCompactSystem S
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ (⋂ i, C i).Nonempty

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmemcell : x ∈ openCell n j
xmemD : x ∈ interior D
this : x ∈ ↑(skeletonLT C 0) ∩ openCell n j
⊢ False

Tactic:
by

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✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ Disjoint (interior D) (closedCell n j)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case pos
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : ⋂ i, s i = ∅
g : ∃ n, s n = ∅
⊢ ∃ n, dissipate s n = ∅

Tactic:
use g.choose

Goal state after:
case h
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : ⋂ i, s i = ∅
g : ∃ n, s n = ∅
⊢ dissipate s g.choose = ∅
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
⊢ Disjoint (interior D) (⋃ n, ⋃ j, closedCell n j)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
i :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
⊢ (match 0, i with
      | 0, i => PartialEquiv.single ![] ↑i
      | n.succ, i => PEmpty.elim i).source =
    ball 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
⊢ IsCompactSystem (insert ∅ S)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
⊢ ∀ (i : ℕ), s' i ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
⊢ ⋂ i, s i = ⋂ i, s' i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
j : ℕ
hj : dissipate s' j = ∅
v : ℕ
hv : n ≤ v
⊢ dissipate s v = dissipate s' v

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
j : ℕ
hj : dissipate s' j = ∅
h₃ : ∀ (v : ℕ), n ≤ v → dissipate s v = dissipate s' v
⊢ dissipate s' (max j n) = ∅

Tactic:
by

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ univ.PairwiseDisjoint fun ni ↦
    ↑(match ni.fst, ni.snd with
        | 0, i => PartialEquiv.single ![] ↑i
        | n.succ, i => PEmpty.elim i) ''
      ball 0 1

Tactic:
by

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
i :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
⊢ ∃ I,
    MapsTo
      (↑(match 0, i with
        | 0, i => PartialEquiv.single ![] ↑i
        | n.succ, i => PEmpty.elim i))
      (sphere 0 1)
      (⋃ m,
        ⋃ (_ : m < 0),
          ⋃ j ∈ I m,
            ↑(match m, j with
                | 0, i => PartialEquiv.single ![] ↑i
                | n.succ, i => PEmpty.elim i) ''
              closedBall 0 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
⊢ IsCompactSystem (insert Set.univ S)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
⊢ ∀
    (j :
      match n with
      | 0 => ↑D
      | n.succ => PEmpty.{u_1 + 1}),
    ↑(match n, j with
          | 0, i => PartialEquiv.single ![] ↑i
          | n.succ, i => PEmpty.elim i) ''
        closedBall 0 1 ⊆
      D

Tactic:
by

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ ⋃ n,
      ⋃ j,
        ↑(match n, j with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => PEmpty.elim i) ''
          closedBall 0 1 =
    D

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k ⊆ ∅
x : α
⊢ x ∈ ⋂ y, ⋂ (_ : y ≤ n), C y → x ∈ ⋂ k, ⋂ (_ : k < n), C k

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ IsCompactSystem S ↔
    ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : IsCompactSystem (insert ∅ S)
C : ℕ → Set α
hdi : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
hi : ∀ (i : ℕ), C i ∈ S
⊢ ∀ (i : ℕ), C i ∈ insert ∅ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Sphere

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
⊢ 0 < Fintype.card ι

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Sphere

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
⊢ ‖v‖ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Sphere

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
contra : v = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Sphere

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
hv₀ : v ≠ 0
⊢ finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1

Tactic:
by

Goal state after: