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_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) ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have h : 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) ⊆
  ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
Tactic: apply subset_union_of_subset_right
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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) ⊆
    ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have h : 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: apply subset_iUnion₂_of_subset l hi
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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 : ℕ∞
⊢ 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
have 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
Tactic: rw [← RelCWComplex.iUnion_openCell_eq_iUnion_closedCell]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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 : ℕ∞
⊢ 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
have 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)
Tactic: congrm D ∪ ?_
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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 : ℕ∞
⊢ 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)
have 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)
Tactic: apply iUnion_congr fun m ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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)
    (⋃ (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)
have 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')
Tactic: rw [iUnion_subtype, iUnion_comm]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ (↑(skeletonLT C (D := D) m) : Set X) ⊆ (↑(skeletonLT C (D := D) n) : Set X)
have 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
Tactic: simp_rw [coe_skeletonLT]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ 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
have 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)
Tactic: apply union_subset_union_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 : 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
⊢ Membership.mem (γ := Set X)
    (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j) x
have 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
Tactic: simp_rw [mem_iUnion, exists_prop] at xmem ⊢
Cleared hypotheses: xmem
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ ∃ (i : ℕ), (↑i : ℕ∞) < n ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1
have 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
Tactic: obtain ⟨l, lltm, xmeml⟩ := xmem
Cleared hypotheses: xmem
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ x ∈ (↑(skeletonLT C (D := D) (HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1)) : Set X)
have rw : x ∈
  D ∪
    ⋃ (m : ℕ),
      ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
Tactic: rw [coe_skeletonLT]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ x ∈
    D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have 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
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 : 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
⊢ Membership.mem (γ := Set X)
    (⋃ (m : ℕ),
      ⋃ (_ : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)
    x
have h : ∃ (i : ℕ),
  (↑i : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1
Tactic: simp_rw [mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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 : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have norm_cast : n < n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ cellFrontier (C := C) (D := D) n j ⊆ (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X)
have 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)
Tactic: obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell n 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 : 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
⊢ cellFrontier (C := C) (D := D) n j ⊆ (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X)
have apply : D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j ⊆ (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X)
Tactic: apply subset_trans hI
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X)
have 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
Tactic: rw [coe_skeletonLT]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ 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
have 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)
Tactic: apply union_subset_union_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 : 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
⊢ Membership.mem (γ := Set X)
    (⋃ (m : ℕ),
      ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑n : ℕ∞)), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)
    x
have 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
Tactic: simp only [mem_iUnion, exists_prop] at xmem ⊢
Cleared hypotheses: xmem
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
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
⊢ ∃ (i : ℕ), LT.lt (α := ℕ∞) (↑i : ℕ∞) (↑n : ℕ∞) ∧ ∃ (i_1 : @cell _ t C D _ i), x ∈ closedCell (C := C) (D := D) i i_1
have 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
Tactic: obtain ⟨i, iltn, j, _, xmem⟩ := xmem
Cleared hypotheses: xmem
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
⊢ (↑(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)
have 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
Tactic: rw [coe_skeletonLT, coe_skeletonLT, union_assoc]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
⊢ 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
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
⊢ 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)
have e_a : Eq.{u_1 + 1} (α := Set X)
  ((⋃ (m : ℕ), ⋃ (_ : 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 < n + 1), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
n : ℕ∞
⊢ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j =
    (↑(skeletonLT C (D := ∅) n) : Set X)
have rw : Eq.{u_1 + 1} (α := Set X) (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j)
  (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j)
Tactic: rw [← RelCWComplex.iUnion_openCell_eq_skeletonLT, empty_union]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
n : ℕ∞
rw :
  Eq.{u_1 + 1} (α := Set X)
    (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j)
    (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j)
⊢ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j =
    (↑(skeletonLT C (D := ∅) n) : Set X)
have rw₁ : Eq.{u_1 + 1} (α := Set X) (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j)
  (⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C ∅ _ m), openCell (C := C) (D := ∅) m j)
Tactic: rw [← RelCWComplex.iUnion_openCell_eq_skeletonLT, empty_union]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
⊢ ⋃ (n : ℕ), (↑(skeletonLT C (D := D) (↑n : ℕ∞)) : Set X) = C
have apply : C ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X)
Tactic: apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeletonLT C _).subset_complex)
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
⊢ C ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X)
have simp_rw : D ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X) ∧
  ∀ (i : ℕ) (j : @cell _ t C D _ i),
    openCell (C := C) (D := D) i j ⊆ ⋃ (i : ℕ), (↑(skeletonLT C (D := D) (↑i : ℕ∞)) : Set X)
Tactic: simp_rw [← union_iUnion_openCell_eq_complex, union_subset_iff, iUnion₂_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
⊢ ⋃ (n : ℕ), (↑(skeleton C (D := D) (↑n : ℕ∞)) : Set X) = C
have apply : C ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X)
Tactic: apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeleton C _).subset_complex)
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
⊢ C ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X)
have simp_rw : D ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X) ∧
  ∀ (i : ℕ) (j : @cell _ t C D _ i),
    openCell (C := C) (D := D) i j ⊆ ⋃ (i : ℕ), (↑(skeleton C (D := D) (↑i : ℕ∞)) : Set X)
Tactic: simp_rw [← union_iUnion_openCell_eq_complex, union_subset_iff, iUnion₂_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ∞
x : X
⊢ Membership.mem (γ := Subcomplex C (D := D)) (skeleton C (D := D) n) x ↔
    x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j
have rw : (x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) < n + 1) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j) ↔
  x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j
Tactic: rw [skeleton, mem_skeletonLT_iff]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ∞
x : X
⊢ (x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) < n + 1) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j) ↔
    x ∈ D ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C D _ m), x ∈ openCell (C := C) (D := D) m j
have suffices : ∀ (m : ℕ), (↑m : ℕ∞) < n + 1 ↔ (↑m : ℕ∞) ≤ n
Tactic: suffices ∀ (m : ℕ), m < n + 1 ↔ m ≤ n by simp_rw [this]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ∞
x : X
m : ℕ
⊢ (↑m : ℕ∞) < n + 1 ↔ (↑m : ℕ∞) ≤ n
have top : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) ⊤ 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) ⊤
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ∞
x : X
m : ℕ
top : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) ⊤ 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) ⊤
⊢ (↑m : ℕ∞) < n + 1 ↔ (↑m : ℕ∞) ≤ n
have coe : ∀ (a : ℕ), (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
x : X
m a : ℕ
⊢ (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
have coe : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) (↑1 : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_lt, Nat.cast_le, Order.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
x : X
m a : ℕ
coe : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) (↑1 : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
⊢ (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
have coe₁ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑(a + 1) : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_lt, Nat.cast_le, Order.lt_add_one_iff]