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 : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
⊢ 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 D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
right : IsClosed[t] D
⊢ IsClosed[t] (C ∩ D)

Tactic:
rw [inter_eq_right.2 base_subset_complex]

Premises used: Iff.mpr, Set.inter_eq_right, Topology.RelCWComplex.base_subset_complex
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
⊢ 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 D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
⊢ 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 D : Set X
inst : RelCWComplex C D
n : ℕ∞
a :
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
a₁ :
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j =
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
a : D ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
a₁ :
  ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
apply union_subset

Premises used: Set.union_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
⊢ D ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

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
n : ℕ∞
⊢ D ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

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 D : Set X
inst : RelCWComplex C D
n : ℕ∞
apply :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) < n) (j : @cell _ t C D _ m),
    openCell (C := C) (D := D) m j ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
apply iUnion₂_subset fun m hm ↦ iUnion_subset fun j ↦ ?_

Premises used: Set.iUnion₂_subset, Set.iUnion_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
h :
  openCell (C := C) (D := D) m j ⊆
    ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ openCell (C := C) (D := D) m j ⊆
    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 D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
h : openCell (C := C) (D := D) m j ⊆ ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ openCell (C := C) (D := D) m j ⊆
    ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
apply subset_iUnion₂_of_subset m hm

Premises used: Set.subset_iUnion₂_of_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
h : openCell (C := C) (D := D) m j ⊆ closedCell (C := C) (D := D) m j
⊢ openCell (C := C) (D := D) m j ⊆ ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
apply subset_iUnion_of_subset j

Premises used: Set.subset_iUnion_of_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
⊢ openCell (C := C) (D := D) m j ⊆ closedCell (C := C) (D := D) m j

Tactic:
openCell_subset_closedCell m j

Premises used: 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
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
⊢ openCell (C := C) (D := D) m j ⊆ closedCell (C := C) (D := D) m j

Tactic:
exact openCell_subset_closedCell m j

Premises used: 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
n : ℕ∞
a :
  ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
apply union_subset subset_union_left

Premises used: Set.union_subset, 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
n : ℕ∞
⊢ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
iUnion₂_subset fun m hm ↦ iUnion_subset fun j ↦ ?_

Premises used: Set.iUnion₂_subset, Set.iUnion_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
a :
  ∀ (m : ℕ) (hm : (↑m : ℕ∞) < n) (j : @cell _ t C D _ m),
    closedCell (C := C) (D := D) m j ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
refine iUnion₂_subset fun m hm ↦ iUnion_subset fun j ↦ ?_

Premises used: Set.iUnion₂_subset, Set.iUnion_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
a :
  cellFrontier (C := C) (D := D) m j ∪ openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ closedCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
rw [← cellFrontier_union_openCell_eq_closedCell]

Premises used: Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
a :
  cellFrontier (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
a₁ :
  openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ cellFrontier (C := C) (D := D) m j ∪ openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
apply union_subset

Premises used: Set.union_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
hm : (↑0 : ℕ∞) < n
j : @cell _ t C D _ 0
⊢ cellFrontier (C := C) (D := D) 0 j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
simp [cellFrontier_zero_eq_empty]

Premises used: Topology.RelCWComplex.cellFrontier_zero_eq_empty
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
a :
  ∀ (I : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hI :
      cellFrontier (C := C) (D := D) (m + 1) j ⊆
        D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j),
    cellFrontier (C := C) (D := D) (m + 1) j ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (m + 1) j

Premises used: Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
a :
  D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
apply hI.trans

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
a :
  ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
apply union_subset subset_union_left

Premises used: Set.union_subset, 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
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
apply :
  ∀ (l : ℕ) (hl : l < m + 1),
    ∀ i ∈ I l,
      closedCell (C := C) (D := D) l i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
apply iUnion₂_subset fun l hl ↦ iUnion₂_subset fun i _ ↦ ?_

Premises used: Set.iUnion₂_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
l : ℕ
hl : l < m + 1
i : @cell _ t C D _ l
h : i ∈ I l
rw :
  cellFrontier (C := C) (D := D) l i ∪ openCell (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ closedCell (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
rw [← cellFrontier_union_openCell_eq_closedCell]

Premises used: Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
l : ℕ
hl : l < m + 1
i : @cell _ t C D _ l
h : i ∈ I l
sr :
  cellFrontier (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
tr :
  openCell (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ cellFrontier (C := C) (D := D) l i ∪ openCell (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
apply union_subset

Premises used: Set.union_subset
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
l : ℕ
hl : l < m + 1
i : @cell _ t C D _ l
h : i ∈ I l
⊢ cellFrontier (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
(hm' l (Nat.le_of_lt_succ hl) ((ENat.coe_lt_coe.2 hl).trans hm) i)

Premises used: Iff.mpr, ENat.coe_lt_coe, Nat.le_of_lt_succ, LT.lt.trans
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
l : ℕ
hl : l < m + 1
i : @cell _ t C D _ l
h : i ∈ I l
⊢ cellFrontier (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
exact (hm' l (Nat.le_of_lt_succ hl) ((ENat.coe_lt_coe.2 hl).trans hm) i)

Premises used: Iff.mpr, ENat.coe_lt_coe, Nat.le_of_lt_succ, LT.lt.trans
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
l : ℕ
hl : l < m + 1
i : @cell _ t C D _ l
h : i ∈ I l
tr :
  openCell (C := C) (D := D) l i ⊆
    ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ openCell (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (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 D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
l : ℕ
hl : l < m + 1
i : @cell _ t C D _ l
h : i ∈ I l
⊢ openCell (C := C) (D := D) l i ⊆
    ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
subset_iUnion₂_of_subset l ((ENat.coe_lt_coe.2 hl).trans hm) <| subset_iUnion _ i

Premises used: Iff.mpr, Set.subset_iUnion₂_of_subset, Set.subset_iUnion, ENat.coe_lt_coe, LT.lt.trans
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
l : ℕ
hl : l < m + 1
i : @cell _ t C D _ l
h : i ∈ I l
⊢ openCell (C := C) (D := D) l i ⊆
    ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
exact subset_iUnion₂_of_subset l ((ENat.coe_lt_coe.2 hl).trans hm) <| subset_iUnion _ i

Premises used: Set.subset_iUnion₂_of_subset, Set.subset_iUnion
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
a :
  ∀ (hm : (↑0 : ℕ∞) < n) (j : @cell _ t C D _ 0),
    cellFrontier (C := C) (D := D) 0 j ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
a₁ :
  ∀ (m : ℕ)
    (hm' :
      ∀ m_1 ≤ m,
        ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
          cellFrontier (C := C) (D := D) m_1 j ⊆
            D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j)
    (hm : (↑(m + 1) : ℕ∞) < n) (j : @cell _ t C D _ (m + 1)),
    cellFrontier (C := C) (D := D) (m + 1) j ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ cellFrontier (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
induction m using Nat.case_strong_induction_on with
      | hz => simp [cellFrontier_zero_eq_empty]
      | hi m hm' =>
        obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (m + 1) j
        apply hI.trans
        apply union_subset subset_union_left
        apply iUnion₂_subset fun l hl ↦ iUnion₂_subset fun i _ ↦ ?_
        rw [← cellFrontier_union_openCell_eq_closedCell]
        apply union_subset
        · exact (hm' l (Nat.le_of_lt_succ hl) ((ENat.coe_lt_coe.2 hl).trans hm) i)
        · apply subset_union_of_subset_right
          exact subset_iUnion₂_of_subset l ((ENat.coe_lt_coe.2 hl).trans hm) <| subset_iUnion _ i

Premises used: Nat.case_strong_induction_on, Set.iUnion₂_subset, Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell, Set.union_subset, Set.subset_union_left, Set.subset_union_of_subset_right, HAdd.hAdd, OfNat.ofNat, Topology.RelCWComplex.cellFrontier_zero_eq_empty, Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
⊢ openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
subset_union_of_subset_right (subset_iUnion₂_of_subset m hm (subset_iUnion _ j)) _

Premises used: Set.subset_iUnion₂_of_subset, Set.subset_union_of_subset_right
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
⊢ openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
exact subset_union_of_subset_right (subset_iUnion₂_of_subset m hm (subset_iUnion _ j)) _

Premises used: Set.subset_iUnion₂_of_subset, Set.subset_union_of_subset_right