awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
hDA : IsClosed[t] (E ∩ D)
h :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
⊢ IsClosed[t] E

Tactic:
apply isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell hEC

Premises used: Topology.RelCWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
rw : D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
⊢ D ⊆ E

Tactic:
rw [← union]
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
⊢ D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)

Tactic:
subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
⊢ D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)

Tactic:
exact subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
⊢ D ⊆ E

Tactic:
have : D ⊆ E := by
        rw [← union]
        exact subset_union_left
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
this : D ⊆ E
hDA : IsClosed[t] D
⊢ IsClosed[t] (E ∩ D)

Tactic:
rw [inter_eq_right.2 this]

Premises used: Iff.mpr, Set.inter_eq_right
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
this : D ⊆ E
⊢ IsClosed[t] D

Tactic:
isClosedBase C

Premises used: Topology.RelCWComplex.isClosedBase
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
this : D ⊆ E
⊢ IsClosed[t] D

Tactic:
exact isClosedBase C

Premises used: Topology.RelCWComplex.isClosedBase
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h :
  0 < n →
    ∀ (j : @cell _ t C D _ n),
      Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
⊢ 0 < n →
    ∀ (j : @cell _ t C D _ n),
      Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)

Tactic:
_
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h : 0 < n
j : @cell _ t C D _ n
pos : ∀ (h : j ∈ I n), Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
neg : ∀ (h : j ∉ I n), Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
⊢ Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)

Tactic:
by_cases h : j ∈ I n
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∈ I n
pos : IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
⊢ Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)

Tactic:
right
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∈ I n
this : closedCell (C := C) (D := D) n j ⊆ E
rw : IsClosed[t] (closedCell (C := C) (D := D) n j)
⊢ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)

Tactic:
rw [inter_eq_right.2 this]

Premises used: Iff.mpr, Set.inter_eq_right
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∈ I n
this : closedCell (C := C) (D := D) n j ⊆ E
⊢ IsClosed[t] (closedCell (C := C) (D := D) n j)

Tactic:
isClosed_closedCell

Premises used: Topology.RelCWComplex.isClosed_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∈ I n
this : closedCell (C := C) (D := D) n j ⊆ E
⊢ IsClosed[t] (closedCell (C := C) (D := D) n j)

Tactic:
exact isClosed_closedCell

Premises used: Topology.RelCWComplex.isClosed_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∈ I n
pos : closedCell (C := C) (D := D) n j ⊆ E
⊢ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)

Tactic:
suffices closedCell n j ⊆ E by
        rw [inter_eq_right.2 this]
        exact isClosed_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∈ I n
⊢ closedCell (C := C) (D := D) n j ⊆ E

Tactic:
closedCell_subset n ⟨j, h⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∈ I n
⊢ closedCell (C := C) (D := D) n j ⊆ E

Tactic:
exact closedCell_subset n ⟨j, h⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∉ I n
neg : Disjoint E (openCell (C := C) (D := D) n j)
⊢ Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)

Tactic:
left
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∉ I n
neg :
  Disjoint D (openCell (C := C) (D := D) n j) ∧
    ∀ (i : ℕ) (i_1 : (↑(I i) : Type u_1)),
      Disjoint (openCell (C := C) (D := D) i (↑i_1 : cell C i)) (openCell (C := C) (D := D) n j)
⊢ Disjoint E (openCell (C := C) (D := D) n j)

Tactic:
simp_rw [← union, disjoint_union_left, disjoint_iUnion_left]

Premises used: Set.disjoint_iUnion_left, Set.disjoint_union_left
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∉ I n
x : ℕ
x_1 : (↑(I x) : Type u_1)
⊢ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) x (↑x_1 : cell C x) ≠
    Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) n j

Tactic:
aesop
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∉ I n
⊢ Disjoint D (openCell (C := C) (D := D) n j) ∧
    ∀ (i : ℕ) (i_1 : (↑(I i) : Type u_1)),
      Disjoint (openCell (C := C) (D := D) i (↑i_1 : cell C i)) (openCell (C := C) (D := D) n j)

Tactic:
exact ⟨disjointBase n j |>.symm, fun _ _ ↦ disjoint_openCell_of_ne (by aesop)⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D : Set X
inst : T2Space X
C : Set X
inst_1 : CWComplex C
E : Set X
I : (n : ℕ) → Set (@cell _ t C ∅ _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := ∅) n (↑i : cell C n) ⊆ E
union rw : ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E
⊢ ∅ ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E

Tactic:
rw [empty_union]

Premises used: Set.empty_union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D : Set X
inst : T2Space X
C : Set X
inst_1 : CWComplex C
E : Set X
I : (n : ℕ) → Set (@cell _ t C ∅ _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := ∅) n (↑i : cell C n) ⊆ E
union : ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E
⊢ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E

Tactic:
union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D : Set X
inst : T2Space X
C : Set X
inst_1 : CWComplex C
E : Set X
I : (n : ℕ) → Set (@cell _ t C ∅ _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := ∅) n (↑i : cell C n) ⊆ E
union : ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E
⊢ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E

Tactic:
exact union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D : Set X
inst : T2Space X
C : Set X
h : CWComplex C
E : Set X
I : (n : ℕ) → Set (@cell _ t C ∅ _ n)
inst_1 : CWComplex E
union rw : ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E
⊢ ∅ ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E

Tactic:
rw [empty_union]

Premises used: Set.empty_union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D : Set X
inst : T2Space X
C : Set X
h : CWComplex C
E : Set X
I : (n : ℕ) → Set (@cell _ t C ∅ _ n)
inst_1 : CWComplex E
union : ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E
⊢ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E

Tactic:
union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D : Set X
inst : T2Space X
C : Set X
h : CWComplex C
E : Set X
I : (n : ℕ) → Set (@cell _ t C ∅ _ n)
inst_1 : CWComplex E
union : ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E
⊢ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) = E

Tactic:
exact union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
simp_rw :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j
⊢ (↑E : Set X) ⊆ C

Tactic:
simp_rw [← union, ← RelCWComplex.union_iUnion_openCell_eq_complex]

Premises used: Topology.RelCWComplex.Subcomplex.union, Topology.RelCWComplex.union_iUnion_openCell_eq_complex
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j

Tactic:
union_subset_union_right _ (iUnion_mono fun _ ↦ iUnion_mono' fun j ↦ ⟨j, subset_rfl⟩)

Premises used: Set.union_subset_union_right, Set.iUnion_mono', Exists.intro, Set.iUnion_mono, Subtype.val, subset_rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j

Tactic:
exact union_subset_union_right _ (iUnion_mono fun _ ↦ iUnion_mono' fun j ↦ ⟨j, subset_rfl⟩)

Premises used: Set.union_subset_union_right, Set.iUnion_mono', Exists.intro, Set.iUnion_mono, subset_rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
simp_rw :
  D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
⊢ D ⊆ (↑E : Set X)

Tactic:
simp_rw [← union]

Premises used: Topology.RelCWComplex.Subcomplex.union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
⊢ D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)

Tactic:
subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
⊢ D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)

Tactic:
exact subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
n : ℕ∞
l : ℕ
this :
  ∀ (i : @cell _ t C D _ l)
    (hi :
      Membership.mem (γ := Set (@cell _ t C D _ l))
        ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) i),
    closedCell (C := C) (D := D) l
        (↑(Subtype.mk (p := fun (x : @cell _ t C D _ l) ↦
              Membership.mem (γ := Set (@cell _ t C D _ l))
                ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) x)
              i hi) :
          cell C l) ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ ∀ (i : (↑((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) : Type u_1)),
    closedCell (C := C) (D := D) l (↑i : cell C l) ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
⟨i, hi⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
n : ℕ∞
l : ℕ
i : @cell _ t C D _ l
hi :
  Membership.mem (γ := Set (@cell _ t C D _ l))
    ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) i
h :
  closedCell (C := C) (D := D) l
      (↑(Subtype.mk (p := fun (x : @cell _ t C D _ l) ↦
            Membership.mem (γ := Set (@cell _ t C D _ l))
              ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) x)
            i hi) :
        cell C l) ⊆
    ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ closedCell (C := C) (D := D) l
      (↑(Subtype.mk (p := fun (x : @cell _ t C D _ l) ↦
            Membership.mem (γ := Set (@cell _ t C D _ l))
              ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) x)
            i hi) :
        cell C l) ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
apply subset_union_of_subset_right

Premises used: Set.subset_union_of_subset_right
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
n : ℕ∞
l : ℕ
i : @cell _ t C D _ l
hi :
  Membership.mem (γ := Set (@cell _ t C D _ l))
    ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) i
h :
  closedCell (C := C) (D := D) l
      (↑(Subtype.mk (p := fun (x : @cell _ t C D _ l) ↦
            Membership.mem (γ := Set (@cell _ t C D _ l))
              ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) x)
            i hi) :
        cell C l) ⊆
    ⋃ (j : @cell _ t C D _ l), closedCell (C := C) (D := D) l j
⊢ closedCell (C := C) (D := D) l
      (↑(Subtype.mk (p := fun (x : @cell _ t C D _ l) ↦
            Membership.mem (γ := Set (@cell _ t C D _ l))
              ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) x)
            i hi) :
        cell C l) ⊆
    ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
apply subset_iUnion₂_of_subset l hi

Premises used: Set.subset_iUnion₂_of_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
n : ℕ∞
l : ℕ
i : @cell _ t C D _ l
hi :
  Membership.mem (γ := Set (@cell _ t C D _ l))
    ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) i
⊢ closedCell (C := C) (D := D) l
      (↑(Subtype.mk (p := fun (x : @cell _ t C D _ l) ↦
            Membership.mem (γ := Set (@cell _ t C D _ l))
              ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) x)
            i hi) :
        cell C l) ⊆
    ⋃ (j : @cell _ t C D _ l), closedCell (C := C) (D := D) l j

Tactic:
subset_iUnion _ _

Premises used: Set.subset_iUnion