awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Bornology.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Bornology α
inst_2 : Bornology β
inst_3 : Bornology γ
inst_4 : Bornology δ
f g : LocallyBoundedMap α β
h :
  Eq (α := (a : α) → β) ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) f) ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toFun : α → β) (comap_cobounded_le' : comap toFun (cobounded β) ≤ cobounded α)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' })
      ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) g)),
  { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' : LocallyBoundedMap α β } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Bornology.Hom (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : FunLike F α β
inst_1 : Bornology α
inst_2 : Bornology β
inst_3 : Bornology γ
inst_4 : Bornology δ
g : LocallyBoundedMap α β
toFun : α → β
comap_cobounded_le' : comap toFun (cobounded β) ≤ cobounded α
h :
  Eq (α := (a : α) → β)
    ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' })
    ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) g)
⊢ { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' : LocallyBoundedMap α β } = g
have mk : ∀ (toFun_1 : α → β) (comap_cobounded_le'_1 : comap toFun_1 (cobounded β) ≤ cobounded α)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' })
      ((fun (f : LocallyBoundedMap α β) ↦ f.toFun) { toFun := toFun_1, comap_cobounded_le' := comap_cobounded_le'_1 })),
  { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' : LocallyBoundedMap α β } =
    { toFun := toFun_1, comap_cobounded_le' := comap_cobounded_le'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.Bornology.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Bornology α
inst_1 : Bornology β
inst_2 : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Bornology α
inst_1 : Bornology β
inst_2 : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Hom (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Bornology α
inst_1 : Bornology β
inst_2 : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
have rw₂ : Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Real (goal)
Goal:
r : ℝ
⊢ BddAbove (α := ℝ≥0) (closedBall 0 r)
have inl : ∀ (hr : 0 ≤ r), BddAbove (α := ℝ≥0) (closedBall 0 r)
Tactic: obtain hr | hr := le_or_gt 0 r
-- Lean 4 proof step from Mathlib.Topology.Bornology.Real (goal)
Goal:
r : ℝ
inl : ∀ (hr : 0 ≤ r), BddAbove (α := ℝ≥0) (closedBall 0 r)
⊢ BddAbove (α := ℝ≥0) (closedBall 0 r)
have inr : ∀ (hr : r < 0), BddAbove (α := ℝ≥0) (closedBall 0 r)
Tactic: obtain hr | hr := le_or_gt 0 r
-- 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
n : ℕ
i : @cell _ t C ∅ _ n
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
have this : ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
  MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
Tactic: have := RelCWComplex.mapsTo 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
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
have rcases : ∀ (I : (m : ℕ) → Finset (@cell _ t C D _ m))
  (hI :
    MapsTo (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)),
  ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
Tactic: rcases mapsTo n i with ⟨I, hI⟩
-- 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)
hI :
  MapsTo (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C D _ m)),
    cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
have h : cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
Tactic: use I
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
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)
hI :
  MapsTo (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ cellFrontier (C := C) (D := D) n i ⊆ D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := D) m j
have hI₁ : (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' sphere 0 1 ⊆
  D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := D) m j) : (Fin m → ℝ) → X) '' closedBall 0 1
Tactic: rw [mapsTo_iff_image_subset] at hI
Cleared hypotheses: hI
-- 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
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, closedCell (C := C) (D := ∅) m j
have rcases : ∀ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m))
  (hI :
    MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)),
  ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := ∅) m j
Tactic: rcases RelCWComplex.mapsTo n i with ⟨I, hI⟩
-- 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
n : ℕ
i : @cell _ t C ∅ _ n
I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
hI :
  MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ ∃ (I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)),
    cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := ∅) m j
have h : cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := ∅) m j
Tactic: use I
-- 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
n : ℕ
i : @cell _ t C ∅ _ n
I : (m : ℕ) → Finset (@cell _ t C ∅ _ m)
hI :
  MapsTo (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (∅ ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
⊢ cellFrontier (C := C) (D := ∅) n i ⊆ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell (C := C) (D := ∅) m j
have hI₁ : (↑(map (C := C) (D := ∅) n i) : (Fin n → ℝ) → X) '' sphere 0 1 ⊆
  ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ j ∈ I m, (↑(map (C := C) (D := ∅) m j) : (Fin m → ℝ) → X) '' closedBall 0 1
Tactic: rw [mapsTo_iff_image_subset, empty_union] at hI
Cleared hypotheses: hI
-- 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
⊢ ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), closedCell (C := C) (D := ∅) n j = C
have this : ∅ ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
Tactic: have := RelCWComplex.union' (C := C)
-- 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
this : ∅ ∪ ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
⊢ ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), closedCell (C := C) (D := ∅) n j = C
have this₁ : ⋃ (n : ℕ), ⋃ (j : @cell _ t C ∅ _ n), (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
Tactic: rw [empty_union] 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 : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ cellFrontier (C := C) (D := D) n i ∪ openCell (C := C) (D := D) n i = closedCell (C := C) (D := D) n i
have rw : (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' (sphere 0 1 ∪ ball 0 1) =
  (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' closedBall 0 1
Tactic: rw [cellFrontier, openCell, closedCell, ← image_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 : RelCWComplex C D
n : ℕ
i : @cell _ t C D _ n
⊢ (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' (sphere 0 1 ∪ ball 0 1) =
    (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) '' closedBall 0 1
have congrm : Eq (α := Set (Fin n → ℝ)) (sphere 0 1 ∪ ball 0 1) (closedBall 0 1)
Tactic: congrm map 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
⊢ (↑(map (C := C) (D := D) n i) : (Fin n → ℝ) → X) 0 ∈ openCell (C := C) (D := D) n i
have h : Membership.mem (γ := Set (Fin n → ℝ)) (ball 0 1) 0
Tactic: apply mem_image_of_mem
-- 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
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
⊢ i ∈ J n
have by_contra : ∀ (hJ : i ∉ J n), False
Tactic: by_contra hJ
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
⊢ False
have h : openCell (C := C) (D := D) n i ⊆
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
Tactic: have h : openCell n i ⊆ D ∪ ⋃ n, ⋃ (j : J n), openCell (C := C) n j :=
    hIJ.symm ▸ subset_union_of_subset_right
      (subset_iUnion_of_subset n (subset_iUnion_of_subset ⟨i, hi⟩ (subset_refl (openCell n i)))) D
-- 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
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
h :
  openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
⊢ Disjoint (openCell (C := C) (D := D) n i)
    (D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n))
have simp_rw : Disjoint (openCell (C := C) (D := D) n i) D ∧
  ∀ (i_1 : ℕ) (i_2 : (↑(J i_1) : Type u_1)),
    Disjoint (openCell (C := C) (D := D) n i) (openCell (C := C) (D := D) i_1 (↑i_2 : cell C i_1))
Tactic: simp_rw [disjoint_union_right, disjoint_iUnion_right]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
h :
  openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
⊢ False
have h' : Disjoint (openCell (C := C) (D := D) n i)
  (D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n))
Tactic: have h' : Disjoint (openCell n i) (D ∪ ⋃ n, ⋃ (j : J n), openCell (C := C) n j) := by
    simp_rw [disjoint_union_right, disjoint_iUnion_right]
    exact ⟨disjointBase n i, fun m j ↦ disjoint_openCell_of_ne (by lia)⟩
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (hypothesis)
Goal:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst : RelCWComplex C D
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
n : ℕ
i : @cell _ t C D _ n
hi : i ∈ I n
hJ : i ∉ J n
h :
  openCell (C := C) (D := D) n i ⊆
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
h' :
  Disjoint (openCell (C := C) (D := D) n i)
    (D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n))
⊢ False
have h'₁ : openCell (C := C) (D := D) n i = ∅
Tactic: rw [disjoint_of_subset_iff_left_eq_empty h] 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
I J : (n : ℕ) → Set (@cell _ t C D _ n)
hIJ :
  D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n) =
    D ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := D) n (↑j : cell C n)
⊢ I = J
have h : ∀ (n : ℕ) (x : @cell _ t C D _ n), x ∈ I n ↔ x ∈ J n
Tactic: ext n x
-- 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
I J : (n : ℕ) → Set (@cell _ t C ∅ _ n)
hIJ :
  Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
    (⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
⊢ I = J
have hIJ₁ : Eq.{u_1 + 1} (α := Set X) (∅ ∪ ⋃ (n : ℕ), ⋃ (j : (↑(I n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
  (∅ ∪ ⋃ (n : ℕ), ⋃ (j : (↑(J n) : Type u_1)), openCell (C := C) (D := ∅) n (↑j : cell C n))
Tactic: apply RelCWComplex.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
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
⊢ closure[t] (openCell (C := C) (D := D) n j) = closedCell (C := C) (D := D) n j
have apply : closedCell (C := C) (D := D) n j ⊆ closure[t] (openCell (C := C) (D := D) n j)
Tactic: apply subset_antisymm (isClosed_closedCell.closure_subset_iff.2 (openCell_subset_closedCell n 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
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
⊢ closedCell (C := C) (D := D) n j ⊆ closure[t] (openCell (C := C) (D := D) n j)
have rw : (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) '' closure (ball 0 1) ⊆ closure[t] (openCell (C := C) (D := D) n j)
Tactic: rw [closedCell, ← closure_ball 0 (by exact one_ne_zero)]
-- 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
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
⊢ (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) '' closure (ball 0 1) ⊆ closure[t] (openCell (C := C) (D := D) n j)
have hf : ContinuousOn (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) (closure (ball 0 1))
Tactic: apply ContinuousOn.image_closure
-- 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
inst_1 : T2Space X
n : ℕ
j : @cell _ t C D _ n
⊢ ContinuousOn (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) (closure (ball 0 1))
have hf : ContinuousOn (↑(map (C := C) (D := D) n j) : (Fin n → ℝ) → X) (closedBall 0 1)
Tactic: rw [closure_ball 0 (by exact one_ne_zero)]
-- 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
inst_1 : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed[t] A ↔
    (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (A ∩ D)
have refine : IsClosed[t] A →
  (∀ (n : ℕ) (j : @cell _ t C D _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := D) n j)) ∧ IsClosed[t] (A ∩ D)
Tactic: refine ⟨?_, closed' A asubc⟩
-- 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
inst_1 : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed[t] A ↔ ∀ (n : ℕ) (j : @cell _ t C ∅ _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := ∅) n j)
have this : IsClosed[t] A ↔
  (∀ (n : ℕ) (j : @cell _ t C ∅ _ n), IsClosed[t] (A ∩ closedCell (C := C) (D := ∅) n j)) ∧ IsClosed[t] (A ∩ ∅)
Tactic: have := RelCWComplex.closed C A asubc
-- 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 : ℕ
j : @cell _ t C D _ n
⊢ closedCell (C := C) (D := D) n j ⊆ C
have simp_rw : closedCell (C := C) (D := D) n j ⊆ 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 : Set X
inst : CWComplex C
n : ℕ
hn : n ≠ 0
j : @cell _ t C ∅ _ n
this : NeZero n := ⋯
⊢ (cellFrontier (C := C) (D := ∅) n j).Nonempty
have h : (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1) ∈
  cellFrontier (C := C) (D := ∅) n j
Tactic: use map n j (Pi.single 0 1)
-- 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
n : ℕ
hn : n ≠ 0
j : @cell _ t C ∅ _ n
this : NeZero n := ⋯
⊢ (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1) ∈
    cellFrontier (C := C) (D := ∅) n j
have h : ∃ (x : Fin n → ℝ),
  ‖x‖ = 1 ∧
    (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) x =
      (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1)
Tactic: simp only [cellFrontier, mem_image, mem_sphere_iff_norm, sub_zero]
-- 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
n : ℕ
hn : n ≠ 0
j : @cell _ t C ∅ _ n
this : NeZero n := ⋯
⊢ ∃ (x : Fin n → ℝ),
    ‖x‖ = 1 ∧
      (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) x =
        (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1)
have w : Fin n → ℝ
Tactic: use Pi.single 0 1, by simp [Pi.norm_single]
-- 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
n : ℕ
hn : n ≠ 0
j : @cell _ t C ∅ _ n
this : NeZero n := ⋯
w : Fin n → ℝ
⊢ ∃ (x : Fin n → ℝ),
    ‖x‖ = 1 ∧
      (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) x =
        (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1)
have left : norm (E := Fin n → ℝ) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1) = 1
Tactic: use Pi.single 0 1, by simp [Pi.norm_single]
-- 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
n : ℕ
hn : n ≠ 0
j : @cell _ t C ∅ _ n
this : NeZero n := ⋯
w : Fin n → ℝ
left : norm (E := Fin n → ℝ) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1) = 1
⊢ ∃ (x : Fin n → ℝ),
    ‖x‖ = 1 ∧
      (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) x =
        (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1)
have right : (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1) =
  (↑(map (C := C) (D := ∅) n j) : (Fin n → ℝ) → X) (Pi.single (M := fun (a : Fin n) ↦ ℝ) 0 1)
Tactic: use Pi.single 0 1, by simp [Pi.norm_single]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Basic (goal)
Goal:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst : RelCWComplex C D
x z : @cell _ t C D _ 0
h :
  Eq.{u_1 + 1} (α := X) ((fun (x : @cell _ t C D _ 0) ↦ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![]) x)
    ((fun (x : @cell _ t C D _ 0) ↦ (↑(map (C := C) (D := D) 0 x) : (Fin 0 → ℝ) → X) ![]) z)
⊢ x = z
have by_contra : ∀ (hne : ¬x = z), False
Tactic: by_contra hne