awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CompactOpen
Goal:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X₀
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Z
inst_4 : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous[instTopologicalSpaceProd, inst_3] fun (p : Y × X₀) ↦ g (p.1, f p.2)
this_1 : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ g (p.swap.1, f p.swap.2)
this : Continuous[instTopologicalSpaceProd, inst_3] fun (p : X₀ × Y) ↦ (g ∘ Prod.swap) (f p.1, p.2)
⊢ Continuous[instTopologicalSpaceProd, inst_3] g

Tactic:
exact (hf.continuous_lift_prod_left this).comp continuous_swap

Premises used: Continuous.comp, continuous_swap, Topology.IsQuotientMap.continuous_lift_prod_left
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
x₁ x₂ : X
rw : ((↑x₁ : OnePoint X) = (↑x₂ : OnePoint X)) = (x₁ = x₂)
⊢ (↑x₁ : OnePoint X) = (↑x₂ : OnePoint X) ↔ x₁ = x₂

Tactic:
rw [iff_eq_eq]

Premises used: iff_eq_eq
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
x₁ x₂ : X
⊢ ((↑x₁ : OnePoint X) = (↑x₂ : OnePoint X)) = (x₁ = x₂)

Tactic:
Option.some.injEq x₁ x₂

Premises used: OnePoint.some, Option.some.injEq, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
x₁ x₂ : X
⊢ ((↑x₁ : OnePoint X) = (↑x₂ : OnePoint X)) = (x₁ = x₂)

Tactic:
exact Option.some.injEq x₁ x₂

Premises used: Option.some.injEq
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
p : OnePoint X → Prop
⊢ (∀ (x : OnePoint X), p x) ↔ p ∞ ∧ ∀ (x : X), p (↑x : OnePoint X)

Tactic:
Option.forall

Premises used: OnePoint.infty, OnePoint.some, Option.forall, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
p : OnePoint X → Prop
⊢ (∃ (x : OnePoint X), p x) ↔ p ∞ ∨ ∃ (x : X), p (↑x : OnePoint X)

Tactic:
Option.exists

Premises used: OnePoint.infty, OnePoint.some, Option.exists, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : Infinite X
⊢ Infinite.{u_1 + 1} (OnePoint X)

Tactic:
inferInstanceAs (Infinite (Option X))

Premises used: _private.0.OnePoint.infinite._proof_1
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := X) some

Tactic:
Option.some_injective X

Premises used: OnePoint.some, Option.some_injective, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
x y : X
⊢ (↑x : OnePoint X) = (↑y : OnePoint X) ↔ x = y

Tactic:
coe_injective.eq_iff

Premises used: OnePoint.coe_injective, Function.Injective.eq_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
x : X
⊢ (↑x : OnePoint X) ≠ ∞

Tactic:
nofun

Premises used: False, _private.0.OnePoint.coe_ne_infty.match_1, Not
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
x : X
⊢ ∞ ≠ (↑x : OnePoint X)

Tactic:
nofun

Premises used: False, _private.0.OnePoint.infty_ne_coe.match_1, Not
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
y : Y
f : X → Y
⊢ OnePoint.elim ∞ y f = y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
y : Y
f : X → Y
x : X
⊢ (↑x : OnePoint X).elim y f = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
⊢ IsCompl (α := Set (OnePoint X)) (range some) {∞}

Tactic:
isCompl_range_some_none X

Premises used: OnePoint.infty, Set.isCompl_range_some_none, OnePoint.some, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
⊢ Eq (α := Set (OnePoint X)) (range some ∪ {∞}) univ

Tactic:
range_some_union_none X

Premises used: OnePoint.infty, OnePoint.some, Set.range_some_union_none, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
⊢ Eq (α := Set (OnePoint X)) (insert ∞ (range some)) univ

Tactic:
insert_none_range_some _

Premises used: Set.insert_none_range_some, OnePoint.infty, OnePoint.some, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
⊢ Eq (α := Set (OnePoint X)) (range some ∩ {∞}) ∅

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
⊢ Eq (α := Set (OnePoint X)) (range some)ᶜ {∞}

Tactic:
compl_range_some X

Premises used: OnePoint.infty, Set.Mem, setOf, OnePoint.some, Set.compl_range_some, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
⊢ Eq (α := Set (OnePoint X)) {∞}ᶜ (range some)

Tactic:
(@isCompl_range_coe_infty X).symm.compl_eq

Premises used: IsCompl.compl_eq, OnePoint.isCompl_range_coe_infty, IsCompl.symm
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
s : Set X
rw : some '' sᶜ ∪ (range some)ᶜ = some '' sᶜ ∪ {∞}
rw₁ rw₂ : some '' sᶜ ∪ {∞} = some '' sᶜ ∪ {∞}
⊢ (some '' s)ᶜ = some '' sᶜ ∪ {∞}

Tactic:
rw [coe_injective.compl_image_eq, compl_range_coe]

Premises used: OnePoint.coe_injective, OnePoint.compl_range_coe, Function.Injective.compl_image_eq
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
x : OnePoint X
infty : Ne.{u_1 + 1} (α := OnePoint X) ∞ ∞ ↔ ∃ (y : X), (↑y : OnePoint X) = ∞
coe : ∀ (x : X), (↑x : OnePoint X) ≠ ∞ ↔ ∃ (y : X), (↑y : OnePoint X) = (↑x : OnePoint X)
⊢ x ≠ ∞ ↔ ∃ (y : X), (↑y : OnePoint X) = x

Tactic:
induction x using OnePoint.rec
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
⊢ Ne.{u_1 + 1} (α := OnePoint X) ∞ ∞ ↔ ∃ (y : X), (↑y : OnePoint X) = ∞

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
x : X
⊢ (↑x : OnePoint X) ≠ ∞ ↔ ∃ (y : X), (↑y : OnePoint X) = (↑x : OnePoint X)

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
⊢ CanLift (OnePoint X) X some fun (x : OnePoint X) ↦ x ≠ ∞

Tactic:
WithTop.canLift

Premises used: OnePoint.infty, OnePoint.some, WithTop.canLift, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
x : OnePoint X
rw : Membership.mem (γ := Set (OnePoint X)) (range some)ᶜ x ↔ x = ∞
rw₁ : Membership.mem (γ := Set (OnePoint X)) {∞} x ↔ x = ∞
rw₂ rw₃ : x = ∞ ↔ x = ∞
⊢ x ∉ range some ↔ x = ∞

Tactic:
rw [← mem_compl_iff, compl_range_coe, mem_singleton_iff]

Premises used: OnePoint.compl_range_coe, Set.mem_singleton_iff, Set.mem_compl_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
⊢ ∞ ∉ range some

Tactic:
notMem_range_coe_iff.2 rfl

Premises used: Iff.mpr, OnePoint.notMem_range_coe_iff, rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
s : Set X
⊢ ∞ ∉ some '' s

Tactic:
notMem_subset (image_subset_range _ _) infty_notMem_range_coe

Premises used: Set.image_subset_range, OnePoint.infty_notMem_range_coe, Set.notMem_subset
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
h : ∀ (x : X), Membership.mem (γ := Set X) (some ⁻¹' {∞}) x ↔ Membership.mem (γ := Set X) ∅ x
⊢ Eq (α := Set X) (some ⁻¹' {∞}) ∅

Tactic:
ext
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
x : X
⊢ Membership.mem (γ := Set X) (some ⁻¹' {∞}) x ↔ Membership.mem (γ := Set X) ∅ x

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
⊢ OnePoint.map f ∞ = ∞

Tactic:
rfl

Premises used: OnePoint.infty, rfl, OnePoint.map
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
x : X
⊢ OnePoint.map f (↑x : OnePoint X) = (↑(f x) : OnePoint Y)

Tactic:
rfl

Premises used: OnePoint.some, rfl, OnePoint.map
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
⊢ Eq.{u_1 + 1} (α := OnePoint X → OnePoint X) (OnePoint.map id) id

Tactic:
Option.map_id

Premises used: Option.map_id, OnePoint.map, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : Y → Z
g : X → Y
⊢ OnePoint.map (f ∘ g) = OnePoint.map f ∘ OnePoint.map g

Tactic:
(Option.map_comp_map _ _).symm

Premises used: Option.map_comp_map, Eq.symm, OnePoint.map, OnePoint
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
⊢ (Membership.mem (γ := Set (OnePoint X)) univ ∞ → IsCompact.{u_1} (X := X) (some ⁻¹' univ)ᶜ) ∧
    IsOpen[inst] (some ⁻¹' univ)

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

Tactic:
⟨?_, hs.inter ht⟩

Premises used: And.intro, IsOpen.inter
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)
refine : ∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ
⊢ (∞ ∈ s ∩ t → IsCompact (some ⁻¹' (s ∩ t))ᶜ) ∧ IsOpen[inst] (some ⁻¹' (s ∩ t))

Tactic:
refine ⟨?_, hs.inter ht⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)
hms' : ∞ ∈ s
hmt' : ∞ ∈ t
⊢ IsCompact (some ⁻¹' (s ∩ t))ᶜ

Tactic:
simpa [compl_inter] using (hms hms').union (hmt hmt')

Premises used: Set.compl_inter, IsCompact.union
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)

Tactic:
⟨?_, this⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)
refine : ∞ ∈ ⋃₀ S → IsCompact (some ⁻¹' ⋃₀ S)ᶜ
⊢ (∞ ∈ ⋃₀ S → IsCompact (some ⁻¹' ⋃₀ S)ᶜ) ∧ IsOpen[inst] (some ⁻¹' ⋃₀ S)

Tactic:
refine ⟨?_, this⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)ᶜ

Tactic:
IsCompact.of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl ?_

Premises used: IsOpen.isClosed_compl, IsCompact.of_isClosed_subset, And.left
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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
refine : (some ⁻¹' ⋃₀ S)ᶜ ⊆ (some ⁻¹' s)ᶜ
⊢ IsCompact (some ⁻¹' ⋃₀ S)ᶜ

Tactic:
refine IsCompact.of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl ?_

Premises used: IsOpen.isClosed_compl, IsCompact.of_isClosed_subset, And.left
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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
⊢ (some ⁻¹' ⋃₀ S)ᶜ ⊆ (some ⁻¹' s)ᶜ

Tactic:
compl_subset_compl.mpr (preimage_mono <| subset_sUnion_of_mem hsS)

Premises used: Iff.mpr, Set.compl_subset_compl, Set.preimage_mono, Set.subset_sUnion_of_mem
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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
⊢ (some ⁻¹' ⋃₀ S)ᶜ ⊆ (some ⁻¹' s)ᶜ

Tactic:
exact compl_subset_compl.mpr (preimage_mono <| subset_sUnion_of_mem hsS)

Premises used: Iff.mpr, Set.compl_subset_compl, Set.preimage_mono, Set.subset_sUnion_of_mem
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)
suffices : IsOpen[inst] (some ⁻¹' ⋃₀ S)
⊢ (∞ ∈ ⋃₀ S → IsCompact (some ⁻¹' ⋃₀ S)ᶜ) ∧ 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)
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)
rw : IsOpen[inst] (⋃ t ∈ S, some ⁻¹' t)
⊢ IsOpen[inst] (some ⁻¹' ⋃₀ S)

Tactic:
rw [preimage_sUnion]

Premises used: Set.preimage_sUnion
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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] (⋃ t ∈ S, some ⁻¹' t)

Tactic:
isOpen_biUnion fun s hs => (ho s hs).2

Premises used: And.right, isOpen_biUnion
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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] (⋃ t ∈ S, some ⁻¹' t)

Tactic:
exact isOpen_biUnion fun s hs => (ho s hs).2

Premises used: And.right, isOpen_biUnion
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
⊢ IsOpen[instTopologicalSpace] s ↔ (∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ) ∧ IsOpen[inst] (some ⁻¹' s)

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsOpen
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
⊢ IsOpen[instTopologicalSpace] s ↔ IsCompact (some ⁻¹' s)ᶜ ∧ IsOpen[inst] (some ⁻¹' s)

Tactic:
simp [isOpen_def, h]

Premises used: OnePoint.isOpen_def
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
⊢ IsOpen[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s)ᶜ ∧ IsCompact (some ⁻¹' s)ᶜ

Tactic:
simp only [isOpen_iff_of_mem' h, isClosed_compl_iff, and_comm]

Premises used: OnePoint.isOpen_iff_of_mem', and_comm, isClosed_compl_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∉ s
⊢ IsOpen[instTopologicalSpace] s ↔ IsOpen[inst] (some ⁻¹' s)

Tactic:
simp [isOpen_def, h]

Premises used: OnePoint.isOpen_def
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
⊢ ∞ ∉ sᶜ

Tactic:
have : ∞ ∉ sᶜ := fun H => H h
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)ᶜ
rw₃ rw₄ : IsOpen[inst] (some ⁻¹' s)ᶜ ↔ IsOpen[inst] (some ⁻¹' s)ᶜ
⊢ IsClosed[instTopologicalSpace] s ↔ IsClosed[inst] (some ⁻¹' s)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_of_notMem this, ← isOpen_compl_iff, preimage_compl]

Premises used: OnePoint.isOpen_iff_of_notMem, Set.preimage_compl, isOpen_compl_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)
rw₃ 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)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_of_mem (mem_compl h), ← preimage_compl, compl_compl]

Premises used: OnePoint.isOpen_iff_of_mem, compl_compl, Set.preimage_compl, isOpen_compl_iff, Set.mem_compl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : IsOpen[inst] (some ⁻¹' some '' s) ↔ IsOpen[inst] s
rw₁ rw₂ : IsOpen[inst] s ↔ IsOpen[inst] s
⊢ IsOpen[instTopologicalSpace] (some '' s) ↔ IsOpen[inst] s

Tactic:
rw [isOpen_iff_of_notMem infty_notMem_image_coe, preimage_image_eq _ coe_injective]

Premises used: OnePoint.infty_notMem_image_coe, OnePoint.coe_injective, OnePoint.isOpen_iff_of_notMem, Set.preimage_image_eq
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : ∞ ∈ (some '' s)ᶜ
⊢ IsOpen[instTopologicalSpace] (some '' s)ᶜ ↔ IsClosed[inst] s ∧ IsCompact s

Tactic:
rw [isOpen_iff_of_mem, ← preimage_compl, compl_compl, preimage_image_eq _ coe_injective]

Premises used: OnePoint.isOpen_iff_of_mem, compl_compl, OnePoint.coe_injective, Set.preimage_image_eq, Set.preimage_compl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ ∞ ∈ (some '' s)ᶜ

Tactic:
infty_notMem_image_coe

Premises used: Set.Mem, OnePoint.infty_notMem_image_coe, setOf, Not
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ ∞ ∈ (some '' s)ᶜ

Tactic:
exact infty_notMem_image_coe

Premises used: OnePoint.infty_notMem_image_coe
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw : IsOpen[instTopologicalSpace] (some '' s)ᶜ ↔ IsClosed[inst] s ∧ IsCompact s
rw₁ rw₂ : IsClosed[inst] s ∧ IsCompact s ↔ IsClosed[inst] s ∧ IsCompact s
⊢ IsClosed[instTopologicalSpace] (some '' s) ↔ IsClosed[inst] s ∧ IsCompact s

Tactic:
rw [← isOpen_compl_iff, isOpen_compl_image_coe]

Premises used: OnePoint.isOpen_compl_image_coe, isOpen_compl_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h₁ : IsClosed[inst] s
h₂ : IsCompact s
⊢ ∞ ∈ opensOfCompl s h₁ h₂

Tactic:
mem_compl infty_notMem_image_coe

Premises used: Set.Mem, OnePoint.infty_notMem_image_coe, setOf, Not, Set.mem_compl
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Continuous[inst, instTopologicalSpace] some

Tactic:
continuous_def.mpr fun _s hs => hs.right

Premises used: Iff.mpr, And.right, continuous_def
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsOpenMap.{u_1, u_1} (X := X) some

Tactic:
fun _ => isOpen_image_coe.2

Premises used: Iff.mpr, IsOpenMap, OnePoint.isOpen_image_coe
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsOpenEmbedding.{u_1, u_1} (X := X) some

Tactic:
.of_continuous_injective_isOpenMap continuous_coe coe_injective isOpenMap_coe

Premises used: OnePoint.isOpenMap_coe, OnePoint.coe_injective, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, OnePoint.continuous_coe
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsOpen[instTopologicalSpace] (range some)

Tactic:
isOpenEmbedding_coe.isOpen_range

Premises used: OnePoint.isOpenEmbedding_coe, Topology.IsOpenEmbedding.isOpen_range
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
rw : IsOpen[instTopologicalSpace] (range some)
⊢ IsClosed[instTopologicalSpace] {∞}

Tactic:
rw [← compl_range_coe, isClosed_compl_iff]

Premises used: OnePoint.compl_range_coe, isClosed_compl_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsOpen[instTopologicalSpace] (range some)

Tactic:
isOpen_range_coe

Premises used: OnePoint.isOpen_range_coe
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsOpen[instTopologicalSpace] (range some)

Tactic:
exact isOpen_range_coe

Premises used: OnePoint.isOpen_range_coe
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ 𝓝 (↑x : OnePoint X) = map some (𝓝 x)

Tactic:
(isOpenEmbedding_coe.map_nhds_eq x).symm

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, OnePoint.isOpenEmbedding_coe, Eq.symm
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
x : X
⊢ 𝓝[some '' s] (↑x : OnePoint X) = map some (𝓝[s] x)

Tactic:
(isOpenEmbedding_coe.isEmbedding.map_nhdsWithin_eq _ _).symm

Premises used: Topology.IsOpenEmbedding.isEmbedding, OnePoint.isOpenEmbedding_coe, Topology.IsEmbedding.map_nhdsWithin_eq, Eq.symm
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (OnePoint X)
x : X
⊢ 𝓝[s] (↑x : OnePoint X) = map some (𝓝[some ⁻¹' s] x)

Tactic:
(isOpenEmbedding_coe.map_nhdsWithin_preimage_eq _ _).symm

Premises used: OnePoint.isOpenEmbedding_coe, Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq, Eq.symm
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ comap some (𝓝 (↑x : OnePoint X)) = 𝓝 x

Tactic:
(isOpenEmbedding_coe.isInducing.nhds_eq_comap x).symm

Premises used: Topology.IsInducing.nhds_eq_comap, OnePoint.isOpenEmbedding_coe, Topology.IsOpenEmbedding.isInducing, Eq.symm
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
x : X
h : (𝓝[≠] x).NeBot
⊢ (𝓝[≠] (↑x : OnePoint X)).NeBot

Tactic:
simpa [nhdsWithin_coe, preimage, coe_eq_coe] using h.map some

Premises used: OnePoint.nhdsWithin_coe, OnePoint.some, Filter.NeBot.map, Set.preimage, OnePoint.coe_eq_coe
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ 𝓝[≠] ∞ = map some (coclosedCompact X)

Tactic:
(nhdsWithin_basis_open ∞ _).ext (hasBasis_coclosedCompact.map _) ?_ ?_

Premises used: nhdsWithin_basis_open, OnePoint.infty, Filter.hasBasis_coclosedCompact, Filter.HasBasis.map, Filter.HasBasis.ext
-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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 ∩ {∞}ᶜ
refine_2 :
  ∀ (i' : Set X),
    IsClosed[inst] i' ∧ IsCompact i' →
      ∃ (i : Set (OnePoint X)), (∞ ∈ i ∧ IsOpen[instTopologicalSpace] i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ
⊢ 𝓝[≠] ∞ = map some (coclosedCompact X)

Tactic:
refine (nhdsWithin_basis_open ∞ _).ext (hasBasis_coclosedCompact.map _) ?_ ?_

Premises used: nhdsWithin_basis_open, OnePoint.infty, Filter.hasBasis_coclosedCompact, Filter.HasBasis.map, Filter.HasBasis.ext