awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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 ∩ {∞}ᶜ

Tactic:
⟨_, (isOpen_iff_of_mem hs).mp hso, ?_⟩

Premises used: OnePoint.isOpen_iff_of_mem, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen[instTopologicalSpace] s
refine_1 : some '' (some ⁻¹' s)ᶜᶜ ⊆ s ∩ {∞}ᶜ
⊢ ∃ (i' : Set X), (IsClosed[inst] i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ s ∩ {∞}ᶜ

Tactic:
refine ⟨_, (isOpen_iff_of_mem hs).mp hso, ?_⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen[instTopologicalSpace] s
⊢ some '' (some ⁻¹' s)ᶜᶜ ⊆ s ∩ {∞}ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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ᶜ

Tactic:
⟨_, ⟨mem_compl infty_notMem_image_coe, isOpen_compl_image_coe.2 ⟨h₁, h₂⟩⟩, ?_⟩

Premises used: Iff.mpr, OnePoint.infty_notMem_image_coe, And.intro, Exists.intro, OnePoint.isOpen_compl_image_coe, Set.mem_compl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h₁ : IsClosed[inst] s
h₂ : IsCompact s
refine_2 : (some '' s)ᶜ ∩ {∞}ᶜ ⊆ some '' sᶜ
⊢ ∃ (i : Set (OnePoint X)), (∞ ∈ i ∧ IsOpen[instTopologicalSpace] i) ∧ i ∩ {∞}ᶜ ⊆ some '' sᶜ

Tactic:
refine ⟨_, ⟨mem_compl infty_notMem_image_coe, isOpen_compl_image_coe.2 ⟨h₁, h₂⟩⟩, ?_⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h₁ : IsClosed[inst] s
h₂ : IsCompact s
⊢ (some '' s)ᶜ ∩ {∞}ᶜ ⊆ some '' sᶜ

Tactic:
simp [compl_image_coe, ← diff_eq]

Premises used: Set.diff_eq, OnePoint.compl_image_coe
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : NoncompactSpace X
rw : (map some (coclosedCompact X)).NeBot
⊢ NeBot (α := OnePoint X) (𝓝[≠] ∞)

Tactic:
rw [nhdsNE_infty_eq]

Premises used: OnePoint.nhdsNE_infty_eq
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : NoncompactSpace X
⊢ (map some (coclosedCompact X)).NeBot

Tactic:
infer_instance
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : ∀ (x : X), (𝓝[≠] x).NeBot
inst_2 : NoncompactSpace X
x : OnePoint X
⊢ (𝓝[≠] x).NeBot

Tactic:
OnePoint.rec OnePoint.nhdsNE_infty_neBot (fun y => OnePoint.nhdsNE_coe_neBot y) x

Premises used: OnePoint.rec
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
rw : Eq (α := Filter (OnePoint X)) (𝓝 ∞) (𝓝[≠] ∞ ⊔ pure ∞)
rw₁ rw₂ : Eq.{u_1 + 1} (α := Filter (OnePoint X)) (𝓝 ∞) (𝓝 ∞)
⊢ 𝓝 ∞ = map some (coclosedCompact X) ⊔ pure ∞

Tactic:
rw [← nhdsNE_infty_eq, nhdsNE_sup_pure]

Premises used: OnePoint.nhdsNE_infty_eq, nhdsNE_sup_pure
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
rw : Tendsto some (coclosedCompact X) (map some (coclosedCompact X) ⊔ pure ∞)
⊢ Tendsto some (coclosedCompact X) (𝓝 ∞)

Tactic:
rw [nhds_infty_eq]

Premises used: OnePoint.nhds_infty_eq
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Tendsto some (coclosedCompact X) (map some (coclosedCompact X) ⊔ pure ∞)

Tactic:
Filter.Tendsto.mono_right tendsto_map le_sup_left

Premises used: le_sup_left, Filter.tendsto_map, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Tendsto some (coclosedCompact X) (map some (coclosedCompact X) ⊔ pure ∞)

Tactic:
exact Filter.Tendsto.mono_right tendsto_map le_sup_left

Premises used: le_sup_left, Filter.tendsto_map, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
rw :
  (map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) fun (s : Set X) ↦
    some '' sᶜ ∪ {∞}
⊢ HasBasis (α := OnePoint X) (𝓝 ∞) (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) fun (s : Set X) ↦ some '' sᶜ ∪ {∞}

Tactic:
rw [nhds_infty_eq]

Premises used: OnePoint.nhds_infty_eq
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ (map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) fun (s : Set X) ↦
    some '' sᶜ ∪ {∞}

Tactic:
(hasBasis_coclosedCompact.map _).sup_pure _

Premises used: Filter.hasBasis_coclosedCompact, Filter.HasBasis.map, Filter.HasBasis.sup_pure
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ (map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) fun (s : Set X) ↦
    some '' sᶜ ∪ {∞}

Tactic:
exact (hasBasis_coclosedCompact.map _).sup_pure _

Premises used: Filter.hasBasis_coclosedCompact, Filter.HasBasis.map, Filter.HasBasis.sup_pure
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ comap some (𝓝 ∞) = coclosedCompact X

Tactic:
simp [nhds_infty_eq, comap_sup, comap_map coe_injective]

Premises used: OnePoint.coe_injective, Filter.comap_map, Filter.comap_sup, OnePoint.nhds_infty_eq
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
f : Filter (OnePoint X)
⊢ f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed[inst] s → IsCompact s → some '' sᶜ ∪ {∞} ∈ f

Tactic:
simp only [hasBasis_nhds_infty.ge_iff, and_imp]

Premises used: and_imp, Filter.HasBasis.ge_iff, OnePoint.hasBasis_nhds_infty
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
f : Ultrafilter (OnePoint X)
⊢ (↑f : Filter (OnePoint X)) ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed[inst] s → IsCompact s → some '' s ∉ f

Tactic:
simp only [le_nhds_infty, ← compl_image_coe, Ultrafilter.mem_coe,
    Ultrafilter.compl_mem_iff_notMem]

Premises used: OnePoint.compl_image_coe, Ultrafilter.compl_mem_iff_notMem, Ultrafilter.mem_coe, OnePoint.le_nhds_infty
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_3
f : OnePoint X → α
l : Filter α
⊢ Tendsto f (𝓝 ∞) l ↔ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l

Tactic:
simp [nhds_infty_eq, and_comm]

Premises used: and_comm, OnePoint.nhds_infty_eq
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
α : Type u_3
f : OnePoint X → α
l : Filter α
⊢ Tendsto f (pure ∞) l ∧ Tendsto (f ∘ some) (coclosedCompact X) l ↔
    ∀ s ∈ l, f ∞ ∈ s ∧ ∃ (t : Set X), IsClosed[inst] t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s

Tactic:
simp only [tendsto_pure_left, hasBasis_coclosedCompact.tendsto_left_iff, forall_and,
      and_assoc]

Premises used: Filter.tendsto_pure_left, Filter.hasBasis_coclosedCompact, and_assoc, Filter.HasBasis.tendsto_left_iff, forall_and
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
f : OnePoint X → Y
⊢ ContinuousAt f ∞ ↔ Tendsto (f ∘ some) (coclosedCompact X) (𝓝 (f ∞))

Tactic:
tendsto_nhds_infty'.trans <| and_iff_right (tendsto_pure_nhds _ _)

Premises used: ContinuousAt, and_iff_right, tendsto_pure_nhds, Iff.trans, OnePoint.tendsto_nhds_infty'
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
f : OnePoint X → Y
⊢ Tendsto (f ∘ some) (coclosedCompact X) (𝓝 (f ∞)) ↔
    ∀ s ∈ 𝓝 (f ∞), ∃ (t : Set X), IsClosed[inst] t ∧ IsCompact t ∧ MapsTo (f ∘ some) tᶜ s

Tactic:
simp only [hasBasis_coclosedCompact.tendsto_left_iff, and_assoc]

Premises used: Filter.hasBasis_coclosedCompact, and_assoc, Filter.HasBasis.tendsto_left_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
f : OnePoint X → Y
x : X
rw : Tendsto (f ∘ some) (𝓝 x) (𝓝 (f (↑x : OnePoint X))) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))
⊢ ContinuousAt f (↑x : OnePoint X) ↔ ContinuousAt (f ∘ some) x

Tactic:
rw [ContinuousAt, nhds_coe_eq, tendsto_map'_iff, ContinuousAt]

Premises used: ContinuousAt, Filter.tendsto_map'_iff, OnePoint.nhds_coe_eq
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
f : OnePoint X → Y
x : X
⊢ Tendsto (f ∘ some) (𝓝 x) (𝓝 (f (↑x : OnePoint X))) ↔ Tendsto (f ∘ some) (𝓝 x) (𝓝 ((f ∘ some) x))

Tactic:
rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
f : OnePoint X → Y
⊢ Continuous[instTopologicalSpace, inst_1] f ↔
    Tendsto (fun (x : X) ↦ f (↑x : OnePoint X)) (coclosedCompact X) (𝓝 (f ∞)) ∧
      Continuous[inst, inst_1] fun (x : X) ↦ f (↑x : OnePoint X)

Tactic:
simp only [continuous_iff_continuousAt, OnePoint.forall, continuousAt_coe, continuousAt_infty',
    Function.comp_def]

Premises used: Function.comp_def, OnePoint.continuousAt_infty', OnePoint.continuousAt_coe, OnePoint.forall, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)
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)
⊢ Continuous[instTopologicalSpace, inst_1] fun (x : OnePoint X) ↦ x.elim y (⇑f : (a : X) → Y)

Tactic:
rw [continuous_iff]

Premises used: OnePoint.continuous_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)
⊢ 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:
⟨h, f.continuous⟩

Premises used: ContinuousMap.continuous, And.intro
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)
⊢ 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:
refine ⟨h, f.continuous⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
inst_2 : DiscreteTopology X
f : OnePoint X → Y
⊢ Continuous[instTopologicalSpace, inst_1] f ↔ Tendsto (fun (x : X) ↦ f (↑x : OnePoint X)) cofinite (𝓝 (f ∞))

Tactic:
simp [continuous_iff, cocompact_eq_cofinite, continuous_of_discreteTopology]

Premises used: OnePoint.continuous_iff, Filter.cocompact_eq_cofinite, continuous_of_discreteTopology
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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
inst_2 : DiscreteTopology X
f : X → Y
y : Y
h : Tendsto f cofinite (𝓝 y)
⊢ Tendsto (⇑{ toFun := f, continuous_toFun := ⋯ } : (a : X) → Y) (coclosedCompact X) (𝓝 y)

Tactic:
simpa [cocompact_eq_cofinite]

Premises used: Filter.cocompact_eq_cofinite
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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
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)) ⋯
                      | 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)
⊢ (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

Tactic:
ext x
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)

Tactic:
OnePoint.rec ?_ ?_ x

Premises used: OnePoint.rec
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)

Tactic:
tendsto_nhds_unique ?_ (continuous_iff_from_discrete _ |>.mp <| map_continuous f)

Premises used: OnePoint.continuous_iff_from_discrete, Iff.mp, ContinuousMapClass.map_continuous, tendsto_nhds_unique
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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
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)) ⋯
                      | 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)
          ∞) :
      Filter Y)
⊢ 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)

Tactic:
refine tendsto_nhds_unique ?_ (continuous_iff_from_discrete _ |>.mp <| map_continuous f)

Premises used: OnePoint.continuous_iff_from_discrete, Iff.mp, ContinuousMapClass.map_continuous, tendsto_nhds_unique
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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
f' : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) } :=
  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)) ⋯
⊢ 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)) ⋯
                      | 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)
          ∞) :
      Filter Y)

Tactic:
Classical.choose_spec f'.property

Premises used: Classical.choose_spec, Classical.choose, Subtype.property
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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
f' : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) } :=
  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)) ⋯
⊢ 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)) ⋯
                      | 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)
          ∞) :
      Filter Y)

Tactic:
exact Classical.choose_spec f'.property

Premises used: Classical.choose_spec, Subtype.property