awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x y : @cell _ t C D _ 0
h : closedCell (C := C) (D := D) 0 x = closedCell (C := C) (D := D) 0 y
⊢ x = y
have h₁ : (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![] = (↑(map (C := C) (D := D) 0 y) : (Fin 0 → ℝ) → X) ![]
Tactic: rw [closedCell_zero_eq_singleton, closedCell_zero_eq_singleton, singleton_eq_singleton_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x y : @cell _ t C D _ 0
h : openCell (C := C) (D := D) 0 x = openCell (C := C) (D := D) 0 y
⊢ x = y
have h₁ : (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![] = (↑(map (C := C) (D := D) 0 y) : (Fin 0 → ℝ) → X) ![]
Tactic: rw [openCell_zero_eq_singleton, openCell_zero_eq_singleton, singleton_eq_singleton_iff] at 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
e : @cell _ t C D _ 1
⊢ (↑(map (C := C) (D := D) 1 e) : (Fin 1 → ℝ) → X) '' sphere 0 1 =
    (↑(map (C := C) (D := D) 1 e) : (Fin 1 → ℝ) → X) '' {-1, 1}
have e_s : Eq (α := Set (Fin 1 → ℝ)) (sphere 0 1) {-1, 1}
Tactic: congr 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
e : @cell _ t C D _ 1
⊢ Eq (α := Set (Fin 1 → ℝ)) (sphere 0 1) {-1, 1}
have e_s : ∀ (f : Fin 1 → ℝ),
  Membership.mem (γ := Set (Fin 1 → ℝ)) (sphere 0 1) f ↔ Membership.mem (γ := Set (Fin 1 → ℝ)) {-1, 1} f
Tactic: ext f
-- 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 : @cell _ t C D _ 1
f : Fin 1 → ℝ
⊢ Membership.mem (γ := Set (Fin 1 → ℝ)) (sphere 0 1) f ↔ Membership.mem (γ := Set (Fin 1 → ℝ)) {-1, 1} f
have e_s : f 0 = 1 ∨ f 0 = -1 ↔ f = -1 ∨ f = 1
Tactic: simp only [mem_sphere_iff_norm, sub_zero, Pi.norm_def, Finset.univ_unique, Fin.default_eq_zero,
    Fin.isValue, Finset.sup_singleton, coe_nnnorm, Real.norm_eq_abs, abs_eq (zero_le_one' ℝ),
    mem_insert_iff, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
e : @cell _ t C D _ 1
f : Fin 1 → ℝ
⊢ f 0 = 1 ∨ f 0 = -1 ↔ f = -1 ∨ f = 1
have e_s : const (Fin 1) (f default) 0 = 1 ∨ const (Fin 1) (f default) 0 = -1 ↔
  const (Fin 1) (f default) 0 = (-1) 0 ∨ Eq (α := Fin 1 → ℝ) (const (Fin 1) (f default)) 1
Tactic: rw [eq_const_of_unique (f := f), ← funext_iff_of_subsingleton (x := 0) (y := 0)]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
e : @cell _ t C ∅ _ 1
⊢ ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
have obtain : ∀ (f : (m : ℕ) → Finset (@cell _ t C ∅ _ m))
  (h : cellFrontier (C := C) (D := ∅) 1 e ⊆ ⋃ (m : ℕ), ⋃ (_ : m < 1), ⋃ j ∈ f m, closedCell (C := C) (D := ∅) m j),
  ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
Tactic: obtain ⟨f, h⟩ := cellFrontier_subset_finite_closedCell 1 e
-- 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 : @cell _ t C ∅ _ 1
f : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
h : cellFrontier (C := C) (D := ∅) 1 e ⊆ ⋃ (m : ℕ), ⋃ (_ : m < 1), ⋃ j ∈ f m, closedCell (C := C) (D := ∅) m j
⊢ ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
have h₁ : (∃ (i : @cell _ t C ∅ _ 0),
    Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) i ∧
      (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) (-1) = (↑(map (C := C) (D := ∅) 0 i) : (Fin 0 → ℝ) → X) ![]) ∧
  ∃ (i : @cell _ t C ∅ _ 0),
    Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) i ∧
      (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) 1 = (↑(map (C := C) (D := ∅) 0 i) : (Fin 0 → ℝ) → X) ![]
Tactic: simp only [RelCWComplex.cellFrontier_one_eq, image_pair, Order.lt_one_iff, iUnion_iUnion_eq_left,
    RelCWComplex.closedCell_zero_eq_singleton, pair_subset_iff, mem_iUnion, mem_singleton_iff,
    exists_prop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
e : @cell _ t C ∅ _ 1
f : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
h :
  (∃ (i : @cell _ t C ∅ _ 0),
      Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) i ∧
        (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) (-1) = (↑(map (C := C) (D := ∅) 0 i) : (Fin 0 → ℝ) → X) ![]) ∧
    ∃ (i : @cell _ t C ∅ _ 0),
      Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) i ∧
        (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) 1 = (↑(map (C := C) (D := ∅) 0 i) : (Fin 0 → ℝ) → X) ![]
⊢ ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
have obtain : ∀ (u : @cell _ t C ∅ _ 0) (hu : Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) u)
  (hun1 : (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) (-1) = (↑(map (C := C) (D := ∅) 0 u) : (Fin 0 → ℝ) → X) ![])
  (v : @cell _ t C ∅ _ 0) (hv : Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) v)
  (hv1 : (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) 1 = (↑(map (C := C) (D := ∅) 0 v) : (Fin 0 → ℝ) → X) ![]),
  ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
Tactic: obtain ⟨⟨u, hu, hun1⟩, v, hv, hv1⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : CWComplex C
e : @cell _ t C ∅ _ 1
f : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
u : @cell _ t C ∅ _ 0
hu : Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) u
hun1 : (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) (-1) = (↑(map (C := C) (D := ∅) 0 u) : (Fin 0 → ℝ) → X) ![]
v : @cell _ t C ∅ _ 0
hv : Membership.mem (γ := Finset (@cell _ t C ∅ _ 0)) (f 0) v
hv1 : (↑(map (C := C) (D := ∅) 1 e) : (Fin 1 → ℝ) → X) 1 = (↑(map (C := C) (D := ∅) 0 v) : (Fin 0 → ℝ) → X) ![]
⊢ ∃ (x : @cell _ t C ∅ _ 0) (y : @cell _ t C ∅ _ 0),
    cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
have h : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 u ∪ closedCell (C := C) (D := ∅) 0 v
Tactic: use u, v
-- 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 ⊆ C
have simp_rw : D ⊆ D ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j
Tactic: simp_rw [← union]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
⊢ IsClosed[t] C
have rw : (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (C ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (C ∩ D)
Tactic: rw [closed C C (by rfl)]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
⊢ (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (C ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (C ∩ D)
have left : ∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (C ∩ closedCell (C := C) (D := D) n j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
left : ∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (C ∩ closedCell (C := C) (D := D) n j)
⊢ (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (C ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (C ∩ D)
have right : IsClosed[t] (C ∩ D)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
⊢ IsClosed[t] (C ∩ closedCell (C := C) (D := D) n j)
have left : IsClosed[t] (closedCell (C := C) (D := D) n j)
Tactic: rw [inter_eq_right.2 (closedCell_subset_complex _ _)]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
⊢ IsClosed[t] (C ∩ D)
have right : IsClosed[t] D
Tactic: rw [inter_eq_right.2 base_subset_complex]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j =
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have a : D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
Tactic: apply subset_antisymm
-- 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 : ℕ∞
a :
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j =
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have a₁ : D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: apply subset_antisymm
-- 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 : ℕ∞
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have a : D ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
Tactic: apply union_subset
-- 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 : ℕ∞
a : D ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have a₁ : ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
Tactic: apply union_subset
-- 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 : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have apply : ∀ (m : ℕ) (hm : (↑m : ℕ∞) < n) (j : @cell _ t C D _ m),
  openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
Tactic: apply iUnion₂_subset fun m hm ↦ iUnion_subset fun 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
⊢ openCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have h : openCell (C := C) (D := D) m j ⊆
  ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
Tactic: apply subset_union_of_subset_right
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : (↑m : ℕ∞) < n
j : @cell _ t C D _ m
⊢ openCell (C := C) (D := D) m j ⊆
    ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have h : openCell (C := C) (D := D) m j ⊆ ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
Tactic: apply subset_iUnion₂_of_subset m hm
-- 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
⊢ openCell (C := C) (D := D) m j ⊆ ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j
have h : openCell (C := C) (D := D) m j ⊆ closedCell (C := C) (D := D) m j
Tactic: apply subset_iUnion_of_subset 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 : ℕ∞
⊢ D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (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 : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (C := C) (D := D) m j ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: apply union_subset subset_union_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
n : ℕ∞
⊢ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), closedCell (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 : ℕ∞) < n) (j : @cell _ t C D _ m),
  closedCell (C := C) (D := D) m j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: refine iUnion₂_subset fun m hm ↦ iUnion_subset fun 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
⊢ closedCell (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 : cellFrontier (C := C) (D := D) m j ∪ openCell (C := C) (D := D) m j ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: rw [← cellFrontier_union_openCell_eq_closedCell]
-- 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 ∪ openCell (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 : cellFrontier (C := C) (D := D) m j ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: apply union_subset
-- 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 :
  cellFrontier (C := C) (D := D) m 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 ∪ openCell (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₁ : openCell (C := C) (D := D) m j ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: apply union_subset
-- 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)
⊢ 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
have a : ∀ (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),
  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: obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (m + 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
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
⊢ 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
have a : D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (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: apply hI.trans
-- 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
⊢ D ∪ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
have a : ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (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: apply union_subset subset_union_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
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
⊢ ⋃ (m_1 : ℕ), ⋃ (_ : m_1 < m + 1), ⋃ j ∈ I m_1, closedCell (C := C) (D := D) m_1 j ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
have apply : ∀ (l : ℕ) (hl : l < m + 1),
  ∀ i ∈ I l,
    closedCell (C := C) (D := D) l i ⊆
      D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: apply iUnion₂_subset fun l hl ↦ iUnion₂_subset fun 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 : ℕ∞
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
⊢ closedCell (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
have rw : cellFrontier (C := C) (D := D) l i ∪ openCell (C := C) (D := D) l i ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: rw [← cellFrontier_union_openCell_eq_closedCell]
-- 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
⊢ cellFrontier (C := C) (D := D) l i ∪ 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 sr : cellFrontier (C := C) (D := D) l i ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: apply union_subset
-- 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
sr :
  cellFrontier (C := C) (D := D) l i ⊆
    D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
⊢ cellFrontier (C := C) (D := D) l i ∪ 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 ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : (↑m : ℕ∞) < n), ⋃ (j : @cell _ t C D _ m), openCell (C := C) (D := D) m j
Tactic: apply union_subset