awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
y : OnePoint X
infty : Specializes.{u_1} (X := OnePoint X) ∞ ∞ ∨ Disjoint.{u_1} (α := Filter (OnePoint X)) (𝓝 ∞) (𝓝 ∞)
infty₁ : ∀ (x : X), ∞ ⤳ (↑x : OnePoint X) ∨ Disjoint (𝓝 ∞) (𝓝 (↑x : OnePoint X))
⊢ ∞ ⤳ y ∨ Disjoint (𝓝 ∞) (𝓝 y)

Tactic:
induction y using OnePoint.rec
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
y : OnePoint X
x : X
coe : (↑x : OnePoint X) ⤳ ∞ ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 ∞)
coe₁ : ∀ (x_1 : X), (↑x : OnePoint X) ⤳ (↑x_1 : OnePoint X) ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 (↑x_1 : OnePoint X))
⊢ (↑x : OnePoint X) ⤳ y ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 y)

Tactic:
induction y using OnePoint.rec
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
⊢ Specializes.{u_1} (X := OnePoint X) ∞ ∞ ∨ Disjoint.{u_1} (α := Filter (OnePoint X)) (𝓝 ∞) (𝓝 ∞)

Tactic:
.inl le_rfl

Premises used: le_rfl, Or.inl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
⊢ Specializes.{u_1} (X := OnePoint X) ∞ ∞ ∨ Disjoint.{u_1} (α := Filter (OnePoint X)) (𝓝 ∞) (𝓝 ∞)

Tactic:
exact .inl le_rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
x : X
⊢ ∞ ⤳ (↑x : OnePoint X) ∨ Disjoint (𝓝 ∞) (𝓝 (↑x : OnePoint X))

Tactic:
.inr (key _).symm

Premises used: Disjoint.symm, Or.inr
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
x : X
⊢ ∞ ⤳ (↑x : OnePoint X) ∨ Disjoint (𝓝 ∞) (𝓝 (↑x : OnePoint X))

Tactic:
exact .inr (key _).symm
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
x : X
⊢ (↑x : OnePoint X) ⤳ ∞ ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 ∞)

Tactic:
.inr (key _)

Premises used: Or.inr
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
x : X
⊢ (↑x : OnePoint X) ⤳ ∞ ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 ∞)

Tactic:
exact .inr (key _)
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
x x_1 : X
coe : x ⤳ x_1 ∨ Disjoint (𝓝 x) (𝓝 x_1)
⊢ (↑x : OnePoint X) ⤳ (↑x_1 : OnePoint X) ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 (↑x_1 : OnePoint X))

Tactic:
rw [nhds_coe_eq, nhds_coe_eq, disjoint_map coe_injective, specializes_coe]

Premises used: OnePoint.coe_injective, Filter.disjoint_map, OnePoint.nhds_coe_eq, OnePoint.specializes_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 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
key : ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)
x x_1 : X
⊢ x ⤳ x_1 ∨ Disjoint (𝓝 x) (𝓝 x_1)

Tactic:
apply specializes_or_disjoint_nhds

Premises used: R1Space.specializes_or_disjoint_nhds
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : T2Space X
⊢ T4Space.{u_1} (OnePoint X)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Infinite X
inst_2 : DiscreteTopology X
inhabit :
  ∀ (inhabited_h : Inhabited X),
    ¬Continuous[_, instTopologicalSpace]
        (⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X)
⊢ ¬Continuous[_, instTopologicalSpace]
      (⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X)

Tactic:
inhabit X
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Infinite X
inst_2 : DiscreteTopology X
inhabited_h : Inhabited X
simp :
  ∃ (x : CofiniteTopology (OnePoint X)),
    ¬Tendsto (β := OnePoint X)
        ((⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X) :
          (a : CofiniteTopology (OnePoint X)) → OnePoint X)
        (𝓝 x)
        (𝓝 ((Equiv.symm CofiniteTopology.of : (a : CofiniteTopology (OnePoint X)) → OnePoint X) x) :
          Filter (OnePoint X))
⊢ ¬Continuous[_, instTopologicalSpace]
      (⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X)

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt, not_forall]

Premises used: ContinuousAt, Classical.not_forall, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Infinite X
inst_2 : DiscreteTopology X
inhabited_h : Inhabited X
h :
  ¬Tendsto.{u_1, u_1} (α := CofiniteTopology (OnePoint X)) (β := OnePoint X)
      ((⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X) :
        (a : CofiniteTopology (OnePoint X)) → OnePoint X)
      (𝓝 ((CofiniteTopology.of : (a : OnePoint X) → CofiniteTopology (OnePoint X)) (↑default : OnePoint X)) :
        Filter (CofiniteTopology (OnePoint X)))
      (𝓝
          ((Equiv.symm CofiniteTopology.of : (a : CofiniteTopology (OnePoint X)) → OnePoint X)
            ((CofiniteTopology.of : (a : OnePoint X) → CofiniteTopology (OnePoint X)) (↑default : OnePoint X) :
              CofiniteTopology (OnePoint X))) :
        Filter (OnePoint X))
⊢ ∃ (x : CofiniteTopology (OnePoint X)),
    ¬Tendsto (β := OnePoint X)
        ((⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X) :
          (a : CofiniteTopology (OnePoint X)) → OnePoint X)
        (𝓝 x)
        (𝓝 ((Equiv.symm CofiniteTopology.of : (a : CofiniteTopology (OnePoint X)) → OnePoint X) x) :
          Filter (OnePoint X))

Tactic:
use CofiniteTopology.of ↑(default : X)

Premises used: CofiniteTopology.of, DFunLike.coe
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Infinite X
inst_2 : DiscreteTopology X
inhabited_h : Inhabited X
⊢ ¬Tendsto.{u_1, u_1} (α := CofiniteTopology (OnePoint X)) (β := OnePoint X)
      ((⇑(Equiv.symm CofiniteTopology.of) : (a : CofiniteTopology (OnePoint X)) → OnePoint X) :
        (a : CofiniteTopology (OnePoint X)) → OnePoint X)
      (𝓝 ((CofiniteTopology.of : (a : OnePoint X) → CofiniteTopology (OnePoint X)) (↑default : OnePoint X)) :
        Filter (CofiniteTopology (OnePoint X)))
      (𝓝
          ((Equiv.symm CofiniteTopology.of : (a : CofiniteTopology (OnePoint X)) → OnePoint X)
            ((CofiniteTopology.of : (a : OnePoint X) → CofiniteTopology (OnePoint X)) (↑default : OnePoint X) :
              CofiniteTopology (OnePoint X))) :
        Filter (OnePoint X))

Tactic:
simpa [nhds_coe_eq, nhds_discrete, CofiniteTopology.nhds_eq, Equiv.symm_apply_eq]
    using (finite_singleton _).infinite_compl

Premises used: CofiniteTopology.nhds_eq, Equiv.symm_apply_eq, OnePoint.nhds_coe_eq, Set.Finite.infinite_compl, nhds_discrete, Set.finite_singleton
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
h_1 : Membership.mem (γ := Set (OnePoint X)) univ ∞
hxy : ∞ ≠ y
⊢ ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
    IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ ∞ ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
⟨{y}ᶜ, {y}, isOpen_compl_singleton, ?_, hxy, rfl, (compl_union_self _).symm.subset,
        disjoint_compl_left⟩

Premises used: Compl.compl, disjoint_compl_left, isOpen_compl_singleton, Eq.subset, And.intro, Exists.intro, Set.compl_union_self, Singleton.singleton, Eq.symm, rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
h_1 : Membership.mem (γ := Set (OnePoint X)) univ ∞
hxy : ∞ ≠ y
infty : IsOpen[instTopologicalSpace] {y}
⊢ ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
    IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ ∞ ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
refine ⟨{y}ᶜ, {y}, isOpen_compl_singleton, ?_, hxy, rfl, (compl_union_self _).symm.subset,
        disjoint_compl_left⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
h_1 : Membership.mem (γ := Set (OnePoint X)) univ ∞
hxy : ∞ ≠ y
infty : IsOpen[inst_1] (some ⁻¹' {y})
infty₁ : ∞ ∉ {y}
⊢ IsOpen[instTopologicalSpace] {y}

Tactic:
rw [OnePoint.isOpen_iff_of_notMem]

Premises used: OnePoint.isOpen_iff_of_notMem
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
h_1 : Membership.mem (γ := Set (OnePoint X)) univ ∞
hxy : ∞ ≠ y
⊢ IsOpen[inst_1] (some ⁻¹' {y})

Tactic:
isOpen_discrete _

Premises used: isOpen_discrete
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
h_1 : Membership.mem (γ := Set (OnePoint X)) univ ∞
hxy : ∞ ≠ y
⊢ ∞ ∉ {y}

Tactic:
hxy

Premises used: Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
h_1 : Membership.mem (γ := Set (OnePoint X)) univ ∞
hxy : ∞ ≠ y
⊢ IsOpen[inst_1] (some ⁻¹' {y})

Tactic:
exacts [isOpen_discrete _, hxy]

Premises used: isOpen_discrete
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
val : X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X)
hxy : (↑val : OnePoint X) ≠ y
⊢ Subset (α := Set (OnePoint X)) univ ({(↑val : OnePoint X)} ∪ {(↑val : OnePoint X)}ᶜ)

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
val : X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X)
hxy : (↑val : OnePoint X) ≠ y
coe : IsOpen[instTopologicalSpace] {(↑val : OnePoint X)}
⊢ ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
    IsOpen[instTopologicalSpace] u ∧
      IsOpen[instTopologicalSpace] v ∧ (↑val : OnePoint X) ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
refine ⟨{some val}, {some val}ᶜ, ?_, isOpen_compl_singleton, rfl, hxy.symm, by simp,
        disjoint_compl_right⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
val : X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X)
hxy : (↑val : OnePoint X) ≠ y
coe : IsOpen[inst_1] (some ⁻¹' {(↑val : OnePoint X)})
coe₁ : ∞ ∉ {(↑val : OnePoint X)}
⊢ IsOpen[instTopologicalSpace] {(↑val : OnePoint X)}

Tactic:
rw [OnePoint.isOpen_iff_of_notMem]

Premises used: OnePoint.isOpen_iff_of_notMem
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
val : X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X)
hxy : (↑val : OnePoint X) ≠ y
⊢ IsOpen[inst_1] (some ⁻¹' {(↑val : OnePoint X)})

Tactic:
isOpen_discrete _

Premises used: isOpen_discrete
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
val : X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X)
hxy : (↑val : OnePoint X) ≠ y
⊢ ∞ ∉ {(↑val : OnePoint X)}

Tactic:
(Option.some_ne_none val).symm

Premises used: OnePoint.infty, Set.Mem, setOf, OnePoint.some, Ne.symm, Set.singleton, Option.some_ne_none, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
y : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ y
val : X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X)
hxy : (↑val : OnePoint X) ≠ y
⊢ IsOpen[inst_1] (some ⁻¹' {(↑val : OnePoint X)})

Tactic:
exacts [isOpen_discrete _, (Option.some_ne_none val).symm]

Premises used: Ne.symm, isOpen_discrete, Option.some_ne_none
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
s : Set (OnePoint X_1)
X : Type u_3
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
x : OnePoint X
h : Membership.mem (γ := Set (OnePoint X)) univ x
y : OnePoint X
h_1 : Membership.mem (γ := Set (OnePoint X)) univ y
hxy : x ≠ y
infty :
  Membership.mem (γ := Set (OnePoint X)) univ ∞ →
    ∀ (hxy : ∞ ≠ y),
      ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
        IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ ∞ ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
coe :
  ∀ (val : X),
    Membership.mem (γ := Set (OnePoint X)) univ (↑val : OnePoint X) →
      ∀ (hxy : (↑val : OnePoint X) ≠ y),
        ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
          IsOpen[instTopologicalSpace] u ∧
            IsOpen[instTopologicalSpace] v ∧ (↑val : OnePoint X) ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
⊢ ∃ (u : Set (OnePoint X)) (v : Set (OnePoint X)),
    IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
cases x with
    | infty =>
      refine ⟨{y}ᶜ, {y}, isOpen_compl_singleton, ?_, hxy, rfl, (compl_union_self _).symm.subset,
        disjoint_compl_left⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, hxy]
    | coe val =>
      refine ⟨{some val}, {some val}ᶜ, ?_, isOpen_compl_singleton, rfl, hxy.symm, by simp,
        disjoint_compl_right⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, (Option.some_ne_none val).symm]

Premises used: OnePoint.infty, OnePoint.isOpen_iff_of_notMem, isOpen_discrete
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
rw : ∀ t ∈ 𝓝 y, ∃ (i : Set X), IsCompact i ∧ MapsTo f iᶜ t
⊢ Tendsto f (coclosedCompact X) (𝓝 y)

Tactic:
rw [coclosedCompact_eq_cocompact, hasBasis_cocompact.tendsto_left_iff]

Premises used: Filter.coclosedCompact_eq_cocompact, Filter.hasBasis_cocompact, Filter.HasBasis.tendsto_left_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
obtain : ∀ (U : Set Y) (hU₁ : U ⊆ N) (hU₂ : IsOpen[inst_1] U) (hU₃ : y ∈ U), ∃ (i : Set X), IsCompact i ∧ MapsTo f iᶜ N
⊢ ∃ (i : Set X), IsCompact i ∧ MapsTo f iᶜ N

Tactic:
obtain ⟨U, hU₁, hU₂, hU₃⟩ := mem_nhds_iff.mp hN

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst_1] U
hU₃ : y ∈ U
⊢ MapsTo f (f ⁻¹' Uᶜ)ᶜ N

Tactic:
simpa using (mapsTo_preimage f U).mono_right hU₁

Premises used: Set.MapsTo.mono_right, Set.mapsTo_preimage
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst_1] U
hU₃ : y ∈ U
refine : IsCompact (f ⁻¹' Uᶜ)
⊢ ∃ (i : Set X), IsCompact i ∧ MapsTo f iᶜ N

Tactic:
refine ⟨f⁻¹' Uᶜ, ?_, by simpa using (mapsTo_preimage f U).mono_right hU₁⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst_1] U
hU₃ : y ∈ U
⊢ Uᶜ ⊆ range f

Tactic:
simpa [hy]
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst_1] U
hU₃ : y ∈ U
rw : IsCompact Uᶜ
⊢ IsCompact (f ⁻¹' Uᶜ)

Tactic:
rw [hf.isCompact_iff, image_preimage_eq_iff.mpr (by simpa [hy])]

Premises used: Iff.mpr, Topology.IsEmbedding.isCompact_iff, Set.image_preimage_eq_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst_1] U
hU₃ : y ∈ U
⊢ IsCompact Uᶜ

Tactic:
(isClosed_compl_iff.mpr hU₂).isCompact

Premises used: Iff.mpr, IsClosed.isCompact, isClosed_compl_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
N : Set Y
hN : N ∈ 𝓝 y
U : Set Y
hU₁ : U ⊆ N
hU₂ : IsOpen[inst_1] U
hU₃ : y ∈ U
⊢ IsCompact Uᶜ

Tactic:
exact (isClosed_compl_iff.mpr hU₂).isCompact

Premises used: Iff.mpr, IsClosed.isCompact, isClosed_compl_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
q : Y
hq : ¬q = y
⊢ q ∈ range f

Tactic:
simpa [hy]
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
⊢ Eq.{u_1 + 1} (α := OnePoint X)
    ((fun (q : Y) ↦
        (if hq : q = y then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q) ⋯) : OnePoint X) : OnePoint X))
      ((fun (p : OnePoint X) ↦ p.elim y f) ∞))
    ∞

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
p : X
⊢ f p ≠ y

Tactic:
simpa [hy] using mem_range_self (f := f) p

Premises used: Set.mem_range_self
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
p : X
⊢ f p ≠ y

Tactic:
have hp : f p ≠ y := by simpa [hy] using mem_range_self (f := f) p
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
inst_3 : CompactSpace Y
y : Y
f : X → Y
hf : IsEmbedding f
hy : range f = {y}ᶜ
_i : T2Space X
this : Tendsto f (coclosedCompact X) (𝓝 y)
p : X
hp : f p ≠ y
⊢ (fun (q : Y) ↦
        (if hq : q = y then ∞ else (↑(Exists.choose (p := fun (y : X) ↦ f y = q) ⋯) : OnePoint X) : OnePoint X))
      ((fun (p : OnePoint X) ↦ p.elim y f) (↑p : OnePoint X)) =
    (↑p : OnePoint X)

Tactic:
simpa [hp] using hf.injective (mem_range_self p).choose_spec

Premises used: Set.mem_range_self, Exists.choose_spec, Topology.IsEmbedding.injective