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
n : ℕ∞
m : ℕ
hm' :
  ∀ m_1 ≤ m,
    ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
      cellFrontier (C := C) (D := D) m_1 j ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
hm : (↑(m + 1) : ℕ∞) < n
j : @cell _ t C D _ (m + 1)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j
l : ℕ
hl : l < m + 1
i : @cell _ t C D _ l
h : i ∈ I l
⊢ openCell (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
have tr : openCell (C := C) (D := D) l i ⊆
  ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (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 D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
⊢ cellFrontier (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
have a : ∀ (hm : (↑0 : ℕ∞) < n) (j : @cell _ t C D _ 0),
  cellFrontier (C := C) (D := D) 0 j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: induction m using Nat.case_strong_induction_on with
      | hz => simp [cellFrontier_zero_eq_empty]
      | hi m hm' =>
        obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (m + 1) j
        apply hI.trans
        apply union_subset subset_union_left
        apply iUnion₂_subset fun l hl ↦ iUnion₂_subset fun i _ ↦ ?_
        rw [← cellFrontier_union_openCell_eq_closedCell]
        apply union_subset
        · exact (hm' l (Nat.le_of_lt_succ hl) ((ENat.coe_lt_coe.2 hl).trans hm) i)
        · apply subset_union_of_subset_right
          exact subset_iUnion₂_of_subset l ((ENat.coe_lt_coe.2 hl).trans hm) <| subset_iUnion _ i
Cleared hypotheses: m, hm, 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 : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
a :
  ∀ (hm : (↑0 : ℕ∞) < n) (j : @cell _ t C D _ 0),
    cellFrontier (C := C) (D := D) 0 j ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ cellFrontier (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
have a₁ : ∀ (m : ℕ)
  (hm' :
    ∀ m_1 ≤ m,
      ∀ (hm : (↑m_1 : ℕ∞) < n) (j : @cell _ t C D _ m_1),
        cellFrontier (C := C) (D := D) m_1 j ⊆
          D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j)
  (hm : (↑(m + 1) : ℕ∞) < n) (j : @cell _ t C D _ (m + 1)),
  cellFrontier (C := C) (D := D) (m + 1) j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: induction m using Nat.case_strong_induction_on with
      | hz => simp [cellFrontier_zero_eq_empty]
      | hi m hm' =>
        obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (m + 1) j
        apply hI.trans
        apply union_subset subset_union_left
        apply iUnion₂_subset fun l hl ↦ iUnion₂_subset fun i _ ↦ ?_
        rw [← cellFrontier_union_openCell_eq_closedCell]
        apply union_subset
        · exact (hm' l (Nat.le_of_lt_succ hl) ((ENat.coe_lt_coe.2 hl).trans hm) i)
        · apply subset_union_of_subset_right
          exact subset_iUnion₂_of_subset l ((ENat.coe_lt_coe.2 hl).trans hm) <| subset_iUnion _ i
Cleared hypotheses: m, hm, 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
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j = C
have suffices : D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j =
  D ∪ ⋃ (m : ℕ), ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) ⊤), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
Tactic: suffices D ∪ ⋃ n, ⋃ (j : cell C n), openCell n j =
      D ∪ ⋃ (m : ℕ) (_ : m < (⊤ : ℕ∞)) (j : cell C m), closedCell m j by
    simpa [union] using 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 : RelCWComplex C D
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j =
    D ∪ ⋃ (m : ℕ), ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) ⊤), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have simp_rw : D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j =
  D ∪ ⋃ (m : ℕ), ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) ⊤), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: simp_rw [← RelCWComplex.iUnion_openCell_eq_iUnion_closedCell, ENat.coe_lt_top, iUnion_true]
-- 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
simp_rw :
  D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j =
    D ∪ ⋃ (m : ℕ), ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) ⊤), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j =
    D ∪ ⋃ (m : ℕ), ⋃ (_ : LT.lt (α := ℕ∞) (↑m : ℕ∞) ⊤), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have simp_rw₁ : D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j =
  D ∪ ⋃ (m : ℕ), ⋃ (_ : True), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: simp_rw [← RelCWComplex.iUnion_openCell_eq_iUnion_closedCell, ENat.coe_lt_top, iUnion_true]
-- 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 : ℕ
j : @cell _ t C D _ n
m : ℕ
i : @cell _ t C D _ m
h : ¬Disjoint (openCell (C := C) (D := D) n j) (openCell (C := C) (D := D) m i)
⊢ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) n j = Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m i
have contrapose! : ∀ (h : Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) n j ≠ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m i),
  Disjoint (openCell (C := C) (D := D) n j) (openCell (C := C) (D := D) m i)
Tactic: contrapose! h
Cleared hypotheses: 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
⊢ Disjoint D (⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j)
have simp_rw : ∀ (i : ℕ) (i_1 : @cell _ t C D _ i), D ∩ openCell (C := C) (D := D) i i_1 = ∅
Tactic: simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, iUnion_eq_empty]
-- 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
⊢ D ∩ openCell (C := C) (D := D) n i = ∅
have rw : openCell (C := C) (D := D) n i ∩ D = ∅
Tactic: rw [inter_comm, (disjointBase n i).inter_eq]
-- 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
rw : openCell (C := C) (D := D) n i ∩ D = ∅
⊢ D ∩ openCell (C := C) (D := D) n i = ∅
have rw₁ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
Tactic: rw [inter_comm, (disjointBase n i).inter_eq]
-- 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
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
hD : IsClosed[t] (A ∩ D)
⊢ IsClosed[t] (A ∩ cellFrontier (C := C) (D := D) (n + 1) j)
have obtain : ∀ (I : (m : ℕ) → Finset (@cell _ t C D _ m))
  (hI :
    cellFrontier (C := C) (D := D) (n + 1) j ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j),
  IsClosed[t] (A ∩ cellFrontier (C := C) (D := D) (n + 1) j)
Tactic: obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (n + 1) 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
inst_1 : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (n + 1) j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
⊢ IsClosed[t] (A ∩ cellFrontier (C := C) (D := D) (n + 1) j)
have rw : IsClosed[t]
  (A ∩ (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j) ∩
    cellFrontier (C := C) (D := D) (n + 1) j)
Tactic: rw [← inter_eq_right.2 hI, ← inter_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 : RelCWComplex C D
inst_1 : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (n + 1) j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
⊢ IsClosed[t]
    (A ∩ (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j) ∩
      cellFrontier (C := C) (D := D) (n + 1) j)
have refine : IsClosed[t] (A ∩ (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j))
Tactic: refine IsClosed.inter ?_ isClosed_cellFrontier
-- 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
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (n + 1) j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
⊢ IsClosed[t] (A ∩ (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j))
have simp_rw : IsClosed[t]
  (A ∩ D ∪
    ⋃ (x : { x : ℕ // x < n + 1 }),
      ⋃ (i : @cell _ t C D _ (↑x : ℕ)),
        ⋃ (_ : Membership.mem (γ := Finset (@cell _ t C D _ (↑x : ℕ))) (I (↑x : ℕ)) i),
          A ∩ closedCell (C := C) (D := D) (↑x : ℕ) i)
Tactic: simp_rw [inter_union_distrib_left, inter_iUnion,
    ← iUnion_subtype (fun m ↦ m < n + 1) (fun m ↦ ⋃ i ∈ I m, A ∩ closedCell m 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
inst_1 : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (n + 1) j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
⊢ IsClosed[t]
    (A ∩ D ∪
      ⋃ (x : { x : ℕ // x < n + 1 }),
        ⋃ (i : @cell _ t C D _ (↑x : ℕ)),
          ⋃ (_ : Membership.mem (γ := Finset (@cell _ t C D _ (↑x : ℕ))) (I (↑x : ℕ)) i),
            A ∩ closedCell (C := C) (D := D) (↑x : ℕ) i)
have apply : IsClosed[t]
  (⋃ (x : { x : ℕ // x < n + 1 }),
    ⋃ (i : @cell _ t C D _ (↑x : ℕ)),
      ⋃ (_ : Membership.mem (γ := Finset (@cell _ t C D _ (↑x : ℕ))) (I (↑x : ℕ)) i),
        A ∩ closedCell (C := C) (D := D) (↑x : ℕ) i)
Tactic: apply hD.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 : RelCWComplex C D
inst_1 : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (n + 1) j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
⊢ IsClosed[t]
    (⋃ (x : { x : ℕ // x < n + 1 }),
      ⋃ (i : @cell _ t C D _ (↑x : ℕ)),
        ⋃ (_ : Membership.mem (γ := Finset (@cell _ t C D _ (↑x : ℕ))) (I (↑x : ℕ)) i),
          A ∩ closedCell (C := C) (D := D) (↑x : ℕ) i)
have h : ∀ (i : { x : ℕ // x < n + 1 }),
  IsClosed[t]
    (⋃ (i_1 : @cell _ t C D _ (↑i : ℕ)),
      ⋃ (_ : Membership.mem (γ := Finset (@cell _ t C D _ (↑i : ℕ))) (I (↑i : ℕ)) i_1),
        A ∩ closedCell (C := C) (D := D) (↑i : ℕ) i_1)
Tactic: apply isClosed_iUnion_of_finite
-- 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
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (@cell _ t C D _ m)
hI :
  cellFrontier (C := C) (D := D) (n + 1) j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
m : ℕ
mlt : m < n + 1
⊢ IsClosed[t]
    (⋃ (i : @cell _ t C D _ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) m mlt) : ℕ)),
      ⋃ (_ :
        Membership.mem (γ := Finset (@cell _ t C D _ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) m mlt) : ℕ)))
          (I (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) m mlt) : ℕ)) i),
        A ∩ closedCell (C := C) (D := D) (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) m mlt) : ℕ) i)
have h : IsClosed[t] (⋃ (x : ↥(I m)), A ∩ closedCell (C := C) (D := D) m (↑x : cell C m))
Tactic: rw [← iUnion_subtype (fun i ↦ i ∈ I m) (fun i ↦ A ∩ closedCell m i.1)]
-- 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 :
  ∀ (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
have rw : (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (A ∩ D)
Tactic: rw [closed C A hAC]
-- 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 :
  ∀ (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)
⊢ (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (A ∩ D)
have refine : ∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
Tactic: refine ⟨?_, hDA⟩
-- 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 :
  ∀ (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)
j : @cell _ t C D _ 0
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) 0 j)
have hz : IsClosed[t] (A ∩ {(↑(map (C := C) (D := D) 0 j) : (Fin 0 → ℝ) → X) ![]})
Tactic: rw [closedCell_zero_eq_singleton]
-- 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
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),
        IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)
have h₁ : IsClosed[t] (A ∩ openCell (C := C) (D := D) n.succ j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n.succ j)
Tactic: specialize h n.succ n.zero_lt_succ j
Cleared hypotheses: 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
inst_1 : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
h : IsClosed[t] (A ∩ openCell (C := C) (D := D) n.succ j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)
have hi : ∀ (h1 : IsClosed[t] (A ∩ openCell (C := C) (D := D) n.succ j)), IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)
Tactic: rcases h with h1 | h2
Cleared hypotheses: 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
inst_1 : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
h : IsClosed[t] (A ∩ openCell (C := C) (D := D) n.succ j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n.succ j)
hi :
  ∀ (h1 : IsClosed[t] (A ∩ openCell (C := C) (D := D) n.succ j)),
    IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)
have hi₁ : ∀ (h2 : IsClosed[t] (A ∩ closedCell (C := C) (D := D) n.succ j)),
  IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)
Tactic: rcases h with h1 | h2
Cleared hypotheses: 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
inst_1 : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j)
j : @cell _ t C D _ (n + 1)
h1 : IsClosed[t] (A ∩ openCell (C := C) (D := D) n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)
have hi : IsClosed[t] (A ∩ cellFrontier (C := C) (D := D) (n + 1) j ∪ A ∩ openCell (C := C) (D := D) (n + 1) j)
Tactic: rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]
-- 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 :
  ∀ (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)
n : ℕ
j : @cell _ t C D _ n
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
have hz : ∀ (j : @cell _ t C D _ 0), IsClosed[t] (A ∩ closedCell (C := C) (D := D) 0 j)
Tactic: induction n using Nat.case_strong_induction_on with
  | hz =>
    rw [closedCell_zero_eq_singleton]
    exact isClosed_inter_singleton
  | hi n hn =>
    specialize h n.succ n.zero_lt_succ j
    rcases h with h1 | h2
    · rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]
      exact (isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell hn j hDA).union h1
    · exact h2
Cleared hypotheses: 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 : 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),
        IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
n : ℕ
j : @cell _ t C D _ n
hz : ∀ (j : @cell _ t C D _ 0), IsClosed[t] (A ∩ closedCell (C := C) (D := D) 0 j)
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
have hi : ∀ (n : ℕ) (hn : ∀ m ≤ n, ∀ (j : @cell _ t C D _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := D) m j))
  (j : @cell _ t C D _ (n + 1)), IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)
Tactic: induction n using Nat.case_strong_induction_on with
  | hz =>
    rw [closedCell_zero_eq_singleton]
    exact isClosed_inter_singleton
  | hi n hn =>
    specialize h n.succ n.zero_lt_succ j
    rcases h with h1 | h2
    · rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]
      exact (isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell hn j hDA).union h1
    · exact h2
Cleared hypotheses: 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 : 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)
⊢ IsClosed[t] A
have 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)
Tactic: apply isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell hAC hDA
-- 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 :
  ∀ (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
⊢ IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
have 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)
Tactic: rcases h n hn j with h | 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
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)
⊢ IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
have 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)
Tactic: rcases h n hn j with h | 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
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) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
have inl : IsClosed[t] (A ∩ openCell (C := C) (D := D) n j)
Tactic: left