awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  MapsTo (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
h : cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j

Tactic:
use I
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  MapsTo (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' sphere 0 1 ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m j) : (Fin m → ℝ) → X) '' closedBall 0 1

Tactic:
rw [mapsTo_iff_image_subset] at hI

Premises used: Set.mapsTo_iff_image_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' sphere 0 1 ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m j) : (Fin m → ℝ) → X) '' closedBall 0 1
⊢ cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j

Tactic:
hI

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

Tactic:
exact hI
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
i : @cell _ t C ∅ _ n
rcases :
  ∀ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m))
    (hI :
      MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
        (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)),
    ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
      cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := ∅) m j
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := ∅) m j

Tactic:
rcases RelCWComplex.mapsTo n i with ⟨I, hI⟩

Premises used: Topology.RelCWComplex.mapsTo
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
i : @cell _ t C ∅ _ n
I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
hI :
  MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
h : cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := ∅) m j
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := ∅) m j

Tactic:
use I
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
i : @cell _ t C ∅ _ n
I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
hI :
  MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) '' sphere 0 1 ⊆
    ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1

Tactic:
rw [mapsTo_iff_image_subset, empty_union] at hI

Premises used: Set.mapsTo_iff_image_subset, Set.empty_union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
i : @cell _ t C ∅ _ n
I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
hI :
  (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) '' sphere 0 1 ⊆
    ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1
⊢ cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := ∅) m j

Tactic:
hI

Premises used: Topology.RelCWComplex.cellFrontier, Topology.RelCWComplex.closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
i : @cell _ t C ∅ _ n
I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
hI :
  (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) '' sphere 0 1 ⊆
    ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1
⊢ cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := ∅) m j

Tactic:
exact hI
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j = C

Tactic:
RelCWComplex.union'

Premises used: Topology.RelCWComplex.union', Topology.RelCWComplex.closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
⊢ ∅ ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C

Tactic:
have := RelCWComplex.union' (C := C)
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
this : ∅ ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C

Tactic:
rw [empty_union] at this

Premises used: Set.empty_union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
this : ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), closedCell (C := C) (D := ∅) n j = C

Tactic:
this

Premises used: Topology.RelCWComplex.closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
this : ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), closedCell (C := C) (D := ∅) n j = C

Tactic:
exact this
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ openCell (C := C) (D := D) n i ⊆ closedCell (C := C) (D := D) n i

Tactic:
image_mono Metric.ball_subset_closedBall

Premises used: Metric.ball_subset_closedBall, Set.image_mono, Topology.RelCWComplex.openCell, Topology.RelCWComplex.closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ cellFrontier (C := C) (D := D) n i ⊆ closedCell (C := C) (D := D) n i

Tactic:
image_mono Metric.sphere_subset_closedBall

Premises used: Topology.RelCWComplex.cellFrontier, Set.image_mono, Topology.RelCWComplex.closedCell, Metric.sphere_subset_closedBall
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
rw :
  (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' (sphere 0 1 ∪ ball 0 1) =
    (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' closedBall 0 1
⊢ cellFrontier (C := C) (D := D) n i ∪ openCell (C := C) (D := D) n i = closedCell (C := C) (D := D) n i

Tactic:
rw [cellFrontier, openCell, closedCell, ← image_union]

Premises used: Topology.RelCWComplex.cellFrontier, Topology.RelCWComplex.openCell, Topology.RelCWComplex.closedCell, Set.image_union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
congrm : Eq (α := Set (Fin n → ℝ)) (sphere 0 1 ∪ ball 0 1) (closedBall 0 1)
⊢ (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' (sphere 0 1 ∪ ball 0 1) =
    (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' closedBall 0 1

Tactic:
congrm map n i '' ?_

Premises used: Topology.RelCWComplex.map
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ Eq (α := Set (Fin n → ℝ)) (sphere 0 1 ∪ ball 0 1) (closedBall 0 1)

Tactic:
sphere_union_ball

Premises used: Metric.sphere_union_ball
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ Eq (α := Set (Fin n → ℝ)) (sphere 0 1 ∪ ball 0 1) (closedBall 0 1)

Tactic:
exact sphere_union_ball

Premises used: Metric.sphere_union_ball
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
h : Membership.mem (γ := Set (Fin n → ℝ)) (ball 0 1) 0
⊢ (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) 0 ∈ openCell (C := C) (D := D) n i

Tactic:
apply mem_image_of_mem

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ Membership.mem (γ := Set (Fin n → ℝ)) (ball 0 1) 0

Tactic:
simp only [mem_ball, dist_self, zero_lt_one]

Premises used: Metric.mem_ball, dist_self, zero_lt_one
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) 0 ∈ closedCell (C := C) (D := D) n i

Tactic:
openCell_subset_closedCell _ _ (map_zero_mem_openCell _ _)

Premises used: Topology.RelCWComplex.map_zero_mem_openCell, Topology.RelCWComplex.openCell_subset_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
by_contra : ∀ (hJ : i ∉ J n), False
⊢ i ∈ J n

Tactic:
by_contra hJ
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
⊢ openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)

Tactic:
have h : openCell n i ⊆ D ∪ ⋃ n, ⋃ (j : J n), openCell (C := C) n j :=
    hIJ.symm ▸ subset_union_of_subset_right
      (subset_iUnion_of_subset n (subset_iUnion_of_subset ⟨i, hi⟩ (subset_refl (openCell n i)))) D
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
h :
  openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
simp_rw :
  Disjoint (openCell (C := C) (D := D) n i) D ∧
    ∀ (i_1 : ℕ) (i_2 : (↑(J i_1) : Type u_1)),
      Disjoint (openCell (C := C) (D := D) n i) (openCell (C := C) (D := D) i_1 (↑i_2 : cell C i_1))
⊢ Disjoint (openCell (C := C) (D := D) n i)
    (D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n))

Tactic:
simp_rw [disjoint_union_right, disjoint_iUnion_right]

Premises used: Set.disjoint_union_right, Set.disjoint_iUnion_right
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
h :
  openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
m : ℕ
j : (↑(J m) : Type u_1)
⊢ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) n i ≠
    Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m (↑j : cell C m)

Tactic:
lia
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
h :
  openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
⊢ Disjoint (openCell (C := C) (D := D) n i) D ∧
    ∀ (i_1 : ℕ) (i_2 : (↑(J i_1) : Type u_1)),
      Disjoint (openCell (C := C) (D := D) n i) (openCell (C := C) (D := D) i_1 (↑i_2 : cell C i_1))

Tactic:
exact ⟨disjointBase n i, fun m j ↦ disjoint_openCell_of_ne (by lia)⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
h :
  openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
⊢ Disjoint (openCell (C := C) (D := D) n i)
    (D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n))

Tactic:
have h' : Disjoint (openCell n i) (D ∪ ⋃ n, ⋃ (j : J n), openCell (C := C) n j) := by
    simp_rw [disjoint_union_right, disjoint_iUnion_right]
    exact ⟨disjointBase n i, fun m j ↦ disjoint_openCell_of_ne (by lia)⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
h :
  openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
h' :
  Disjoint (openCell (C := C) (D := D) n i)
    (D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n))
⊢ openCell (C := C) (D := D) n i = ∅

Tactic:
rw [disjoint_of_subset_iff_left_eq_empty h] at h'

Premises used: Set.disjoint_of_subset_iff_left_eq_empty
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
h :
  openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
h' : openCell (C := C) (D := D) n i = ∅
⊢ False

Tactic:
notMem_empty _ (h' ▸ map_zero_mem_openCell n i)

Premises used: Set.notMem_empty
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
h :
  openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
h' : openCell (C := C) (D := D) n i = ∅
⊢ False

Tactic:
exact notMem_empty _ (h' ▸ map_zero_mem_openCell n i)

Premises used: Set.notMem_empty
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
h : ∀ (n : ℕ) (x : @cell _ t C D _ n), x ∈ I n ↔ x ∈ J n
⊢ I = J

Tactic:
ext n x
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
x : @cell _ t C D _ n
⊢ x ∈ I n ↔ x ∈ J n

Tactic:
⟨fun h ↦ subset_of_eq_union_iUnion I J hIJ n h,
    fun h ↦ subset_of_eq_union_iUnion J I hIJ.symm n h⟩

Premises used: _private.0.Topology.RelCWComplex.subset_of_eq_union_iUnion, Iff.intro, Eq.symm
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
x : @cell _ t C D _ n
⊢ x ∈ I n ↔ x ∈ J n

Tactic:
exact ⟨fun h ↦ subset_of_eq_union_iUnion I J hIJ n h,
    fun h ↦ subset_of_eq_union_iUnion J I hIJ.symm n h⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
I J : (n : ℕ) → Set (@cell _ t C ∅ _ n)
hIJ :
  Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
    (⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
hIJ₁ :
  Eq.{u_1 + 1} (α := Set X) (∅ ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
    (∅ ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
⊢ I = J

Tactic:
apply RelCWComplex.eq_of_eq_union_iUnion

Premises used: Topology.RelCWComplex.eq_of_eq_union_iUnion
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
I J : (n : ℕ) → Set (@cell _ t C ∅ _ n)
hIJ hIJ₁ :
  Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
    (⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
⊢ Eq.{u_1 + 1} (α := Set X) (∅ ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
    (∅ ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))

Tactic:
simp_rw [empty_union, hIJ]

Premises used: Set.empty_union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ IsCompact (closedCell (C := C) (D := D) n i)

Tactic:
(isCompact_closedBall _ _).image_of_continuousOn (continuousOn n i)

Premises used: Topology.RelCWComplex.continuousOn, Topology.RelCWComplex.closedCell, IsCompact.image_of_continuousOn, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
n : ℕ
i : @cell _ t C D _ n
⊢ IsClosed[t] (closedCell (C := C) (D := D) n i)

Tactic:
isCompact_closedCell.isClosed

Premises used: Topology.RelCWComplex.isCompact_closedCell, IsCompact.isClosed
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ IsCompact (cellFrontier (C := C) (D := D) n i)

Tactic:
(isCompact_sphere _ _).image_of_continuousOn ((continuousOn n i).mono sphere_subset_closedBall)

Premises used: Topology.RelCWComplex.continuousOn, Topology.RelCWComplex.cellFrontier, isCompact_sphere, IsCompact.image_of_continuousOn, ContinuousOn.mono, Metric.sphere_subset_closedBall
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
n : ℕ
i : @cell _ t C D _ n
⊢ IsClosed[t] (cellFrontier (C := C) (D := D) n i)

Tactic:
isCompact_cellFrontier.isClosed

Premises used: Topology.RelCWComplex.isCompact_cellFrontier, IsCompact.isClosed
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
apply : closedCell (C := C) (D := D) n j ⊆ closure[t] (openCell (C := C) (D := D) n j)
⊢ closure[t] (openCell (C := C) (D := D) n j) = closedCell (C := C) (D := D) n j

Tactic:
apply subset_antisymm (isClosed_closedCell.closure_subset_iff.2 (openCell_subset_closedCell n j))

Premises used: Iff.mpr, subset_antisymm, Topology.RelCWComplex.isClosed_closedCell, IsClosed.closure_subset_iff, Topology.RelCWComplex.openCell_subset_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
⊢ Ne (α := ℝ) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
⊢ Ne (α := ℝ) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
rw :
  (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) '' closure (ball 0 1) ⊆ closure[t] (openCell (C := C) (D := D) n j)
⊢ closedCell (C := C) (D := D) n j ⊆ closure[t] (openCell (C := C) (D := D) n j)

Tactic:
rw [closedCell, ← closure_ball 0 (by exact one_ne_zero)]

Premises used: Topology.RelCWComplex.closedCell, closure_ball, OfNat.ofNat