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
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:
exact subset_iUnion _ _

Premises used: Set.subset_iUnion
-- 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 : ℕ∞
rw :
  D ∪
      ⋃ (n_1 : ℕ),
        ⋃ (j : (↑((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) n_1) : Type u_1)),
          openCell (C := C) (D := D) n_1 (↑j : cell C n_1) =
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ D ∪
      ⋃ (n_1 : ℕ),
        ⋃ (j : (↑((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) n_1) : Type u_1)),
          openCell (C := C) (D := D) n_1 (↑j : cell C n_1) =
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
rw [← RelCWComplex.iUnion_openCell_eq_iUnion_closedCell]

Premises used: _private.0.Topology.RelCWComplex.iUnion_openCell_eq_iUnion_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
n : ℕ∞
congrm :
  Eq.{u_1 + 1} (α := Set X)
    (⋃ (n_1 : ℕ),
      ⋃ (j : (↑((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) n_1) : Type u_1)),
        openCell (C := C) (D := D) n_1 (↑j : cell C n_1))
    (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j)
⊢ D ∪
      ⋃ (n_1 : ℕ),
        ⋃ (j : (↑((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) n_1) : Type u_1)),
          openCell (C := C) (D := D) n_1 (↑j : cell C n_1) =
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j

Tactic:
congrm D ∪ ?_
-- 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 : ℕ∞
apply :
  ∀ (m : ℕ),
    Eq.{u_1 + 1} (α := Set X)
      (⋃ (j : (↑((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) m) : Type u_1)),
        openCell (C := C) (D := D) m (↑j : cell C m))
      (⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j)
⊢ Eq.{u_1 + 1} (α := Set X)
    (⋃ (n_1 : ℕ),
      ⋃ (j : (↑((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) n_1) : Type u_1)),
        openCell (C := C) (D := D) n_1 (↑j : cell C n_1))
    (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j)

Tactic:
apply iUnion_congr fun m ↦ ?_

Premises used: Set.iUnion_congr
-- 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 : ℕ∞
m : ℕ
rw :
  Eq.{u_1 + 1} (α := Set X)
    (⋃ (x : @cell _ t C D _ m),
      ⋃ (hx :
        Membership.mem (γ := Set (@cell _ t C D _ m))
          ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) m) x),
        openCell (C := C) (D := D) m
          (↑(Subtype.mk (p := fun (x : @cell _ t C D _ m) ↦
                Membership.mem (γ := Set (@cell _ t C D _ m))
                  ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) m) x)
                x hx) :
            cell C m))
    (⋃ (i' : @cell _ t C D _ m), ⋃ (_ : (↑m : ℕ∞) < n), openCell (C := C) (D := D) m i')
⊢ Eq.{u_1 + 1} (α := Set X)
    (⋃ (j : (↑((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) m) : Type u_1)),
      openCell (C := C) (D := D) m (↑j : cell C m))
    (⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j)

Tactic:
rw [iUnion_subtype, iUnion_comm]

Premises used: Set.iUnion_comm, Set.iUnion_subtype
-- 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 : ℕ∞
m : ℕ
⊢ Eq.{u_1 + 1} (α := Set X)
    (⋃ (x : @cell _ t C D _ m),
      ⋃ (hx :
        Membership.mem (γ := Set (@cell _ t C D _ m))
          ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) m) x),
        openCell (C := C) (D := D) m
          (↑(Subtype.mk (p := fun (x : @cell _ t C D _ m) ↦
                Membership.mem (γ := Set (@cell _ t C D _ m))
                  ((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) m) x)
                x hx) :
            cell C m))
    (⋃ (i' : @cell _ t C D _ m), ⋃ (_ : (↑m : ℕ∞) < n), openCell (C := C) (D := D) m i')

Tactic:
rfl
-- 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
⊢ (↑(skeletonLT C (D := D) 0) : Set X) = D

Tactic:
simp [coe_skeletonLT]

Premises used: Topology.RelCWComplex.coe_skeletonLT
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
⊢ (↑(skeletonLT C (D := ∅) 0) : Set X) = ∅

Tactic:
RelCWComplex.skeletonLT_zero_eq_base

Premises used: Topology.RelCWComplex.skeletonLT_zero_eq_base
-- 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
⊢ (↑(skeletonLT C (D := D) ⊤) : Set X) = C

Tactic:
simp [coe_skeletonLT, union]

Premises used: Topology.RelCWComplex.coe_skeletonLT, Topology.RelCWComplex.union
-- 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
⊢ (↑(skeleton C (D := D) ⊤) : Set X) = C

Tactic:
skeletonLT_top

Premises used: WithTop.map₂, Topology.RelCWComplex.skeletonLT_top, Option.map₂
-- 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 m : ℕ∞
h : m ≤ n
simp_rw :
  D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : (↑m_1 : ℕ∞) < m), ⋃ (j : @cell _ t C D _ m_1), closedCell (C := C) (D := D) m_1 j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ (↑(skeletonLT C (D := D) m) : Set X) ⊆ (↑(skeletonLT C (D := D) n) : Set X)

Tactic:
simp_rw [coe_skeletonLT]

Premises used: Topology.RelCWComplex.coe_skeletonLT
-- 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 m : ℕ∞
h : m ≤ n
h₁ :
  Subset.{u_1} (α := Set X)
    (⋃ (m_1 : ℕ), ⋃ (_ : (↑m_1 : ℕ∞) < m), ⋃ (j : @cell _ t C D _ m_1), closedCell (C := C) (D := D) m_1 j)
    (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)
⊢ D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : (↑m_1 : ℕ∞) < m), ⋃ (j : @cell _ t C D _ m_1), closedCell (C := C) (D := D) m_1 j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
apply union_subset_union_right

Premises used: Set.union_subset_union_right
-- 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 m : ℕ∞
h : m ≤ n
x : X
xmem :
  Membership.mem (γ := Set X)
    (⋃ (m_1 : ℕ), ⋃ (_ : (↑m_1 : ℕ∞) < m), ⋃ (j : @cell _ t C D _ m_1), closedCell (C := C) (D := D) m_1 j) x
h₁ :
  ∀ (xmem : ∃ (i : ℕ), (↑i : ℕ∞) < m ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1),
    ∃ (i : ℕ), (↑i : ℕ∞) < n ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1
⊢ Membership.mem (γ := Set X)
    (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j) x

Tactic:
simp_rw [mem_iUnion, exists_prop] at xmem ⊢

Premises used: Set.mem_iUnion, exists_prop
-- 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 m : ℕ∞
h : m ≤ n
x : X
xmem : ∃ (i : ℕ), (↑i : ℕ∞) < m ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1
h₁ :
  ∀ (l : ℕ) (lltm : (↑l : ℕ∞) < m) (xmeml : ∃ (i : @cell _ t C D _ l), x ∈ closedCell (C := C) (D := D) l i),
    ∃ (i : ℕ), (↑i : ℕ∞) < n ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1
⊢ ∃ (i : ℕ), (↑i : ℕ∞) < n ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1

Tactic:
obtain ⟨l, lltm, xmeml⟩ := xmem
-- 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 m : ℕ∞
h : m ≤ n
x : X
l : ℕ
lltm : (↑l : ℕ∞) < m
xmeml : ∃ (i : @cell _ t C D _ l), x ∈ closedCell (C := C) (D := D) l i
⊢ ∃ (i : ℕ), (↑i : ℕ∞) < n ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1

Tactic:
⟨l, lt_of_lt_of_le lltm h, xmeml⟩

Premises used: And.intro, Exists.intro, lt_of_lt_of_le
-- 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 m : ℕ∞
h : m ≤ n
x : X
l : ℕ
lltm : (↑l : ℕ∞) < m
xmeml : ∃ (i : @cell _ t C D _ l), x ∈ closedCell (C := C) (D := D) l i
⊢ ∃ (i : ℕ), (↑i : ℕ∞) < n ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1

Tactic:
exact ⟨l, lt_of_lt_of_le lltm h, xmeml⟩
-- 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
⊢ Monotone (β := Subcomplex C (D := D)) (skeletonLT C (D := D))

Tactic:
fun _ _ h ↦ skeletonLT_mono h

Premises used: Topology.RelCWComplex.skeletonLT_mono, Monotone, Set.Subset
-- 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 m : ℕ∞
h : m ≤ n
⊢ m + 1 ≤ n + 1

Tactic:
gcongr
-- 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
⊢ Monotone (β := Subcomplex C (D := D)) (skeleton C (D := D))

Tactic:
fun _ _ h ↦ skeleton_mono h

Premises used: Monotone, Set.Subset, Topology.RelCWComplex.skeleton_mono
-- 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
x : X
xmem : x ∈ closedCell (C := C) (D := D) n j
rw :
  x ∈
    D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ x ∈ (↑(skeletonLT C (D := D) (HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1)) : Set X)

Tactic:
rw [coe_skeletonLT]

Premises used: Topology.RelCWComplex.coe_skeletonLT
-- 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
x : X
xmem : x ∈ closedCell (C := C) (D := D) n j
h :
  Membership.mem (γ := Set X)
    (⋃ (m : ℕ),
      ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)
    x
⊢ x ∈
    D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
right
-- 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
x : X
xmem : x ∈ closedCell (C := C) (D := D) n j
h :
  ∃ (i : ℕ),
    (↑i : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1
⊢ Membership.mem (γ := Set X)
    (⋃ (m : ℕ),
      ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)
    x

Tactic:
simp_rw [mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, exists_prop
-- 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
x : X
xmem : x ∈ closedCell (C := C) (D := D) n j
norm_cast : n < n + 1
⊢ (↑n : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
norm_cast
-- 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
x : X
xmem : x ∈ closedCell (C := C) (D := D) n j
⊢ n < n + 1

Tactic:
lt_add_one n

Premises used: lt_add_one
-- 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
x : X
xmem : x ∈ closedCell (C := C) (D := D) n j
⊢ n < n + 1

Tactic:
exact lt_add_one n

Premises used: lt_add_one
-- 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
x : X
xmem : x ∈ closedCell (C := C) (D := D) n j
⊢ ∃ (i : ℕ),
    (↑i : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1

Tactic:
refine ⟨n, (by norm_cast; exact lt_add_one n), ⟨j,xmem⟩⟩
-- 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
⊢ closedCell (C := C) (D := D) n j ⊆ (↑(skeleton C (D := D) (↑n : ℕ∞)) : Set X)

Tactic:
closedCell_subset_skeletonLT n j

Premises used: Topology.RelCWComplex.closedCell_subset_skeletonLT
-- 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
⊢ openCell (C := C) (D := D) n j ⊆ (↑(skeletonLT C (D := D) (HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1)) : Set X)

Tactic:
(openCell_subset_closedCell _ _).trans (closedCell_subset_skeletonLT _ _)

Premises used: Topology.RelCWComplex.closedCell_subset_skeletonLT, HasSubset.Subset.trans, Topology.RelCWComplex.openCell_subset_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
n : ℕ
j : @cell _ t C D _ n
⊢ openCell (C := C) (D := D) n j ⊆ (↑(skeleton C (D := D) (↑n : ℕ∞)) : Set X)

Tactic:
(openCell_subset_closedCell _ _).trans (closedCell_subset_skeleton _ _)

Premises used: HasSubset.Subset.trans, Topology.RelCWComplex.openCell_subset_closedCell, Topology.RelCWComplex.closedCell_subset_skeleton
-- 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
obtain :
  ∀ (I : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hI :
      cellFrontier (C := C) (D := D) n j ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j),
    cellFrontier (C := C) (D := D) n j ⊆ (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X)
⊢ cellFrontier (C := C) (D := D) n j ⊆ (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X)

Tactic:
obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell n j

Premises used: Topology.RelCWComplex.cellFrontier_subset_base_union_finite_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
n : ℕ
j : @cell _ t C D _ n
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI : cellFrontier (C := C) (D := D) n j ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
apply :
  D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X)
⊢ cellFrontier (C := C) (D := D) n j ⊆ (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X)

Tactic:
apply subset_trans hI

Premises used: subset_trans
-- 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
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI : cellFrontier (C := C) (D := D) n j ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
rw :
  D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j ⊆
    D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X)

Tactic:
rw [coe_skeletonLT]

Premises used: Topology.RelCWComplex.coe_skeletonLT
-- 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
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI : cellFrontier (C := C) (D := D) n j ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
h :
  Subset.{u_1} (α := Set X) (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j)
    (⋃ (m : ℕ),
      ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j ⊆
    D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
apply union_subset_union_right

Premises used: Set.union_subset_union_right
-- 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
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI : cellFrontier (C := C) (D := D) n j ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
x : X
xmem : Membership.mem (γ := Set X) (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j) x
h :
  ∀ (xmem : ∃ i < n, ∃ i_1 ∈ I i, x ∈ closedCell (C := C) (D := D) i i_1),
    ∃ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1
⊢ Membership.mem (γ := Set X)
    (⋃ (m : ℕ),
      ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)
    x

Tactic:
simp only [mem_iUnion, exists_prop] at xmem ⊢

Premises used: Set.mem_iUnion, exists_prop
-- 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
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI : cellFrontier (C := C) (D := D) n j ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
x : X
xmem : ∃ i < n, ∃ i_1 ∈ I i, x ∈ closedCell (C := C) (D := D) i i_1
h :
  ∀ (i : ℕ) (iltn : i < n),
    ∀ j ∈ I i,
      ∀ (xmem : x ∈ closedCell (C := C) (D := D) i j),
        ∃ (i : ℕ),
          LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1
⊢ ∃ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1

Tactic:
obtain ⟨i, iltn, j, _, xmem⟩ := xmem
-- 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_1 : @cell _ t C D _ n
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI : cellFrontier (C := C) (D := D) n j_1 ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
x : X
i : ℕ
iltn : i < n
j : @cell _ t C D _ i
left : j ∈ I i
xmem : x ∈ closedCell (C := C) (D := D) i j
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : i < n
⊢ LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞)

Tactic:
norm_cast
-- 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_1 : @cell _ t C D _ n
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI : cellFrontier (C := C) (D := D) n j_1 ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
x : X
i : ℕ
iltn : i < n
j : @cell _ t C D _ i
left : j ∈ I i
xmem : x ∈ closedCell (C := C) (D := D) i j
⊢ ∃ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1

Tactic:
exact ⟨i, by norm_cast, j, xmem⟩
-- 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 + 1)
⊢ cellFrontier (C := C) (D := D) (n + 1) j ⊆ (↑(skeleton C (D := D) (↑n : ℕ∞)) : Set X)

Tactic:
cellFrontier_subset_skeletonLT _ _

Premises used: Topology.RelCWComplex.cellFrontier_subset_skeletonLT, WithTop.map₂, WithTop.some, Option.map₂
-- 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
l : ℕ
⊢ ⋃ (j : @cell _ t C D _ l), cellFrontier (C := C) (D := D) l j ⊆ (↑(skeletonLT C (D := D) (↑l : ℕ∞)) : Set X)

Tactic:
iUnion_subset (fun _ ↦ cellFrontier_subset_skeletonLT _ _)

Premises used: Set.iUnion_subset, Topology.RelCWComplex.cellFrontier_subset_skeletonLT
-- 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
l : ℕ
⊢ ⋃ (j : @cell _ t C D _ l), cellFrontier (C := C) (D := D) l j ⊆ (↑(skeleton C (D := D) (↑l : ℕ∞)) : Set X)

Tactic:
(iUnion_cellFrontier_subset_skeletonLT l).trans (skeletonLT_mono le_self_add)

Premises used: Topology.RelCWComplex.skeletonLT_mono, HasSubset.Subset.trans, Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT, le_self_add
-- 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 : ℕ
rw :
  D ∪
      ((⋃ (m : ℕ),
          ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j) ∪
        ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j) =
    D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X) ∪ ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j =
    (↑(skeletonLT C (D := D) (HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1)) : Set X)

Tactic:
rw [coe_skeletonLT, coe_skeletonLT, union_assoc]

Premises used: Topology.RelCWComplex.coe_skeletonLT, Set.union_assoc
-- 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 : ℕ
e_a :
  Eq.{u_1 + 1} (α := Set X)
    ((⋃ (m : ℕ),
        ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j) ∪
      ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j)
    (⋃ (m : ℕ),
      ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)
⊢ D ∪
      ((⋃ (m : ℕ),
          ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j) ∪
        ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j) =
    D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j

Tactic:
congr