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
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
⊢ Membership.mem (γ := Finset (@cell _ t C D _ k)) (if h : l ≤ n then p l h j k else ∅) i

Tactic:
simp [Nat.le_of_lt_succ hln, hi]

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i_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 ∈ 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:
exact .inr ⟨l, hln, j, hj, by simp [Nat.le_of_lt_succ hln, hi]⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ (n + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ openCell (C := C) (D := D) l j
h : ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
right
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ (n + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
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
h : j ∈ I l ∧ x ∈ openCell (C := C) (D := D) l j
⊢ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell (C := C) (D := D) i i_1

Tactic:
use l, hln, j
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ (n + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ openCell (C := C) (D := D) l j
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
⊢ j ∈ I l ∧ x ∈ openCell (C := C) (D := D) l j

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

Premises used: Nat.succ_eq_add_one, Finset.mem_union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ (n + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ openCell (C := C) (D := D) l j
⊢ (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:
⟨Or.intro_left _ hj, hxj⟩

Premises used: Or.intro_left, And.intro
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ (n + 1)
J : (m : ℕ) → Finset (@cell _ t C D _ m)
p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
    cellFrontier (C := C) (D := D) m i ⊆
      D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j
I : (m : ℕ) → Finset (@cell _ t C D _ m) :=
  fun (m : ℕ) ↦
    J m ∪
      (Finset.range n.succ).biUnion fun (l : ℕ) ↦
        (J l).biUnion fun (y : @cell _ t C D _ l) ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (C := C) (D := D) (n + 1) i
l : ℕ
hln : l < n.succ
j : @cell _ t C D _ l
hj : j ∈ J l
hxj : x ∈ openCell (C := C) (D := D) l j
⊢ (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:
exact ⟨Or.intro_left _ hj, hxj⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
hz :
  ∀ (i : @cell _ t C D _ 0),
    ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
      cellFrontier (C := C) (D := D) 0 i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < 0), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
hi :
  ∀ (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
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, openCell (C := C) (D := D) m j

Tactic:
induction n using Nat.case_strong_induction_on with
  | hz => simp [cellFrontier_zero_eq_empty]
  | hi n hn =>
    -- We apply `cellFrontier_subset_base_union_finite_closedCell` once and then apply
    -- the induction hypothesis to the finitely many cells that
    -- `cellFrontier_subset_base_union_finite_closedCell` gives us.
    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⟩

Premises used: Set.mem_union, Nat.case_strong_induction_on, Nat.succ_eq_add_one, Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell, Set.mem_iUnion, Finset.mem_range, exists_prop, Finset.mem_union, Topology.RelCWComplex.cellFrontier_zero_eq_empty, Topology.RelCWComplex.cellFrontier_union_openCell_eq_closedCell, Nat.succ, Finset.mem_biUnion
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
n : ℕ
i : @cell _ t C ∅ _ n
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, openCell (C := C) (D := ∅) m j

Tactic:
simpa using RelCWComplex.cellFrontier_subset_finite_openCell n i

Premises used: Topology.RelCWComplex.cellFrontier_subset_finite_openCell
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E F : Subcomplex C (D := D)
h :
  Eq.{u_1 + 1} (α := Set X) ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) E)
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) F)
obtain :
  ∀ (E : Set X) (I : (n : ℕ) → Set (@cell _ t C D _ n)) (closed' : IsClosed[t] E)
    (hE : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E)
    (h :
      Eq.{u_1 + 1} (α := Set X)
        ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) E I closed' hE))
        ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) F)),
    mk (C := C) (D := D) E I closed' hE = F
⊢ E = F

Tactic:
obtain ⟨E, _, _, hE⟩ := E
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
F : Subcomplex C (D := D)
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closed' : IsClosed[t] E
hE : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
h :
  Eq.{u_1 + 1} (α := Set X)
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) E I closed' hE))
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) F)
obtain :
  ∀ (F : Set X) (I_1 : (n : ℕ) → Set (@cell _ t C D _ n)) (closed'_1 : IsClosed[t] F)
    (hF : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I_1 n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = F)
    (h :
      Eq.{u_1 + 1} (α := Set X)
        ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) E I closed' hE))
        ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) F I_1 closed'_1 hF))),
    mk (C := C) (D := D) E I closed' hE = mk (C := C) (D := D) F I_1 closed'_1 hF
⊢ mk (C := C) (D := D) E I closed' hE = F

Tactic:
obtain ⟨F, _, _, hF⟩ := F
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closed' : IsClosed[t] E
hE : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
F : Set X
I_1 : (n : ℕ) → Set (@cell _ t C D _ n)
closed'_1 : IsClosed[t] F
hF : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I_1 n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = F
h :
  Eq.{u_1 + 1} (α := Set X)
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) E I closed' hE))
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) F I_1 closed'_1 hF))
e_I : I = I_1
⊢ mk (C := C) (D := D) E I closed' hE = mk (C := C) (D := D) F I_1 closed'_1 hF

Tactic:
congr
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closed' : IsClosed[t] E
hE : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
F : Set X
I_1 : (n : ℕ) → Set (@cell _ t C D _ n)
closed'_1 : IsClosed[t] F
hF : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I_1 n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = F
h :
  Eq.{u_1 + 1} (α := Set X)
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) E I closed' hE))
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) F I_1 closed'_1 hF))
e_I :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I_1 n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
⊢ I = I_1

Tactic:
apply eq_of_eq_union_iUnion

Premises used: Topology.RelCWComplex.eq_of_eq_union_iUnion
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closed' : IsClosed[t] E
hE : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
F : Set X
I_1 : (n : ℕ) → Set (@cell _ t C D _ n)
closed'_1 : IsClosed[t] F
hF : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I_1 n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = F
h :
  Eq.{u_1 + 1} (α := Set X)
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) E I closed' hE))
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) F I_1 closed'_1 hF))
e_I : E = F
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I_1 n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)

Tactic:
rw [hE, hF]
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closed' : IsClosed[t] E
hE : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
F : Set X
I_1 : (n : ℕ) → Set (@cell _ t C D _ n)
closed'_1 : IsClosed[t] F
hF : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I_1 n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = F
h :
  Eq.{u_1 + 1} (α := Set X)
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) E I closed' hE))
    ((fun (E : Subcomplex C (D := D)) ↦ E.carrier (C := C) (D := D)) (mk (C := C) (D := D) F I_1 closed'_1 hF))
⊢ E = F

Tactic:
simpa using h
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
x : X
⊢ x ∈ E.carrier (C := C) (D := D) ↔ x ∈ (↑E : Set X)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
⊢ (↑E : Set X) = E.carrier (C := C) (D := D)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E F : Subcomplex C (D := D)
h : ∀ (x : X), x ∈ E ↔ x ∈ F
⊢ E = F

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E F : Subcomplex C (D := D)
⊢ E = F ↔ (↑E : Set X) = (↑F : Set X)

Tactic:
SetLike.coe_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, SetLike.coe_injective, Iff.symm
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
F : Set X
hF : F = (↑E : Set X)
J : (n : ℕ) → Set (@cell _ t C D _ n)
hJ : J = E.I (C := C) (D := D)
⊢ (↑(E.copy (C := C) (D := D) F hF J hJ) : Set X) = F

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
F : Set X
hF : F = (↑E : Set X)
J : (n : ℕ) → Set (@cell _ t C D _ n)
hJ : J = E.I (C := C) (D := D)
⊢ E.copy (C := C) (D := D) F hF J hJ = E

Tactic:
SetLike.coe_injective hF

Premises used: SetLike.coe_injective
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
rw : E.carrier (C := C) (D := D) = (↑E : Set X)
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    (↑E : Set X)

Tactic:
rw [E.union']

Premises used: Topology.RelCWComplex.Subcomplex.union'
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
⊢ E.carrier (C := C) (D := D) = (↑E : Set X)

Tactic:
rfl
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
E : Subcomplex C (D := D)
⊢ IsClosed[t] (↑E : Set X)

Tactic:
E.closed'

Premises used: Topology.RelCWComplex.Subcomplex.closed'
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
E : Subcomplex C (D := ∅)
⊢ ∅ ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := ∅) n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) =
    (↑E : Set X)

Tactic:
have := RelCWComplex.Subcomplex.union E (C := C)
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
E : Subcomplex C (D := ∅)
this :
  ∅ ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := ∅) n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) =
    (↑E : Set X)
⊢ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := ∅) n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) =
    (↑E : Set X)

Tactic:
rw [empty_union] at this

Premises used: Set.empty_union
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
E : Subcomplex C (D := ∅)
this :
  ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := ∅) n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) =
    (↑E : Set X)
⊢ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := ∅) n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) =
    (↑E : Set X)

Tactic:
this
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
E : Subcomplex C (D := ∅)
this :
  ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := ∅) n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) =
    (↑E : Set X)
⊢ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := ∅) n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n) =
    (↑E : Set X)

Tactic:
exact this
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
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
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
simp_rw :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j
⊢ E ⊆ C

Tactic:
simp_rw [← union, ← 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_1 D_1 : Set X
inst : T2Space X
C D : Set X
inst_1 : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j

Tactic:
union_subset_union_right D
        (iUnion_mono fun n ↦ iUnion_subset fun i ↦ subset_iUnion _ (i : cell C n))

Premises used: Set.iUnion_subset, Topology.RelCWComplex.openCell, Set.union_subset_union_right, Set.subset_iUnion, Set.iUnion_mono, Subtype.val
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
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
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), openCell (C := C) (D := D) n j

Tactic:
exact union_subset_union_right D
        (iUnion_mono fun n ↦ iUnion_subset fun i ↦ subset_iUnion _ (i : cell C n))

Premises used: Set.iUnion_subset, Set.union_subset_union_right, Set.subset_iUnion, Set.iUnion_mono
-- Module: Mathlib.Topology.CWComplex.Classical.Basic
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
E : Set X
I : (n : ℕ) → Set (@cell _ t C D _ n)
closedCell_subset : ∀ (n : ℕ) (i : (↑(I n) : Type u_1)), closedCell (C := C) (D := D) n (↑i : cell C n) ⊆ E
union : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) = E
⊢ E ⊆ C

Tactic:
have hEC : (E : Set X) ⊆ C := by
      simp_rw [← union, ← union_iUnion_openCell_eq_complex (C := C)]
      exact union_subset_union_right D
        (iUnion_mono fun n ↦ iUnion_subset fun i ↦ subset_iUnion _ (i : cell C n))