awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∀ (x : 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 : OnePoint X) :
        Y)
      ((f : (a : OnePoint X) → Y) (↑x : OnePoint X) : Y)

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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 ∞))
rw₁ rw₂ :
  Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) atTop (𝓝 (f ∞)) ↔
    Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) atTop (𝓝 (f ∞))
⊢ Continuous[_, inst] f ↔ Tendsto (fun (x : ℕ) ↦ f (↑x : OnePoint ℕ)) atTop (𝓝 (f ∞))

Tactic:
rw [continuous_iff_from_discrete, Nat.cofinite_eq_atTop]

Premises used: OnePoint.continuous_iff_from_discrete, Nat.cofinite_eq_atTop
-- 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 : ℕ → Y
y : Y
h rwa rwa₁ rwa₂ rwa₃ : Tendsto f atTop (𝓝 y)
⊢ Tendsto f cofinite (𝓝 y)

Tactic:
rwa [Nat.cofinite_eq_atTop]

Premises used: Nat.cofinite_eq_atTop
-- 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 : T2Space Y
x : { f : ℕ → Y // ∃ (L : Y), Tendsto (fun (x : ℕ) ↦ f x) cofinite (𝓝 L) }
f : ℕ → Y
hf rwa rwa₁ rwa₂ rwa₃ : ∃ (L : Y), Tendsto (fun (x : ℕ) ↦ f x) cofinite (𝓝 L)
⊢ ∃ (L : Y), Tendsto (fun (x : ℕ) ↦ f x) atTop (𝓝 L)

Tactic:
rwa [← Nat.cofinite_eq_atTop]

Premises used: Nat.cofinite_eq_atTop
-- 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 : T2Space Y
x : { f : ℕ → Y // ∃ (L : Y), Tendsto (fun (x : ℕ) ↦ f x) atTop (𝓝 L) }
f : ℕ → Y
hf rwa rwa₁ rwa₂ rwa₃ : ∃ (L : Y), Tendsto (fun (x : ℕ) ↦ f x) atTop (𝓝 L)
⊢ ∃ (L : Y), Tendsto (fun (x : ℕ) ↦ f x) cofinite (𝓝 L)

Tactic:
rwa [Nat.cofinite_eq_atTop]

Premises used: Nat.cofinite_eq_atTop
-- 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 : T2Space Y
⊢ C(OnePoint ℕ, Y) ≃ { f : ℕ → Y // ∃ (L : Y), Tendsto (fun (x : ℕ) ↦ f x) atTop (𝓝 L) }

Tactic:
refine (continuousMapDiscreteEquiv ℕ Y).trans {
    toFun := fun ⟨f, hf⟩ ↦ ⟨f, by rwa [← Nat.cofinite_eq_atTop]⟩
    invFun := fun ⟨f, hf⟩ ↦ ⟨f, by rwa [Nat.cofinite_eq_atTop]⟩ }

Premises used: Equiv.trans, Equiv.mk, OnePoint.continuousMapDiscreteEquiv, Nat
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NoncompactSpace X
rw : Dense (X := OnePoint X) {∞}ᶜ
⊢ DenseRange.{u_1, u_1} (X := OnePoint X) some

Tactic:
rw [DenseRange, ← compl_infty]

Premises used: OnePoint.compl_infty, DenseRange
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NoncompactSpace X
⊢ Dense (X := OnePoint X) {∞}ᶜ

Tactic:
dense_compl_singleton _

Premises used: dense_compl_singleton
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NoncompactSpace X
⊢ Dense (X := OnePoint X) {∞}ᶜ

Tactic:
exact dense_compl_singleton _

Premises used: dense_compl_singleton
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NoncompactSpace X
⊢ IsDenseEmbedding.{u_1, u_1} (α := X) some

Tactic:
{ isOpenEmbedding_coe with dense := denseRange_coe }

Premises used: OnePoint.denseRange_coe, Topology.IsOpenEmbedding.toIsEmbedding, IsDenseEmbedding.mk, IsDenseInducing.mk, OnePoint.isOpenEmbedding_coe, Topology.IsEmbedding.injective, Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ (↑x : OnePoint X) ⤳ (↑y : OnePoint X) ↔ x ⤳ y

Tactic:
isOpenEmbedding_coe.isInducing.specializes_iff

Premises used: Topology.IsInducing.specializes_iff, OnePoint.isOpenEmbedding_coe, Topology.IsOpenEmbedding.isInducing
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ Inseparable (↑x : OnePoint X) (↑y : OnePoint X) ↔ Inseparable x y

Tactic:
isOpenEmbedding_coe.isInducing.inseparable_iff

Premises used: OnePoint.isOpenEmbedding_coe, Topology.IsOpenEmbedding.isInducing, Topology.IsInducing.inseparable_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ ¬∞ ⤳ (↑x : OnePoint X)

Tactic:
isClosed_infty.not_specializes rfl (coe_ne_infty x)

Premises used: OnePoint.isClosed_infty, IsClosed.not_specializes, rfl, OnePoint.coe_ne_infty
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ ¬Inseparable ∞ (↑x : OnePoint X)

Tactic:
fun h =>
  not_specializes_infty_coe h.specializes

Premises used: OnePoint.not_specializes_infty_coe, Inseparable.specializes, Not
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ ¬Inseparable (↑x : OnePoint X) ∞

Tactic:
fun h =>
  not_specializes_infty_coe h.specializes'

Premises used: Inseparable.specializes', OnePoint.not_specializes_infty_coe, Not
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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'
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'
⊢ Inseparable x y ↔
    x = ∞ ∧ y = ∞ ∨ ∃ (x' : X), x = (↑x' : OnePoint X) ∧ ∃ (y' : X), y = (↑y' : OnePoint X) ∧ Inseparable x' y'

Tactic:
induction x using OnePoint.rec
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
y : OnePoint X
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'
infty₁ :
  ∀ (x : X),
    Inseparable ∞ (↑x : OnePoint X) ↔
      Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∧ (↑x : OnePoint X) = ∞ ∨
        ∃ (x' : X), ∞ = (↑x' : OnePoint X) ∧ ∃ (y' : X), (↑x : OnePoint X) = (↑y' : OnePoint X) ∧ Inseparable x' y'
⊢ 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 y using OnePoint.rec
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
y : OnePoint X
x : X
coe :
  Inseparable (↑x : OnePoint X) ∞ ↔
    (↑x : OnePoint X) = ∞ ∧ Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∨
      ∃ (x' : X), (↑x : OnePoint X) = (↑x' : OnePoint X) ∧ ∃ (y' : X), ∞ = (↑y' : OnePoint X) ∧ Inseparable x' y'
coe₁ :
  ∀ (x_1 : X),
    Inseparable (↑x : OnePoint X) (↑x_1 : OnePoint X) ↔
      (↑x : OnePoint X) = ∞ ∧ (↑x_1 : OnePoint X) = ∞ ∨
        ∃ (x' : X),
          (↑x : OnePoint X) = (↑x' : OnePoint X) ∧
            ∃ (y' : X), (↑x_1 : OnePoint X) = (↑y' : OnePoint X) ∧ Inseparable x' y'
⊢ 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 y using OnePoint.rec
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ 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:
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]

Premises used: OnePoint.not_inseparable_infty_coe, Inseparable.refl, OnePoint.coe_eq_coe, OnePoint.not_inseparable_coe_infty
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ Inseparable ∞ (↑x : OnePoint X) ↔
    Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∧ (↑x : OnePoint X) = ∞ ∨
      ∃ (x' : X), ∞ = (↑x' : OnePoint X) ∧ ∃ (y' : X), (↑x : OnePoint X) = (↑y' : OnePoint X) ∧ Inseparable x' y'

Tactic:
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]

Premises used: OnePoint.not_inseparable_infty_coe, Inseparable.refl, OnePoint.coe_eq_coe, OnePoint.not_inseparable_coe_infty
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ Inseparable (↑x : OnePoint X) ∞ ↔
    (↑x : OnePoint X) = ∞ ∧ Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞ ∨
      ∃ (x' : X), (↑x : OnePoint X) = (↑x' : OnePoint X) ∧ ∃ (y' : X), ∞ = (↑y' : OnePoint X) ∧ Inseparable x' y'

Tactic:
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]

Premises used: OnePoint.not_inseparable_infty_coe, Inseparable.refl, OnePoint.coe_eq_coe, OnePoint.not_inseparable_coe_infty
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x x_1 : X
⊢ Inseparable (↑x : OnePoint X) (↑x_1 : OnePoint X) ↔
    (↑x : OnePoint X) = ∞ ∧ (↑x_1 : OnePoint X) = ∞ ∨
      ∃ (x' : X),
        (↑x : OnePoint X) = (↑x' : OnePoint X) ∧
          ∃ (y' : X), (↑x_1 : OnePoint X) = (↑y' : OnePoint X) ∧ Inseparable x' y'

Tactic:
simp [not_inseparable_infty_coe, not_inseparable_coe_infty, coe_eq_coe, Inseparable.refl]

Premises used: OnePoint.not_inseparable_infty_coe, Inseparable.refl, OnePoint.coe_eq_coe, OnePoint.not_inseparable_coe_infty
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
simp_rw :
  (Tendsto.{u_1, u_2} (β := OnePoint Y) (fun (x : X) ↦ (↑(f x) : OnePoint Y)) (comap some (𝓝 ∞)) (𝓝 ∞) ∧
      Continuous[inst, instTopologicalSpace] fun (x : X) ↦ (↑(f x) : OnePoint Y)) ↔
    Continuous[inst, instTopologicalSpace] (some ∘ f) ∧ Tendsto (some ∘ f) (comap some (𝓝 ∞)) (𝓝 ∞)
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (OnePoint.map f) ↔
    Continuous[inst, inst_1] f ∧ Tendsto f (coclosedCompact X) (coclosedCompact Y)

Tactic:
simp_rw [continuous_iff, map_some, ← comap_coe_nhds_infty, tendsto_comap_iff, map_infty,
    isOpenEmbedding_coe.isInducing.continuous_iff (Y := Y)]

Premises used: OnePoint.continuous_iff, Topology.IsInducing.continuous_iff, Filter.tendsto_comap_iff, OnePoint.isOpenEmbedding_coe, OnePoint.comap_coe_nhds_infty, OnePoint.map_some, Topology.IsOpenEmbedding.isInducing, OnePoint.map_infty
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ (Tendsto.{u_1, u_2} (β := OnePoint Y) (fun (x : X) ↦ (↑(f x) : OnePoint Y)) (comap some (𝓝 ∞)) (𝓝 ∞) ∧
      Continuous[inst, instTopologicalSpace] fun (x : X) ↦ (↑(f x) : OnePoint Y)) ↔
    Continuous[inst, instTopologicalSpace] (some ∘ f) ∧ Tendsto (some ∘ f) (comap some (𝓝 ∞)) (𝓝 ∞)

Tactic:
and_comm

Premises used: and_comm
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ (Tendsto.{u_1, u_2} (β := OnePoint Y) (fun (x : X) ↦ (↑(f x) : OnePoint Y)) (comap some (𝓝 ∞)) (𝓝 ∞) ∧
      Continuous[inst, instTopologicalSpace] fun (x : X) ↦ (↑(f x) : OnePoint Y)) ↔
    Continuous[inst, instTopologicalSpace] (some ∘ f) ∧ Tendsto (some ∘ f) (comap some (𝓝 ∞)) (𝓝 ∞)

Tactic:
exact and_comm

Premises used: and_comm
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hc : Continuous[inst, inst_1] f
h : Tendsto f (coclosedCompact X) (coclosedCompact Y)
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (OnePoint.map f)

Tactic:
continuous_map_iff.mpr ⟨hc, h⟩

Premises used: Iff.mpr, And.intro, OnePoint.continuous_map_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
rw : Tendsto some (cocompact X) (map some (coclosedCompact X) ⊔ pure ∞)
⊢ Tendsto some (cocompact X) (𝓝 ∞)

Tactic:
rw [nhds_infty_eq]

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

Tactic:
(tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left

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

Tactic:
exact (tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left

Premises used: le_sup_left, Filter.tendsto_map, Filter.Tendsto.mono_left, Filter.cocompact_le_coclosedCompact, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
⊢ Tendsto some (cocompact X) (𝓝 ∞)

Tactic:
have : Tendsto ((↑) : X → OnePoint X) (cocompact X) (𝓝 ∞) := by
      rw [nhds_infty_eq]
      exact (tendsto_map.mono_left cocompact_le_coclosedCompact).mono_right le_sup_left
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
this : Tendsto some (cocompact X) (𝓝 ∞)
rw : IsCompact (X := OnePoint X) (insert none (range Option.some))
⊢ IsCompact.{u_1} (X := OnePoint X) univ

Tactic:
rw [← insert_none_range_some X]

Premises used: Set.insert_none_range_some
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact (X := OnePoint X) (insert none (range Option.some))

Tactic:
this.isCompact_insert_range_of_cocompact continuous_coe

Premises used: OnePoint.infty, OnePoint.some, OnePoint.continuous_coe, Filter.Tendsto.isCompact_insert_range_of_cocompact, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
this : Tendsto some (cocompact X) (𝓝 ∞)
⊢ IsCompact (X := OnePoint X) (insert none (range Option.some))

Tactic:
exact this.isCompact_insert_range_of_cocompact continuous_coe

Premises used: OnePoint.continuous_coe, Filter.Tendsto.isCompact_insert_range_of_cocompact
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T0Space X
⊢ T0Space.{u_1} (OnePoint X)

Tactic:
⟨fun x y hxy => ?_⟩

Premises used: T0Space.mk
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T0Space X
refine : ∀ (x y : OnePoint X) (hxy : Inseparable x y), x = y
⊢ T0Space.{u_1} (OnePoint X)

Tactic:
refine ⟨fun x y hxy => ?_⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T0Space X
x y : OnePoint X
hxy : Inseparable x y
inl : ∀ (hxy : Inseparable.{u_1} (X := OnePoint X) ∞ ∞), Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞
inr :
  ∀ (x y : X) (h : Inseparable x y) (hxy : Inseparable (↑x : OnePoint X) (↑y : OnePoint X)),
    (↑x : OnePoint X) = (↑y : OnePoint X)
⊢ x = y

Tactic:
rcases inseparable_iff.1 hxy with (⟨rfl, rfl⟩ | ⟨x, rfl, y, rfl, h⟩)

Premises used: OnePoint.inseparable_iff, Iff.mp, 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 : T0Space X
hxy : Inseparable.{u_1} (X := OnePoint X) ∞ ∞
⊢ Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞

Tactic:
rfl

Premises used: 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 : T0Space X
x y : X
h : Inseparable x y
hxy : Inseparable (↑x : OnePoint X) (↑y : OnePoint X)
⊢ (↑x : OnePoint X) = (↑y : OnePoint X)

Tactic:
congr_arg some h.eq

Premises used: OnePoint.some, Inseparable.eq, congr_arg
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T0Space X
hxy : Inseparable.{u_1} (X := OnePoint X) ∞ ∞
⊢ Eq.{u_1 + 1} (α := OnePoint X) ∞ ∞

Tactic:
exacts [rfl, congr_arg some h.eq]

Premises used: 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 : T1Space X
z : OnePoint X
infty : IsClosed[instTopologicalSpace] {∞}
coe : ∀ (x : X), IsClosed[instTopologicalSpace] {(↑x : OnePoint X)}
⊢ IsClosed[instTopologicalSpace] {z}

Tactic:
induction z 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 : T1Space X
⊢ IsClosed[instTopologicalSpace] {∞}

Tactic:
isClosed_infty

Premises used: OnePoint.isClosed_infty
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T1Space X
⊢ IsClosed[instTopologicalSpace] {∞}

Tactic:
exact isClosed_infty

Premises used: OnePoint.isClosed_infty
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T1Space X
x : X
coe : IsClosed[inst] {x} ∧ IsCompact (X := X) {x}
⊢ IsClosed[instTopologicalSpace] {(↑x : OnePoint X)}

Tactic:
rw [← image_singleton, isClosed_image_coe]

Premises used: Set.image_singleton, OnePoint.isClosed_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 : T1Space X
x : X
⊢ IsClosed[inst] {x} ∧ IsCompact (X := X) {x}

Tactic:
⟨isClosed_singleton, isCompact_singleton⟩

Premises used: isCompact_singleton, And.intro, isClosed_singleton
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
inst_1 : T1Space X
x : X
⊢ IsClosed[inst] {x} ∧ IsCompact (X := X) {x}

Tactic:
exact ⟨isClosed_singleton, isCompact_singleton⟩
-- 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
this : R1Space.{u_1} (OnePoint X)
⊢ NormalSpace.{u_1} (OnePoint X)

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 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
suffices : R1Space.{u_1} (OnePoint X)
⊢ NormalSpace.{u_1} (OnePoint X)

Tactic:
suffices R1Space (OnePoint X) by 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 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
z : X
rw : Disjoint (𝓝 z) (cocompact X) ∧ range some ∈ map some (𝓝 z)
⊢ Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)

Tactic:
rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact,
      disjoint_map coe_injective, ← principal_singleton, disjoint_principal_right, compl_infty]

Premises used: OnePoint.compl_infty, disjoint_sup_right, OnePoint.coe_injective, Filter.disjoint_map, OnePoint.nhds_coe_eq, Filter.principal_singleton, Filter.coclosedCompact_eq_cocompact, OnePoint.nhds_infty_eq, Filter.disjoint_principal_right
-- 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
z : X
⊢ Disjoint (𝓝 z) (cocompact X) ∧ range some ∈ map some (𝓝 z)

Tactic:
⟨disjoint_nhds_cocompact z, range_mem_map⟩

Premises used: disjoint_nhds_cocompact, And.intro, Filter.range_mem_map
-- 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
z : X
⊢ Disjoint (𝓝 z) (cocompact X) ∧ range some ∈ map some (𝓝 z)

Tactic:
exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
-- 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
⊢ ∀ (z : X), Disjoint (𝓝 (↑z : OnePoint X)) (𝓝 ∞)

Tactic:
have key : ∀ z : X, Disjoint (𝓝 (some z)) (𝓝 ∞) := fun z ↦ by
    rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact,
      disjoint_map coe_injective, ← principal_singleton, disjoint_principal_right, compl_infty]
    exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
-- 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)) (𝓝 ∞)
⊢ R1Space.{u_1} (OnePoint X)

Tactic:
⟨fun x y ↦ ?_⟩

Premises used: R1Space.mk
-- 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)) (𝓝 ∞)
refine : ∀ (x y : OnePoint X), x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)
⊢ R1Space.{u_1} (OnePoint X)

Tactic:
refine ⟨fun x y ↦ ?_⟩
-- 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 y : OnePoint X
infty : ∞ ⤳ y ∨ Disjoint (𝓝 ∞) (𝓝 y)
coe : ∀ (x : X), (↑x : OnePoint X) ⤳ y ∨ Disjoint (𝓝 (↑x : OnePoint X)) (𝓝 y)
⊢ x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)

Tactic:
induction x using OnePoint.rec