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 : ℕ
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)
hi :
  ∀ (J : (m : ℕ) → Finset (@cell _ t C D _ m))
    (hJ :
      cellFrontier (C := C) (D := D) n.succ i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j),
    ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
      cellFrontier (C := C) (D := D) (n + 1) i ⊆
        D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) (n + 1) i ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
have hi₁ : ∀ (J : (m : ℕ) → Finset (@cell _ t C D _ m))
  (hJ :
    cellFrontier (C := C) (D := D) n.succ i ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell (C := C) (D := D) m j)
  (p : (m : ℕ) → m ≤ n → (i : @cell _ t C D _ m) → (m : ℕ) → Finset (@cell _ t C D _ m))
  (hp :
    ∀ (m : ℕ) (a : m ≤ n) (i : @cell _ t C D _ m),
      cellFrontier (C := C) (D := D) m i ⊆
        D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell (C := C) (D := D) m_1 j),
  ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) (n + 1) i ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell (C := C) (D := D) m j
Tactic: 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⟩
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ ∃ (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
have 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
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⟩
Cleared hypotheses: n, i
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
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
⊢ ∃ (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
have 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
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⟩
Cleared hypotheses: n, 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
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)
⊢ E = F
have 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
Tactic: obtain ⟨E, _, _, hE⟩ := E
Cleared hypotheses: E, 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
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)
⊢ mk (C := C) (D := D) E I closed' hE = F
have 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
Tactic: obtain ⟨F, _, _, hF⟩ := F
Cleared hypotheses: F, 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
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))
⊢ mk (C := C) (D := D) E I closed' hE = mk (C := C) (D := D) F I_1 closed'_1 hF
have e_I : I = I_1
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 : 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))
⊢ I = I_1
have 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)
Tactic: apply eq_of_eq_union_iUnion
-- 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
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))
⊢ 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)
have e_I : E = F
Tactic: rw [hE, hF]
-- 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
E : Subcomplex C (D := D)
⊢ 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)
have rw : E.carrier (C := C) (D := D) = (↑E : Set X)
Tactic: rw [E.union']
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
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)
have this : ∅ ∪ ⋃ (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)
-- 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
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
have 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
Tactic: simp_rw [← union, ← union_iUnion_openCell_eq_complex (C := C)]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
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
⊢ IsClosed[t] E
have hEC : 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))
-- 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
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
hEC : E ⊆ C
⊢ IsClosed[t] E
have hDA : IsClosed[t] (E ∩ D)
Tactic: apply isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell hEC
-- 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
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
hEC : E ⊆ C
hDA : IsClosed[t] (E ∩ D)
⊢ IsClosed[t] E
have h : ∀ (n : ℕ),
  0 < n →
    ∀ (j : @cell _ t C D _ n),
      Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
Tactic: apply isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell hEC
-- 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
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
hEC : E ⊆ C
⊢ D ⊆ E
have rw : D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
Tactic: rw [← union]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
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
hEC : E ⊆ C
⊢ IsClosed[t] (E ∩ D)
have this : D ⊆ E
Tactic: have : D ⊆ E := by
        rw [← union]
        exact subset_union_left
-- 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
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
hEC : E ⊆ C
this : D ⊆ E
⊢ IsClosed[t] (E ∩ D)
have hDA : IsClosed[t] D
Tactic: rw [inter_eq_right.2 this]
-- 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
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
hEC : E ⊆ C
n : ℕ
h : 0 < n
j : @cell _ t C D _ n
⊢ Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
have pos : ∀ (h : j ∈ I n), Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
Tactic: by_cases h : j ∈ I n
-- 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
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
hEC : E ⊆ C
n : ℕ
h : 0 < n
j : @cell _ t C D _ n
pos : ∀ (h : j ∈ I n), Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
⊢ Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
have neg : ∀ (h : j ∉ I n), Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
Tactic: by_cases h : j ∈ I n
-- 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
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
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∈ I n
⊢ Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
have pos : IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
Tactic: 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
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
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∈ I n
this : closedCell (C := C) (D := D) n j ⊆ E
⊢ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
have rw : IsClosed[t] (closedCell (C := C) (D := D) n j)
Tactic: rw [inter_eq_right.2 this]
-- 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
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
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∈ I n
⊢ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
have pos : closedCell (C := C) (D := D) n j ⊆ E
Tactic: suffices closedCell n j ⊆ E by
        rw [inter_eq_right.2 this]
        exact isClosed_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
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
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∉ I n
⊢ Disjoint E (openCell (C := C) (D := D) n j) ∨ IsClosed[t] (E ∩ closedCell (C := C) (D := D) n j)
have neg : Disjoint E (openCell (C := C) (D := D) n j)
Tactic: left
-- 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
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
hEC : E ⊆ C
n : ℕ
h_1 : 0 < n
j : @cell _ t C D _ n
h : j ∉ I n
⊢ Disjoint E (openCell (C := C) (D := D) n j)
have neg : Disjoint D (openCell (C := C) (D := D) n j) ∧
  ∀ (i : ℕ) (i_1 : (↑(I i) : Type u_1)),
    Disjoint (openCell (C := C) (D := D) i (↑i_1 : cell C i)) (openCell (C := C) (D := D) n j)
Tactic: simp_rw [← union, disjoint_union_left, disjoint_iUnion_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
E : Subcomplex C (D := D)
⊢ (↑E : Set X) ⊆ C
have simp_rw : D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) 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: simp_rw [← union, ← RelCWComplex.union_iUnion_openCell_eq_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 : RelCWComplex C D
E : Subcomplex C (D := D)
⊢ D ⊆ (↑E : Set X)
have simp_rw : D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(E.I (C := C) (D := D) n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
Tactic: simp_rw [← union]
-- 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 : (↑((fun (l : ℕ) ↦ ({x : @cell _ t C D _ l | (↑l : ℕ∞) < n} : Set (@cell _ t C D _ l))) l) : Type u_1)),
    closedCell (C := C) (D := D) l (↑i : cell C l) ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have this : ∀ (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
Tactic: ⟨i, hi⟩