awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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] (A ∩ openCell (C := C) (D := D) n j)
have inl : IsClosed[t] ∅
Tactic: rw [disjoint_iff_inter_eq_empty.1 h]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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)
⊢ ∃ (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
have 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
Tactic: obtain ⟨J, hJ⟩ := cellFrontier_subset_base_union_finite_closedCell n.succ i
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ ∃ (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
have 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
Tactic: choose p hp using hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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 ∅
⊢ ∃ (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
have h : 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
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
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 + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
have hJ₁ : x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j
Tactic: specialize hJ hx
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
have 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
Tactic: simp only [mem_union, mem_iUnion, exists_prop] at hJ ⊢
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
have h : ∀ (hJ : x ∈ D), x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
Tactic: rcases hJ with hJ | hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
have 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
Tactic: rcases hJ with hJ | hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
have 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
Tactic: obtain ⟨l, hln, j, hj, hxj⟩ := hJ
Cleared hypotheses: hJ
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
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 ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
have hxj₁ : x ∈ cellFrontier (C := C) (D := D) l j ∪ openCell (C := C) (D := D) l j
Tactic: rw [← cellFrontier_union_openCell_eq_closedCell] at hxj
Cleared hypotheses: hxj
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
have 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
Tactic: rcases hxj with hxj | hxj
Cleared hypotheses: hxj
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
have 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
Tactic: rcases hxj with hxj | hxj
Cleared hypotheses: hxj
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
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 ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
have hp₁ : x ∈ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < l), ⋃ j_1 ∈ p l sorry j m, openCell (C := C) (D := D) m j_1
Tactic: specialize hp l (Nat.le_of_lt_succ hln) j hxj
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
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 < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
have hp₁ : x ∈ D ∨ ∃ i < l, ∃ i_1 ∈ p l sorry j i, x ∈ openCell (C := C) (D := D) i i_1
Tactic: simp_rw [mem_union, mem_iUnion, exists_prop] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
have h : (∃ i < l, ∃ i_1 ∈ p l sorry 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 sorry j k) (hxi : x ∈ openCell (C := C) (D := D) k i),
    i ∈ I k
Tactic: refine .imp_right (fun ⟨k, hkl, i, hi, hxi⟩ ↦ ⟨k, lt_trans hkl hln, i, ?_, hxi⟩) hp
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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 : ∃ 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
⊢ i ∈ I k
have 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
Tactic: simp only [Nat.succ_eq_add_one, Finset.mem_union, Finset.mem_biUnion, Finset.mem_range, I]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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 ∈ 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
have h : ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
Tactic: right
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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 ∈ openCell (C := C) (D := D) l j
⊢ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
have h : j ∈ I l ∧ x ∈ openCell (C := C) (D := D) l j
Tactic: use l, hln, j
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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 ∈ openCell (C := C) (D := D) l j
⊢ j ∈ I l ∧ x ∈ openCell (C := C) (D := D) l j
have h : (j ∈ J l ∨
    Membership.mem (γ := Finset (@cell _ t C D _ l))
      ((Finset.range (n + 1)).biUnion fun (l_1 : ℕ) ↦
        (J l_1).biUnion fun (y : @cell _ t C D _ l_1) ↦ if h : l_1 ≤ n then p l_1 h y l else ∅)
      j) ∧
  x ∈ openCell (C := C) (D := D) l j
Tactic: simp only [Nat.succ_eq_add_one, Finset.mem_union, I]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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)
⊢ ∃ (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
have 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
Tactic: classical
    obtain ⟨J, hJ⟩ := cellFrontier_subset_base_union_finite_closedCell n.succ i
    choose p hp using hn
    let I m := J m ∪ ((Finset.range n.succ).biUnion
      (fun l ↦ (J l).biUnion (fun y ↦ if h : l ≤ n then p l h y m else ∅)))
    use I
    intro x hx
    specialize hJ hx
    simp only [mem_union, mem_iUnion, exists_prop] at hJ ⊢
    rcases hJ with hJ | hJ
    · exact .inl hJ
    obtain ⟨l, hln, j, hj, hxj⟩ := hJ
    rw [← cellFrontier_union_openCell_eq_closedCell] at hxj
    rcases hxj with hxj | hxj
    · specialize hp l (Nat.le_of_lt_succ hln) j hxj
      simp_rw [mem_union, mem_iUnion, exists_prop] at hp
      refine .imp_right (fun ⟨k, hkl, i, hi, hxi⟩ ↦ ⟨k, lt_trans hkl hln, i, ?_, hxi⟩) hp
      simp only [Nat.succ_eq_add_one, Finset.mem_union, Finset.mem_biUnion, Finset.mem_range, I]
      exact .inr ⟨l, hln, j, hj, by simp [Nat.le_of_lt_succ hln, hi]⟩
    · right
      use l, hln, j
      simp only [Nat.succ_eq_add_one, Finset.mem_union, I]
      exact ⟨Or.intro_left _ hj, hxj⟩