-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.cellFrontier_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) :
    cellFrontier n j ⊆ skeletonLT C n

Proof state:
case intro.h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j ⊆ ⋃ m, ⋃ (_ : ↑m < ↑n), ⋃ j, closedCell m j

Tactic:
intro x xmem

Result:
case intro.h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
xmem : x ∈ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < ↑n), ⋃ j, closedCell m j

Proof state:
case intro
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j ⊆ skeletonLT C ↑n

Tactic:
apply union_subset_union_right

Result:
case intro.h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j ⊆ ⋃ m, ⋃ (_ : ↑m < ↑n), ⋃ j, closedCell m j

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ cellFrontier n j ⊆ skeletonLT C ↑n

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

Result:
case intro
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ cellFrontier n j ⊆ skeletonLT C ↑n

Proof state:
case intro.h.intro.intro.intro.intro
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j✝ : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j✝ ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
i : ℕ
iltn : i < n
j : cell C i
left✝ : j ∈ I i
xmem : x ∈ closedCell i j
⊢ ∃ i, ↑i < ↑n ∧ ∃ i_1, x ∈ closedCell i i_1

Tactic:
exact ⟨i, by norm_cast, j, xmem⟩

Result:
no goals

Proof state:
case intro
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ cellFrontier n j ⊆ skeletonLT C ↑n

Tactic:
apply subset_trans hI

Result:
case intro
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j ⊆ skeletonLT C ↑n

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j✝ : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j✝ ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
i : ℕ
iltn : i < n
j : cell C i
left✝ : j ∈ I i
xmem : x ∈ closedCell i j
⊢ ↑i < ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
case intro.h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
xmem : x ∈ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < ↑n), ⋃ j, closedCell m j

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

Result:
case intro.h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
xmem : ∃ i < n, ∃ i_1 ∈ I i, x ∈ closedCell i i_1
⊢ ∃ i, ↑i < ↑n ∧ ∃ i_1, x ∈ closedCell i i_1

Proof state:
case intro.h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
xmem : ∃ i < n, ∃ i_1 ∈ I i, x ∈ closedCell i i_1
⊢ ∃ i, ↑i < ↑n ∧ ∃ i_1, x ∈ closedCell i i_1

Tactic:
obtain ⟨i, iltn, j, _, xmem⟩ := xmem

Result:
case intro.h.intro.intro.intro.intro
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j✝ : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j✝ ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
i : ℕ
iltn : i < n
j : cell C i
left✝ : j ∈ I i
xmem : x ∈ closedCell i j
⊢ ∃ i, ↑i < ↑n ∧ ∃ i_1, x ∈ closedCell i i_1