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
inst_1 : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
apply :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
⊢ IsClosed[t] A

Tactic:
apply isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell hAC hDA

Premises used: Topology.RelCWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_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
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
n : ℕ
hn : 0 < n
j : @cell _ t C D _ n
inl :
  ∀ (h : Disjoint A (openCell (C := C) (D := D) n j)),
    IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
inr :
  ∀ (h : IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)),
    IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
⊢ IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)

Tactic:
rcases h n hn j with h | h
-- 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
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h_1 :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
n : ℕ
hn : 0 < n
j : @cell _ t C D _ n
h : Disjoint A (openCell (C := C) (D := D) n j)
inl : IsClosed[t] (A ∩ openCell (C := C) (D := D) n j)
⊢ IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)

Tactic:
left
-- 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
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h_1 :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
n : ℕ
hn : 0 < n
j : @cell _ t C D _ n
h : Disjoint A (openCell (C := C) (D := D) n j)
inl : IsClosed[t] ∅
⊢ IsClosed[t] (A ∩ openCell (C := C) (D := D) n j)

Tactic:
rw [disjoint_iff_inter_eq_empty.1 h]

Premises used: Set.disjoint_iff_inter_eq_empty, Iff.mp
-- 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
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h_1 :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
n : ℕ
hn : 0 < n
j : @cell _ t C D _ n
h : Disjoint A (openCell (C := C) (D := D) n j)
⊢ IsClosed[t] ∅

Tactic:
isClosed_empty

Premises used: isClosed_empty
-- 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
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h_1 :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
n : ℕ
hn : 0 < n
j : @cell _ t C D _ n
h : Disjoint A (openCell (C := C) (D := D) n j)
⊢ IsClosed[t] ∅

Tactic:
exact isClosed_empty

Premises used: isClosed_empty
-- 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
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h_1 :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
n : ℕ
hn : 0 < n
j : @cell _ t C D _ n
h : IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
⊢ IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)

Tactic:
Or.inr h

Premises used: Or.inr
-- 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
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h_1 :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C D _ n),
        Disjoint A (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
n : ℕ
hn : 0 < n
j : @cell _ t C D _ n
h : IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
⊢ IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)

Tactic:
exact Or.inr h

Premises used: Or.inr
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
inst_1 : T2Space X
A : Set X
hAC : A ⊆ C
h :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C ∅ _ n),
        IsClosed[t] (A ∩ openCell (C := C) (D := ∅) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := ∅) n j)
⊢ IsClosed[t] (A ∩ ∅)

Tactic:
simp
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
inst_1 : T2Space X
A : Set X
hAC : A ⊆ C
h :
  ∀ (n : ℕ),
    0 < n →
      ∀ (j : @cell _ t C ∅ _ n),
        Disjoint A (openCell (C := C) (D := ∅) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := ∅) n j)
⊢ IsClosed[t] (A ∩ ∅)

Tactic:
simp
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
i : @cell _ t C D _ 0
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) 0 i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < 0), ⋃ j ∈ I 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 : ℕ
hn :
  ∀ m ≤ n,
    ∀ (i : @cell _ t C D _ m),
      ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
        cellFrontier (C := C) (D := D) m i ⊆
          D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ I m_1, openCell (C := C) (D := D) m_1 j
i : @cell _ t C D _ (n + 1)
hi :
  ∀ (J : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hJ :
      cellFrontier (C := C) (D := D) n.succ i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j),
    ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
      cellFrontier (C := C) (D := D) (n + 1) i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) (n + 1) i ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j

Tactic:
obtain ⟨J, hJ⟩ := cellFrontier_subset_base_union_finite_closedCell n.succ i

Premises used: Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell, Nat.succ
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
hn :
  ∀ m ≤ n,
    ∀ (i : @cell _ t C D _ m),
      ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
        cellFrontier (C := C) (D := D) m i ⊆
          D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ I m_1, openCell (C := C) (D := D) m_1 j
i : @cell _ t C D _ (n + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
hJ :
  cellFrontier (C := C) (D := D) n.succ i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j
hi :
  ∀ (p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m))
    (hp :
      ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
        cellFrontier (C := C) (D := D) m i ⊆
          D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j),
    ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
      cellFrontier (C := C) (D := D) (n + 1) i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) (n + 1) i ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j

Tactic:
choose p hp using hn
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
hJ :
  cellFrontier (C := C) (D := D) n.succ i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
h :
  cellFrontier (C := C) (D := D) (n + 1) i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) (n + 1) i ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
hJ :
  cellFrontier (C := C) (D := D) n.succ i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
⊢ x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j

Tactic:
specialize hJ hx
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
hJ : x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j
h :
  ∀ (hJ : x ∈ D ∨ ∃ i < n.succ, ∃ i_1 ∈ J i, x ∈ closedCell (C := C) (D := D) i i_1),
    x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
⊢ x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j

Tactic:
simp only [mem_union, mem_iUnion, exists_prop] at hJ ⊢

Premises used: Set.mem_union, Set.mem_iUnion, exists_prop
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
hJ : x ∈ D ∨ ∃ i < n.succ, ∃ i_1 ∈ J i, x ∈ closedCell (C := C) (D := D) i i_1
h : ∀ (hJ : x ∈ D), x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
h₁ :
  ∀ (hJ : ∃ i < n.succ, ∃ i_1 ∈ J i, x ∈ closedCell (C := C) (D := D) i i_1),
    x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
rcases hJ with hJ | hJ
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
hJ : x ∈ D
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
.inl hJ

Premises used: Or.inl
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
hJ : x ∈ D
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
exact .inl hJ
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
hJ : ∃ i < n.succ, ∃ i_1 ∈ J i, x ∈ closedCell (C := C) (D := D) i i_1
h :
  ∀ (l : ℕ) (hln : l < n.succ) (j : @cell _ t C D _ l) (hj : j ∈ J l) (hxj : x ∈ closedCell (C := C) (D := D) l j),
    x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
obtain ⟨l, hln, j, hj, hxj⟩ := hJ
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ closedCell (C := C) (D := D) l j
⊢ x ∈ cellFrontier (C := C) (D := D) l j ∪ openCell (C := C) (D := D) l j

Tactic:
rw [← cellFrontier_union_openCell_eq_closedCell] at hxj

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 : ℕ
i : @cell _ t C D _ (n + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ cellFrontier (C := C) (D := D) l j ∪ openCell (C := C) (D := D) l j
h :
  ∀ (hxj : x ∈ cellFrontier (C := C) (D := D) l j),
    x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
h₁ :
  ∀ (hxj : x ∈ openCell (C := C) (D := D) l j), x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
rcases hxj with hxj | hxj
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ cellFrontier (C := C) (D := D) l j
⊢ x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < l), ⋃ j_1 ∈ p l ⋯ j m, openCell (C := C) (D := D) m j_1

Tactic:
specialize hp l (Nat.le_of_lt_succ hln) j hxj

Premises used: Nat.le_of_lt_succ
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ cellFrontier (C := C) (D := D) l j
hp : x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < l), ⋃ j_1 ∈ p l ⋯ j m, openCell (C := C) (D := D) m j_1
⊢ x ∈ D ∨ ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
simp_rw [mem_union, mem_iUnion, exists_prop] at hp

Premises used: Set.mem_union, Set.mem_iUnion, exists_prop
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ cellFrontier (C := C) (D := D) l j
hp : x ∈ D ∨ ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell (C := C) (D := D) i i_1
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
.imp_right (fun ⟨k, hkl, i, hi, hxi⟩ ↦ ⟨k, lt_trans hkl hln, i, ?_, hxi⟩) hp

Premises used: Or.imp_right
-- 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 + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ cellFrontier (C := C) (D := D) l j
hp : x ∈ D ∨ ∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell (C := C) (D := D) i i_1
h :
  (∃ i < l, ∃ i_1 ∈ p l ⋯ j i, x ∈ openCell (C := C) (D := D) i i_1) →
    ∀ (k : ℕ) (hkl : k < l) (i : @cell _ t C D _ k) (hi : i ∈ p l ⋯ j k) (hxi : x ∈ openCell (C := C) (D := D) k i),
      i ∈ I k
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
refine .imp_right (fun ⟨k, hkl, i, hi, hxi⟩ ↦ ⟨k, lt_trans hkl hln, i, ?_, hxi⟩) hp
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i_1 : @cell _ t C D _ (n + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i_1
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ cellFrontier (C := C) (D := D) l j
hp : x ∈ D ∨ ∃ i < l, ∃ i_2 ∈ p l ⋯ j i, x ∈ openCell (C := C) (D := D) i i_2
h_1 : ∃ i < l, ∃ i_2 ∈ p l ⋯ j i, x ∈ openCell (C := C) (D := D) i i_2
k : ℕ
hkl : k < l
i : @cell _ t C D _ k
hi : i ∈ p l ⋯ j k
hxi : x ∈ openCell (C := C) (D := D) k i
h :
  i ∈ J k ∨
    ∃ a < n + 1, ∃ a_1 ∈ J a, Membership.mem (γ := Finset (@cell _ t C D _ k)) (if h : a ≤ n then p a h a_1 k else ∅) i
⊢ i ∈ I k

Tactic:
simp only [Nat.succ_eq_add_one, Finset.mem_union, Finset.mem_biUnion, Finset.mem_range, I]

Premises used: Nat.succ_eq_add_one, Finset.mem_range, Finset.mem_union, Finset.mem_biUnion