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
this :
  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
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j = C

Tactic:
simpa [union] using this

Premises used: Topology.RelCWComplex.union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
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
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j = C

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
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
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
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
⊢ 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:
simp_rw [← RelCWComplex.iUnion_openCell_eq_iUnion_closedCell, ENat.coe_lt_top, iUnion_true]

Premises used: Set.iUnion_true, _private.0.Topology.RelCWComplex.iUnion_openCell_eq_iUnion_closedCell, ENat.coe_lt_top
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
⊢ ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), openCell (C := C) (D := ∅) n j = C

Tactic:
simpa using RelCWComplex.union_iUnion_openCell_eq_complex (C := C)

Premises used: Topology.RelCWComplex.union_iUnion_openCell_eq_complex
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
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)
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)
⊢ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) n j = Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m i

Tactic:
contrapose! h
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
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 : 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:
disjoint_openCell_of_ne h

Premises used: Topology.RelCWComplex.disjoint_openCell_of_ne
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
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 : 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:
exact disjoint_openCell_of_ne h

Premises used: Topology.RelCWComplex.disjoint_openCell_of_ne
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
simp_rw : ∀ (i : ℕ) (i_1 : @cell _ t C D _ i), D ∩ openCell (C := C) (D := D) i i_1 = ∅
⊢ Disjoint D (⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j)

Tactic:
simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, iUnion_eq_empty]

Premises used: Set.disjoint_iff_inter_eq_empty, Set.iUnion_eq_empty, Set.inter_iUnion
-- 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
rw : openCell (C := C) (D := D) n i ∩ D = ∅
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
⊢ D ∩ openCell (C := C) (D := D) n i = ∅

Tactic:
rw [inter_comm, (disjointBase n i).inter_eq]

Premises used: Set.inter_comm, Topology.RelCWComplex.disjointBase, Disjoint.inter_eq
-- 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
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)
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)
⊢ IsClosed[t] (A ∩ cellFrontier (C := C) (D := D) (n + 1) j)

Tactic:
obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (n + 1) j

Premises used: Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell, HAdd.hAdd, OfNat.ofNat
-- 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
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
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)
⊢ IsClosed[t] (A ∩ cellFrontier (C := C) (D := D) (n + 1) j)

Tactic:
rw [← inter_eq_right.2 hI, ← inter_assoc]

Premises used: Iff.mpr, Set.inter_eq_right, Set.inter_assoc
-- 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
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)

Tactic:
IsClosed.inter ?_ isClosed_cellFrontier

Premises used: IsClosed.inter, Topology.RelCWComplex.isClosed_cellFrontier
-- 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
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
refine : IsClosed[t] (A ∩ (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)

Tactic:
refine IsClosed.inter ?_ isClosed_cellFrontier

Premises used: IsClosed.inter, Topology.RelCWComplex.isClosed_cellFrontier
-- 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
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
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)
⊢ IsClosed[t] (A ∩ (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j))

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)]

Premises used: Inter.inter, HAdd.hAdd, Topology.RelCWComplex.closedCell, LT.lt, Set.inter_iUnion, Set.iUnion_subtype, OfNat.ofNat, Subtype.val, Set.iUnion, Set.inter_union_distrib_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
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
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)
⊢ 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:
apply hD.union

Premises used: IsClosed.union
-- 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
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
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)
⊢ 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 isClosed_iUnion_of_finite

Premises used: isClosed_iUnion_of_finite
-- 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
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
h : IsClosed[t] (⋃ (x : ↥(I m)), A ∩ closedCell (C := C) (D := D) m (↑x : cell C m))
⊢ 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)

Tactic:
rw [← iUnion_subtype (fun i ↦ i ∈ I m) (fun i ↦ A ∩ closedCell m i.1)]

Premises used: Membership.mem, Inter.inter, Topology.RelCWComplex.closedCell, Set.iUnion_subtype, Subtype.val
-- 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
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] (⋃ (x : ↥(I m)), A ∩ closedCell (C := C) (D := D) m (↑x : cell C m))

Tactic:
isClosed_iUnion_of_finite (fun ⟨j, _⟩ ↦ hn m (Nat.le_of_lt_succ mlt) j)

Premises used: isClosed_iUnion_of_finite, _private.0.Topology.RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell.match_2, Inter.inter, IsClosed, Nat.le_of_lt_succ, Topology.RelCWComplex.closedCell, Subtype.val
-- 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
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] (⋃ (x : ↥(I m)), A ∩ closedCell (C := C) (D := D) m (↑x : cell C m))

Tactic:
exact isClosed_iUnion_of_finite (fun ⟨j, _⟩ ↦ hn m (Nat.le_of_lt_succ mlt) j)

Premises used: isClosed_iUnion_of_finite
-- 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
n : ℕ
hn : ∀ m ≤ n, ∀ (j : @cell _ t C ∅ _ m), IsClosed[t] (A ∩ closedCell (C := C) (D := ∅) m j)
j : @cell _ t C ∅ _ (n + 1)
⊢ IsClosed[t] (A ∩ ∅)

Tactic:
simp only [inter_empty, isClosed_empty]

Premises used: isClosed_empty, Set.inter_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 :
  ∀ (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)
rw : (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (A ∩ D)
⊢ IsClosed[t] A

Tactic:
rw [closed C A hAC]

Premises used: Topology.RelCWComplex.closed
-- 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),
        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)

Tactic:
⟨?_, hDA⟩

Premises used: And.intro
-- 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),
        IsClosed[t] (A ∩ openCell (C := C) (D := D) n j) ∨ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)
refine : ∀ (n : ℕ) (j : @cell _ t C D _ n), 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)

Tactic:
refine ⟨?_, hDA⟩
-- 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),
        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
hz : IsClosed[t] (A ∩ {(↑(map (C := C) (D := D) 0 j) : (Fin 0 → ℝ) → X) ![]})
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) 0 j)

Tactic:
rw [closedCell_zero_eq_singleton]

Premises used: Topology.RelCWComplex.closedCell_zero_eq_singleton
-- 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),
        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 ∩ {(↑(map (C := C) (D := D) 0 j) : (Fin 0 → ℝ) → X) ![]})

Tactic:
isClosed_inter_singleton

Premises used: isClosed_inter_singleton
-- 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),
        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 ∩ {(↑(map (C := C) (D := D) 0 j) : (Fin 0 → ℝ) → X) ![]})

Tactic:
exact isClosed_inter_singleton

Premises used: isClosed_inter_singleton
-- 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),
        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 ∩ 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

Premises used: Nat.zero_lt_succ, Nat.succ
-- 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)
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)
hi₁ :
  ∀ (h2 : IsClosed[t] (A ∩ closedCell (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)

Tactic:
rcases h with h1 | h2
-- 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)
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)
hi : IsClosed[t] (A ∩ cellFrontier (C := C) (D := D) (n + 1) j ∪ A ∩ openCell (C := C) (D := D) (n + 1) j)
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)

Tactic:
rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]

Premises used: Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell, Set.inter_union_distrib_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)
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 ∩ cellFrontier (C := C) (D := D) (n + 1) j ∪ A ∩ openCell (C := C) (D := D) (n + 1) j)

Tactic:
(isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell hn j hDA).union h1

Premises used: IsClosed.union, Topology.RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_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)
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 ∩ cellFrontier (C := C) (D := D) (n + 1) j ∪ A ∩ openCell (C := C) (D := D) (n + 1) j)

Tactic:
exact (isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell hn j hDA).union h1

Premises used: IsClosed.union, Topology.RelCWComplex.isClosed_inter_cellFrontier_succ_of_le_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)
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)
h2 : IsClosed[t] (A ∩ closedCell (C := C) (D := D) n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)

Tactic:
h2
-- 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)
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)
h2 : IsClosed[t] (A ∩ closedCell (C := C) (D := D) n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) (n + 1) j)

Tactic:
exact h2
-- 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),
        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)
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)
⊢ IsClosed[t] (A ∩ closedCell (C := C) (D := D) n 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

Premises used: Nat.case_strong_induction_on, isClosed_inter_singleton, Topology.RelCWComplex.closedCell_zero_eq_singleton, Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell, Set.inter_union_distrib_left