awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen[inst] (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen[inst] (some ⁻¹' t)
⊢ (∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ) ∧ IsOpen[inst] (some ⁻¹' (s ∩ t))
have refine : ∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ
Tactic: refine ⟨?_, hs.inter ht⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ t ∈ S, (∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ) ∧ IsOpen[inst] (some ⁻¹' t)
this : IsOpen[inst] (some ⁻¹' ⋃₀ S)
⊢ (∞ ∈ ⋃₀ S → IsCompact (some ⁻¹' ⋃₀ S)ᶜ) ∧ IsOpen[inst] (some ⁻¹' ⋃₀ S)
have refine : ∞ ∈ ⋃₀ S → IsCompact (some ⁻¹' ⋃₀ S)ᶜ
Tactic: refine ⟨?_, this⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ t ∈ S, (∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ) ∧ IsOpen[inst] (some ⁻¹' t)
this : IsOpen[inst] (some ⁻¹' ⋃₀ S)
s : Set (OnePoint X)
hsS : s ∈ S
hs : ∞ ∈ s
⊢ IsCompact (some ⁻¹' ⋃₀ S)ᶜ
have refine : (some ⁻¹' ⋃₀ S)ᶜ ⊆ (some ⁻¹' s)ᶜ
Tactic: refine IsCompact.of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl ?_
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ t ∈ S, (∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ) ∧ IsOpen[inst] (some ⁻¹' t)
⊢ (∞ ∈ ⋃₀ S → IsCompact (some ⁻¹' ⋃₀ S)ᶜ) ∧ IsOpen[inst] (some ⁻¹' ⋃₀ S)
have suffices : IsOpen[inst] (some ⁻¹' ⋃₀ S)
Tactic: suffices IsOpen ((↑) ⁻¹' ⋃₀ S : Set X) by
      refine ⟨?_, this⟩
      rintro ⟨s, hsS : s ∈ S, hs : ∞ ∈ s⟩
      refine IsCompact.of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl ?_
      exact compl_subset_compl.mpr (preimage_mono <| subset_sUnion_of_mem hsS)
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
S : Set (Set (OnePoint X))
ho : ∀ t ∈ S, (∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ) ∧ IsOpen[inst] (some ⁻¹' t)
⊢ IsOpen[inst] (some ⁻¹' ⋃₀ S)
have rw : IsOpen[inst] (⋃ t ∈ S, some ⁻¹' t)
Tactic: rw [preimage_sUnion]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s)
have this : ∞ ∉ sᶜ
Tactic: have : ∞ ∉ sᶜ := fun H => H h
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
this : ∞ ∉ sᶜ
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s)
have rw : IsOpen[instTopologicalSpace] sᶜ ↔ IsClosed[inst] (some ⁻¹' s)
Tactic: rw [← isOpen_compl_iff, isOpen_iff_of_notMem this, ← isOpen_compl_iff, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
this : ∞ ∉ sᶜ
rw : IsOpen[instTopologicalSpace] sᶜ ↔ IsClosed[inst] (some ⁻¹' s)
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s)
have rw₁ : IsOpen[inst] (some ⁻¹' sᶜ) ↔ IsClosed[inst] (some ⁻¹' s)
Tactic: rw [← isOpen_compl_iff, isOpen_iff_of_notMem this, ← isOpen_compl_iff, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
this : ∞ ∉ sᶜ
rw : IsOpen[instTopologicalSpace] sᶜ ↔ IsClosed[inst] (some ⁻¹' s)
rw₁ : IsOpen[inst] (some ⁻¹' sᶜ) ↔ IsClosed[inst] (some ⁻¹' s)
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s)
have rw₂ : IsOpen[inst] (some ⁻¹' sᶜ) ↔ IsOpen[inst] (some ⁻¹' s)ᶜ
Tactic: rw [← isOpen_compl_iff, isOpen_iff_of_notMem this, ← isOpen_compl_iff, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
this : ∞ ∉ sᶜ
rw : IsOpen[instTopologicalSpace] sᶜ ↔ IsClosed[inst] (some ⁻¹' s)
rw₁ : IsOpen[inst] (some ⁻¹' sᶜ) ↔ IsClosed[inst] (some ⁻¹' s)
rw₂ : IsOpen[inst] (some ⁻¹' sᶜ) ↔ IsOpen[inst] (some ⁻¹' s)ᶜ
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s)
have rw₃ : IsOpen[inst] (some ⁻¹' s)ᶜ ↔ IsOpen[inst] (some ⁻¹' s)ᶜ
Tactic: rw [← isOpen_compl_iff, isOpen_iff_of_notMem this, ← isOpen_compl_iff, preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∉ s
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
have rw : IsOpen[instTopologicalSpace] sᶜ ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
Tactic: rw [← isOpen_compl_iff, isOpen_iff_of_mem (mem_compl h), ← preimage_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∉ s
rw : IsOpen[instTopologicalSpace] sᶜ ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
have rw₁ : IsClosed[inst] (some ⁻¹' sᶜ)ᶜ ∧ IsCompact (some ⁻¹' sᶜ)ᶜ ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
Tactic: rw [← isOpen_compl_iff, isOpen_iff_of_mem (mem_compl h), ← preimage_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∉ s
rw : IsOpen[instTopologicalSpace] sᶜ ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
rw₁ : IsClosed[inst] (some ⁻¹' sᶜ)ᶜ ∧ IsCompact (some ⁻¹' sᶜ)ᶜ ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
have rw₂ : IsClosed[inst] (some ⁻¹' sᶜᶜ) ∧ IsCompact (some ⁻¹' sᶜᶜ) ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
Tactic: rw [← isOpen_compl_iff, isOpen_iff_of_mem (mem_compl h), ← preimage_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∉ s
rw : IsOpen[instTopologicalSpace] sᶜ ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
rw₁ : IsClosed[inst] (some ⁻¹' sᶜ)ᶜ ∧ IsCompact (some ⁻¹' sᶜ)ᶜ ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
rw₂ : IsClosed[inst] (some ⁻¹' sᶜᶜ) ∧ IsCompact (some ⁻¹' sᶜᶜ) ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
have rw₃ : IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s) ↔ IsClosed[inst] (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)
Tactic: rw [← isOpen_compl_iff, isOpen_iff_of_mem (mem_compl h), ← preimage_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsOpen[instTopologicalSpace] (some '' s) ↔ IsOpen[inst] s
have rw : IsOpen[inst] (some ⁻¹' some '' s) ↔ IsOpen[inst] s
Tactic: rw [isOpen_iff_of_notMem infty_notMem_image_coe, preimage_image_eq _ coe_injective]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : IsOpen[inst] (some ⁻¹' some '' s) ↔ IsOpen[inst] s
⊢ IsOpen[instTopologicalSpace] (some '' s) ↔ IsOpen[inst] s
have rw₁ : IsOpen[inst] s ↔ IsOpen[inst] s
Tactic: rw [isOpen_iff_of_notMem infty_notMem_image_coe, preimage_image_eq _ coe_injective]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsOpen[instTopologicalSpace] (some '' s)ᶜ ↔ IsClosed[inst] s ∧ IsCompact s
have rw : ∞ ∈ (some '' s)ᶜ
Tactic: rw [isOpen_iff_of_mem, ← preimage_compl, compl_compl, preimage_image_eq _ coe_injective]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsClosed[instTopologicalSpace] (some '' s) ↔ IsClosed[inst] s ∧ IsCompact s
have rw : IsOpen[instTopologicalSpace] (some '' s)ᶜ ↔ IsClosed[inst] s ∧ IsCompact s
Tactic: rw [← isOpen_compl_iff, isOpen_compl_image_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : IsOpen[instTopologicalSpace] (some '' s)ᶜ ↔ IsClosed[inst] s ∧ IsCompact s
⊢ IsClosed[instTopologicalSpace] (some '' s) ↔ IsClosed[inst] s ∧ IsCompact s
have rw₁ : IsClosed[inst] s ∧ IsCompact s ↔ IsClosed[inst] s ∧ IsCompact s
Tactic: rw [← isOpen_compl_iff, isOpen_compl_image_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsClosed[instTopologicalSpace] {∞}
have rw : IsOpen[instTopologicalSpace] (range some)
Tactic: rw [← compl_range_coe, isClosed_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ 𝓝[≠] ∞ = map some (coclosedCompact X)
have refine_1 : ∀ (i : Set (OnePoint X)),
  ∞ ∈ i ∧ IsOpen[instTopologicalSpace] i → ∃ (i' : Set X), (IsClosed[inst] i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ
Tactic: refine (nhdsWithin_basis_open ∞ _).ext (hasBasis_coclosedCompact.map _) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
refine_1 :
  ∀ (i : Set (OnePoint X)),
    ∞ ∈ i ∧ IsOpen[instTopologicalSpace] i → ∃ (i' : Set X), (IsClosed[inst] i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ
⊢ 𝓝[≠] ∞ = map some (coclosedCompact X)
have refine_2 : ∀ (i' : Set X),
  IsClosed[inst] i' ∧ IsCompact i' →
    ∃ (i : Set (OnePoint X)), (∞ ∈ i ∧ IsOpen[instTopologicalSpace] i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ
Tactic: refine (nhdsWithin_basis_open ∞ _).ext (hasBasis_coclosedCompact.map _) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen[instTopologicalSpace] s
⊢ ∃ (i' : Set X), (IsClosed[inst] i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ s ∩ {∞}ᶜ
have refine_1 : some '' (some ⁻¹' s)ᶜᶜ ⊆ s ∩ {∞}ᶜ
Tactic: refine ⟨_, (isOpen_iff_of_mem hs).mp hso, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h₁ : IsClosed[inst] s
h₂ : IsCompact s
⊢ ∃ (i : Set (OnePoint X)), (∞ ∈ i ∧ IsOpen[instTopologicalSpace] i) ∧ i ∩ {∞}ᶜ ⊆ some '' sᶜ
have refine_2 : (some '' s)ᶜ ∩ {∞}ᶜ ⊆ some '' sᶜ
Tactic: refine ⟨_, ⟨mem_compl infty_notMem_image_coe, isOpen_compl_image_coe.2 ⟨h₁, h₂⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : NoncompactSpace X
⊢ NeBot (α := OnePoint X) (𝓝[≠] ∞)
have rw : (map some (coclosedCompact X)).NeBot
Tactic: rw [nhdsNE_infty_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ 𝓝 ∞ = map some (coclosedCompact X) ⊔ pure ∞
have rw : Eq (α := Filter (OnePoint X)) (𝓝 ∞) (𝓝[≠] ∞ ⊔ pure ∞)
Tactic: rw [← nhdsNE_infty_eq, nhdsNE_sup_pure]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
rw : Eq (α := Filter (OnePoint X)) (𝓝 ∞) (𝓝[≠] ∞ ⊔ pure ∞)
⊢ 𝓝 ∞ = map some (coclosedCompact X) ⊔ pure ∞
have rw₁ : Eq.{u_1 + 1} (α := Filter (OnePoint X)) (𝓝 ∞) (𝓝 ∞)
Tactic: rw [← nhdsNE_infty_eq, nhdsNE_sup_pure]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Tendsto some (coclosedCompact X) (𝓝 ∞)
have rw : Tendsto some (coclosedCompact X) (map some (coclosedCompact X) ⊔ pure ∞)
Tactic: rw [nhds_infty_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ HasBasis (α := OnePoint X) (𝓝 ∞) (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) fun (s : Set X) ↦ some '' sᶜ ∪ {∞}
have rw : (map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) fun (s : Set X) ↦
  some '' sᶜ ∪ {∞}
Tactic: rw [nhds_infty_eq]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ ContinuousAt f (↑x : OnePoint X) ↔ ContinuousAt (f ∘ some) x
have rw : Tendsto (f ∘ some) (𝓝 x) (𝓝 (f (↑x : OnePoint X))) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))
Tactic: rw [ContinuousAt, nhds_coe_eq, tendsto_map'_iff, ContinuousAt]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst_1 : TopologicalSpace Y
f : C(X, Y)
y : Y
h : Tendsto (⇑f : (a : X) → Y) (coclosedCompact X) (𝓝 y)
⊢ Continuous[instTopologicalSpace, inst_1] fun (x : OnePoint X) ↦ x.elim y (⇑f : (a : X) → Y)
have rw : Tendsto (fun (x : X) ↦ (↑x : OnePoint X).elim y (⇑f : (a : X) → Y)) (coclosedCompact X)
    (𝓝 (OnePoint.elim.{u_1, u_3} (X := X) ∞ y (⇑f : (a : X) → Y))) ∧
  Continuous[inst, inst_1] fun (x : X) ↦ (↑x : OnePoint X).elim y (⇑f : (a : X) → Y)
Tactic: rw [continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst_1 : DiscreteTopology X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
inst_4 : Infinite X
f : ContinuousMap.{u_1, u_3} (OnePoint X) Y
⊢ (fun (f : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }) ↦
        ({
            toFun := fun (x : OnePoint X) ↦
              match (motive := OnePoint X → Y) x with
              | none => Classical.choose (p := fun (x : Y) ↦ Tendsto (fun (x : X) ↦ (↑f : X → Y) x) cofinite (𝓝 x)) ⋯
              | Option.some x => (↑f : X → Y) x,
            continuous_toFun := ⋯ } :
          ContinuousMap.{u_1, u_3} (OnePoint X) Y))
      ((fun (f : ContinuousMap.{u_1, u_3} (OnePoint X) Y) ↦
          (Subtype.mk (p := fun (f : X → Y) ↦ ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L))
              (fun (x : X) ↦ (f : (a : OnePoint X) → Y) (↑x : OnePoint X)) ⋯ :
            { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }))
        f) =
    f
have h : ∀ (x : OnePoint X),
  Eq.{u_3 + 1} (α := Y)
    (((fun (f : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }) ↦
              ({
                  toFun := fun (x : OnePoint X) ↦
                    match (motive := OnePoint X → Y) x with
                    | none =>
                      Classical.choose (p := fun (x : Y) ↦ Tendsto (fun (x : X) ↦ (↑f : X → Y) x) cofinite (𝓝 x)) sorry
                    | Option.some x => (↑f : X → Y) x,
                  continuous_toFun := sorry } :
                ContinuousMap.{u_1, u_3} (OnePoint X) Y))
            ((fun (f : ContinuousMap.{u_1, u_3} (OnePoint X) Y) ↦
                (Subtype.mk (p := fun (f : X → Y) ↦ ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L))
                    (fun (x : X) ↦ (f : (a : OnePoint X) → Y) (↑x : OnePoint X)) sorry :
                  { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }))
              f) :
          (a : OnePoint X) → Y)
        x :
      Y)
    ((f : (a : OnePoint X) → Y) x : Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst_1 : DiscreteTopology X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
inst_4 : Infinite X
f : ContinuousMap.{u_1, u_3} (OnePoint X) Y
x : OnePoint X
⊢ Eq.{u_3 + 1} (α := Y)
    (((fun (f : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }) ↦
              ({
                  toFun := fun (x : OnePoint X) ↦
                    match (motive := OnePoint X → Y) x with
                    | none =>
                      Classical.choose (p := fun (x : Y) ↦ Tendsto (fun (x : X) ↦ (↑f : X → Y) x) cofinite (𝓝 x)) ⋯
                    | Option.some x => (↑f : X → Y) x,
                  continuous_toFun := ⋯ } :
                ContinuousMap.{u_1, u_3} (OnePoint X) Y))
            ((fun (f : ContinuousMap.{u_1, u_3} (OnePoint X) Y) ↦
                (Subtype.mk (p := fun (f : X → Y) ↦ ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L))
                    (fun (x : X) ↦ (f : (a : OnePoint X) → Y) (↑x : OnePoint X)) ⋯ :
                  { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }))
              f) :
          (a : OnePoint X) → Y)
        x :
      Y)
    ((f : (a : OnePoint X) → Y) x : Y)
have h : Eq.{u_3 + 1} (α := Y)
  (((fun (f : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }) ↦
            ({
                toFun := fun (x : OnePoint X) ↦
                  match (motive := OnePoint X → Y) x with
                  | none =>
                    Classical.choose (p := fun (x : Y) ↦ Tendsto (fun (x : X) ↦ (↑f : X → Y) x) cofinite (𝓝 x)) sorry
                  | Option.some x => (↑f : X → Y) x,
                continuous_toFun := sorry } :
              ContinuousMap.{u_1, u_3} (OnePoint X) Y))
          ((fun (f : ContinuousMap.{u_1, u_3} (OnePoint X) Y) ↦
              (Subtype.mk (p := fun (f : X → Y) ↦ ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L))
                  (fun (x : X) ↦ (f : (a : OnePoint X) → Y) (↑x : OnePoint X)) sorry :
                { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }))
            f) :
        (a : OnePoint X) → Y)
      ∞ :
    Y)
  ((f : (a : OnePoint X) → Y) ∞ : Y)
Tactic: refine OnePoint.rec ?_ ?_ x
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst_1 : DiscreteTopology X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
inst_4 : Infinite X
f : ContinuousMap.{u_1, u_3} (OnePoint X) Y
x : OnePoint X
⊢ Eq.{u_3 + 1} (α := Y)
    (((fun (f : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }) ↦
              ({
                  toFun := fun (x : OnePoint X) ↦
                    match (motive := OnePoint X → Y) x with
                    | none =>
                      Classical.choose (p := fun (x : Y) ↦ Tendsto (fun (x : X) ↦ (↑f : X → Y) x) cofinite (𝓝 x)) ⋯
                    | Option.some x => (↑f : X → Y) x,
                  continuous_toFun := ⋯ } :
                ContinuousMap.{u_1, u_3} (OnePoint X) Y))
            ((fun (f : ContinuousMap.{u_1, u_3} (OnePoint X) Y) ↦
                (Subtype.mk (p := fun (f : X → Y) ↦ ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L))
                    (fun (x : X) ↦ (f : (a : OnePoint X) → Y) (↑x : OnePoint X)) ⋯ :
                  { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }))
              f) :
          (a : OnePoint X) → Y)
        ∞ :
      Y)
    ((f : (a : OnePoint X) → Y) ∞ : Y)
have h : Tendsto.{u_1, u_3} (β := Y) (fun (x : X) ↦ ((f : (a : OnePoint X) → Y) (↑x : OnePoint X) : Y)) cofinite
  (𝓝
      (((fun (f : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }) ↦
              ({
                  toFun := fun (x : OnePoint X) ↦
                    match (motive := OnePoint X → Y) x with
                    | none =>
                      Classical.choose (p := fun (x : Y) ↦ Tendsto (fun (x : X) ↦ (↑f : X → Y) x) cofinite (𝓝 x)) sorry
                    | Option.some x => (↑f : X → Y) x,
                  continuous_toFun := sorry } :
                ContinuousMap.{u_1, u_3} (OnePoint X) Y))
            ((fun (f : ContinuousMap.{u_1, u_3} (OnePoint X) Y) ↦
                (Subtype.mk (p := fun (f : X → Y) ↦ ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L))
                    (fun (x : X) ↦ (f : (a : OnePoint X) → Y) (↑x : OnePoint X)) sorry :
                  { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }))
              f) :
          (a : OnePoint X) → Y)
        ∞) :
    Filter Y)
Tactic: refine tendsto_nhds_unique ?_ (continuous_iff_from_discrete _ |>.mp <| map_continuous f)
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
Y : Type u_3
inst : TopologicalSpace Y
f : OnePoint ℕ → Y
⊢ Continuous[_, inst] f ↔ Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) atTop (𝓝 (f ∞))
have rw : Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) cofinite (𝓝 (f ∞)) ↔
  Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) atTop (𝓝 (f ∞))
Tactic: rw [continuous_iff_from_discrete, Nat.cofinite_eq_atTop]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
Y : Type u_3
inst : TopologicalSpace Y
f : OnePoint ℕ → Y
rw :
  Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) cofinite (𝓝 (f ∞)) ↔
    Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) atTop (𝓝 (f ∞))
⊢ Continuous[_, inst] f ↔ Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) atTop (𝓝 (f ∞))
have rw₁ : Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) atTop (𝓝 (f ∞)) ↔
  Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) atTop (𝓝 (f ∞))
Tactic: rw [continuous_iff_from_discrete, Nat.cofinite_eq_atTop]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NoncompactSpace X
⊢ DenseRange.{u_1, u_1} (X := OnePoint X) some
have rw : Dense (X := OnePoint X) {∞}ᶜ
Tactic: rw [DenseRange, ← compl_infty]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : OnePoint X
⊢ Inseparable x y ↔
    x = ∞ ∧ y = ∞ ∨ ∃ (x' : X), x = (↑x' : OnePoint X) ∧ ∃ (y' : X), y = (↑y' : OnePoint X) ∧ Inseparable x' y'
have infty : Inseparable ∞ y ↔
  Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∧ y = ∞ ∨
    ∃ (x' : X), ∞ = (↑x' : OnePoint X) ∧ ∃ (y' : X), y = (↑y' : OnePoint X) ∧ Inseparable x' y'
Tactic: induction x using OnePoint.rec
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : OnePoint X
infty :
  Inseparable ∞ y ↔
    Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∧ y = ∞ ∨
      ∃ (x' : X), ∞ = (↑x' : OnePoint X) ∧ ∃ (y' : X), y = (↑y' : OnePoint X) ∧ Inseparable x' y'
⊢ Inseparable x y ↔
    x = ∞ ∧ y = ∞ ∨ ∃ (x' : X), x = (↑x' : OnePoint X) ∧ ∃ (y' : X), y = (↑y' : OnePoint X) ∧ Inseparable x' y'
have coe : ∀ (x : X),
  Inseparable (↑x : OnePoint X) y ↔
    (↑x : OnePoint X) = ∞ ∧ y = ∞ ∨
      ∃ (x' : X), (↑x : OnePoint X) = (↑x' : OnePoint X) ∧ ∃ (y' : X), y = (↑y' : OnePoint X) ∧ Inseparable x' y'
Tactic: induction x using OnePoint.rec
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
y : OnePoint X
⊢ Inseparable ∞ y ↔
    Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∧ y = ∞ ∨
      ∃ (x' : X), ∞ = (↑x' : OnePoint X) ∧ ∃ (y' : X), y = (↑y' : OnePoint X) ∧ Inseparable x' y'
have infty : Inseparable.{u_1} (X := OnePoint X) ∞ ∞ ↔
  Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∧ Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∨
    ∃ (x' : X), ∞ = (↑x' : OnePoint X) ∧ ∃ (y' : X), ∞ = (↑y' : OnePoint X) ∧ Inseparable x' y'
Tactic: induction y using OnePoint.rec
Cleared hypotheses: y