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 : T2Space X
inst_1 : RelCWComplex C D
x : X
m a : ℕ
coe : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) (↑1 : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
coe₁ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑(a + 1) : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
⊢ (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
have coe₂ : m < a + 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_lt, Nat.cast_le, Order.lt_add_one_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 : T2Space X
inst_1 : RelCWComplex C D
x : X
m a : ℕ
coe : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) (↑1 : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
coe₁ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑(a + 1) : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
coe₂ : m < a + 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
⊢ (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
have coe₃ : m < a + 1 ↔ m ≤ a
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_lt, Nat.cast_le, Order.lt_add_one_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 : T2Space X
inst_1 : RelCWComplex C D
x : X
m a : ℕ
coe : (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) (↑1 : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
coe₁ : LT.lt (α := ℕ∞) (↑m : ℕ∞) (↑(a + 1) : ℕ∞) ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
coe₂ : m < a + 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
coe₃ : m < a + 1 ↔ m ≤ a
⊢ (↑m : ℕ∞) < HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) 1 ↔ LE.le (α := ℕ∞) (↑m : ℕ∞) (↑a : ℕ∞)
have coe₄ : m ≤ a ↔ m ≤ a
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_lt, Nat.cast_le, Order.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
n : ℕ∞
x : X
⊢ Membership.mem (γ := Subcomplex C (D := ∅)) (skeleton C (D := ∅) n) x ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
have rw : (Membership.mem (γ := Set X) ∅ x ∨
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j) ↔
  ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
Tactic: rw [RelCWComplex.mem_skeleton_iff, mem_empty_iff_false, false_or]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
n : ℕ∞
x : X
rw :
  (Membership.mem (γ := Set X) ∅ x ∨
      ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j) ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
⊢ Membership.mem (γ := Subcomplex C (D := ∅)) (skeleton C (D := ∅) n) x ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
have rw₁ : (False ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j) ↔
  ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
Tactic: rw [RelCWComplex.mem_skeleton_iff, mem_empty_iff_false, false_or]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst : T2Space X
inst_1 : CWComplex C
n : ℕ∞
x : X
rw :
  (Membership.mem (γ := Set X) ∅ x ∨
      ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j) ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
rw₁ :
  (False ∨ ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j) ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
⊢ Membership.mem (γ := Subcomplex C (D := ∅)) (skeleton C (D := ∅) n) x ↔
    ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
have rw₂ : (∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j) ↔
  ∃ (m : ℕ) (_ : (↑m : ℕ∞) ≤ n) (j : @cell _ t C ∅ _ m), x ∈ openCell (C := C) (D := ∅) m j
Tactic: rw [RelCWComplex.mem_skeleton_iff, mem_empty_iff_false, false_or]
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ Disjoint (↑(skeletonLT C (D := D) n) : Set X) (openCell (C := C) (D := D) m j)
have simp_rw : Disjoint D (openCell (C := C) (D := D) m j) ∧
  ∀ (i : ℕ) (i_1 : (↑i : ℕ∞) < n) (i_2 : @cell _ t C D _ i),
    Disjoint (openCell (C := C) (D := D) i i_2) (openCell (C := C) (D := D) m j)
Tactic: simp_rw [← iUnion_openCell_eq_skeletonLT, 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 : T2Space X
inst_1 : RelCWComplex C D
n : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ Disjoint D (openCell (C := C) (D := D) m j) ∧
    ∀ (i : ℕ) (i_1 : (↑i : ℕ∞) < n) (i_2 : @cell _ t C D _ i),
      Disjoint (openCell (C := C) (D := D) i i_2) (openCell (C := C) (D := D) m j)
have refine : ∀ (i : ℕ) (i_1 : (↑i : ℕ∞) < n) (i_2 : @cell _ t C D _ i),
  Disjoint (openCell (C := C) (D := D) i i_2) (openCell (C := C) (D := D) m j)
Tactic: refine ⟨(disjointBase m j).symm, ?_⟩
-- 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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
l : ℕ
hln : (↑l : ℕ∞) < n
i : @cell _ t C D _ l
⊢ Disjoint (openCell (C := C) (D := D) l i) (openCell (C := C) (D := D) m j)
have ne : Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) l i ≠ Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m j
Tactic: apply disjoint_openCell_of_ne
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
l : ℕ
hln : (↑l : ℕ∞) < n
i : @cell _ t C D _ l
h : Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) l i = Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m j
⊢ False
have hln₁ : (↑m : ℕ∞) < n
Tactic: simp_all only [Sigma.mk.inj_iff]
Cleared hypotheses: hln, h
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
l : ℕ
hln : (↑l : ℕ∞) < n
i : @cell _ t C D _ l
h : Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) l i = Sigma.mk (β := fun (n : ℕ) ↦ @cell _ t C D _ n) m j
hln₁ : (↑m : ℕ∞) < n
⊢ False
have a : l = m ∧ i ≍ j
Tactic: simp_all only [Sigma.mk.inj_iff]
Cleared hypotheses: hln, 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 : T2Space X
inst_1 : RelCWComplex C D
n : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ (↑(skeletonLT C (D := D) n) : Set X) ∩ closedCell (C := C) (D := D) m j =
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
have refine : (↑(skeletonLT C (D := D) n) : Set X) ∩ closedCell (C := C) (D := D) m j ⊆
  (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
Tactic: refine subset_antisymm ?_ (inter_subset_inter_right _ (cellFrontier_subset_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 : T2Space X
inst_1 : RelCWComplex C D
n : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ (↑(skeletonLT C (D := D) n) : Set X) ∩ closedCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
have rw : (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j ∪
    (↑(skeletonLT C (D := D) n) : Set X) ∩ openCell (C := C) (D := D) m j ⊆
  (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
Tactic: rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j ∪
      (↑(skeletonLT C (D := D) n) : Set X) ∩ openCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
have apply : (↑(skeletonLT C (D := D) n) : Set X) ∩ openCell (C := C) (D := D) m j ⊆
  (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
Tactic: apply union_subset (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 : ℕ∞
m : ℕ
j : @cell _ t C D _ m
hnm : n ≤ (↑m : ℕ∞)
⊢ (↑(skeletonLT C (D := D) n) : Set X) ∩ openCell (C := C) (D := D) m j ⊆
    (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
have rw : ∅ ⊆ (↑(skeletonLT C (D := D) n) : Set X) ∩ cellFrontier (C := C) (D := D) m j
Tactic: rw [(disjoint_skeletonLT_openCell hnm).inter_eq]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
⊢ Disjoint (interior D) (closedCell (C := C) (D := D) n j)
have rw : interior D ∩ closedCell (C := C) (D := D) n j = ∅
Tactic: rw [disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
⊢ interior D ∩ closedCell (C := C) (D := D) n j = ∅
have by_contra! : ∀ (h : (interior D ∩ closedCell (C := C) (D := D) n j).Nonempty), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
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
h : (interior D ∩ closedCell (C := C) (D := D) n j).Nonempty
⊢ False
have h₁ : (openCell (C := C) (D := D) n j ∩ interior D).Nonempty
Tactic: rw [← closure_openCell_eq_closedCell, inter_comm,
    closure_inter_open_nonempty_iff isOpen_interior] 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 : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
h : (openCell (C := C) (D := D) n j ∩ interior D).Nonempty
⊢ False
have rcases : ∀ (x : X) (xmemcell : x ∈ openCell (C := C) (D := D) n j) (xmemD : x ∈ interior D), False
Tactic: rcases h with ⟨x, xmemcell, xmemD⟩
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 : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
x : X
xmemcell : x ∈ openCell (C := C) (D := D) n j
xmemD : x ∈ interior D
this : x ∈ (↑(skeletonLT C (D := D) 0) : Set X) ∩ openCell (C := C) (D := D) n j
⊢ False
have rwa : ∀ (this : Membership.mem (γ := Set X) ∅ x), False
Tactic: rwa [(disjoint_skeletonLT_openCell n.cast_nonneg').inter_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
n : ℕ
j : @cell _ t C D _ n
x : X
xmemcell : x ∈ openCell (C := C) (D := D) n j
xmemD : x ∈ interior D
⊢ False
have suffices : x ∈ (↑(skeletonLT C (D := D) 0) : Set X) ∩ openCell (C := C) (D := D) n j
Tactic: suffices x ∈ (skeletonLT C 0 : Set X) ∩ openCell n j by
    rwa [(disjoint_skeletonLT_openCell n.cast_nonneg').inter_eq] at this
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
⊢ Disjoint (interior D) (⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j)
have simp_rw : interior D ∩ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j = ∅
Tactic: simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, disjoint_interior_base_closedCell.inter_eq,
    iUnion_empty]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
simp_rw : interior D ∩ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j = ∅
⊢ Disjoint (interior D) (⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j)
have simp_rw₁ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ℕ), ⋃ (i_1 : @cell _ t C D _ i), interior D ∩ closedCell (C := C) (D := D) i i_1) ∅
Tactic: simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, disjoint_interior_base_closedCell.inter_eq,
    iUnion_empty]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : T2Space X
inst_1 : RelCWComplex C D
simp_rw : interior D ∩ ⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j = ∅
simp_rw₁ :
  Eq.{u_1 + 1} (α := Set X) (⋃ (i : ℕ), ⋃ (i_1 : @cell _ t C D _ i), interior D ∩ closedCell (C := C) (D := D) i i_1) ∅
⊢ Disjoint (interior D) (⋃ (n : ℕ), ⋃ (j : @cell _ t C D _ n), closedCell (C := C) (D := D) n j)
have simp_rw₂ : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ℕ), ⋃ (i : @cell _ t C D _ i), ∅) ∅
Tactic: simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, disjoint_interior_base_closedCell.inter_eq,
    iUnion_empty]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
        IsClosed[inst_2] (A ∩ D) →
      IsClosed[inst_2] A
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ ∃ (I : (m : ℕ) → Finset (cell m)),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
have h : MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
  (D ∪
    ⋃ (m : ℕ),
      ⋃ (_ : m < n),
        ⋃ (j : cell m),
          ⋃ (_ :
            Membership.mem (γ := Finset (cell m)) ((fun (m : ℕ) ↦ (Finite.toFinset (s := univ) sorry : Finset (cell m))) m)
              j),
            (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
Tactic: use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
        IsClosed[inst_2] (A ∩ D) →
      IsClosed[inst_2] A
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : m < n),
          ⋃ (j : cell m),
            ⋃ (_ :
              Membership.mem (γ := Finset (cell m))
                ((fun (m : ℕ) ↦ (Finite.toFinset (s := univ) ⋯ : Finset (cell m))) m) j),
              (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
have h : MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
  (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
Tactic: simp only [Finite.mem_toFinset, mem_univ, iUnion_true]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D : Set X_1
inst_1 : RelCWComplex C_1 D
X : Type u
inst_2 : TopologicalSpace X
C : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) →
      IsClosed[inst_2] A
union' : ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ ∃ (I : (m : ℕ) → Finset (cell m)),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
have h : MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
  (⋃ (m : ℕ),
    ⋃ (_ : m < n),
      ⋃ (j : cell m),
        ⋃ (_ :
          Membership.mem (γ := Finset (cell m)) ((fun (m : ℕ) ↦ (Finite.toFinset (s := univ) sorry : Finset (cell m))) m)
            j),
          (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
Tactic: use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D : Set X_1
inst_1 : RelCWComplex C_1 D
X : Type u
inst_2 : TopologicalSpace X
C : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) →
      IsClosed[inst_2] A
union' : ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (⋃ (m : ℕ),
      ⋃ (_ : m < n),
        ⋃ (j : cell m),
          ⋃ (_ :
            Membership.mem (γ := Finset (cell m)) ((fun (m : ℕ) ↦ (Finite.toFinset (s := univ) ⋯ : Finset (cell m))) m)
              j),
            (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
have h : MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
  (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
Tactic: simp only [Finite.mem_toFinset, mem_univ, iUnion_true]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u + 1} (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ ∃ (I : (m : ℕ) → Finset (cell m)),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
have h : MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
  (D ∪
    ⋃ (m : ℕ),
      ⋃ (_ : m < n),
        ⋃ (j : cell m),
          ⋃ (_ :
            Membership.mem (γ := Finset (cell m)) ((fun (m : ℕ) ↦ (Finite.toFinset (s := univ) sorry : Finset (cell m))) m)
              j),
            (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
Tactic: use fun m ↦ finite_univ.toFinset (s := (univ : Set (cell m)))