awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : T0Space X
s : Set X
hs : IsOpen[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst_1] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst_1] U
hU : Xor (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
⊢ s ∩ U = s

Tactic:
have : s ∩ U = s := hmin (s ∩ U) inter_subset_left ⟨x, hx, hxU⟩ (hs.inter hUo)
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : T0Space X
s : Set X
hs : IsOpen[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst_1] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst_1] U
hU : Xor (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
this : s ∩ U = s
⊢ False

Tactic:
hyU (this.symm.subset hy).2

Premises used: Eq.subset, And.right, Eq.symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : T0Space X
s : Set X
hs : IsOpen[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst_1] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst_1] U
hU : Xor (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
this : s ∩ U = s
⊢ False

Tactic:
exact hyU (this.symm.subset hy).2

Premises used: Eq.subset, And.right, Eq.symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsOpen[inst] s
hne : s.Nonempty
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
⊢ ∃ (x : X), s = {x}

Tactic:
exists_eq_singleton_iff_nonempty_subsingleton.2 ⟨hne, minimal_nonempty_open_subsingleton hs hmin⟩

Premises used: Iff.mpr, minimal_nonempty_open_subsingleton, Set.exists_eq_singleton_iff_nonempty_subsingleton, And.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hfin : s.Finite
hne : s.Nonempty
ho : IsOpen[inst] s
⊢ s.Finite

Tactic:
hfin
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hfin : s.Finite
hne : s.Nonempty
ho : IsOpen[inst] s
lift :
  ∀ (s : Finset X) (hne : (↑s : Set X).Nonempty) (ho : IsOpen[inst] (↑s : Set X)), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
⊢ ∃ x ∈ s, IsOpen[inst] {x}

Tactic:
lift s to Finset X using hfin

Premises used: Finset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
a :
  ∀ (s : Finset X),
    (∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}) →
      ∀ (hne : (↑s : Set X).Nonempty) (ho : IsOpen[inst] (↑s : Set X)), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}

Tactic:
induction s using Finset.strongInductionOn
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
a :
  ∀ (t : Finset X) (hts : t ⊂ s) (htne : t.Nonempty) (hto : IsOpen[inst] (↑t : Set X)),
    ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
a₁ : ∀ (ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}

Tactic:
rcases em (∃ t, t ⊂ s ∧ t.Nonempty ∧ IsOpen (t : Set X)) with (⟨t, hts, htne, hto⟩ | ht)

Premises used: HasSSubset.SSubset, Exists, em, And, SetLike.coe, Finset.Nonempty, IsOpen
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen[inst] (↑t : Set X)
a : ∀ (x : X) (hxt : x ∈ (↑t : Set X)) (hxo : IsOpen[inst] {x}), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}

Tactic:
rcases ihs t hts htne hto with ⟨x, hxt, hxo⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen[inst] (↑t : Set X)
x : X
hxt : x ∈ (↑t : Set X)
hxo : IsOpen[inst] {x}
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}

Tactic:
⟨x, hts.1 hxt, hxo⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen[inst] (↑t : Set X)
x : X
hxt : x ∈ (↑t : Set X)
hxo : IsOpen[inst] {x}
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}

Tactic:
exact ⟨x, hts.1 hxt, hxo⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
a : ∀ (x : X) (hx : (↑s : Set X) = {x}), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
rsuffices : ∃ (x : X), (↑s : Set X) = {x}
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}

Tactic:
rsuffices ⟨x, hx⟩ : ∃ x, (s : Set X) = {x}

Premises used: SetLike.coe
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
x : X
hx : (↑s : Set X) = {x}
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}

Tactic:
⟨x, hx.symm ▸ rfl, hx ▸ ho⟩

Premises used: Eq.rec, And.intro, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
x : X
hx : (↑s : Set X) = {x}
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}

Tactic:
exact ⟨x, hx.symm ▸ rfl, hx ▸ ho⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
⊢ ∃ (x : X), (↑s : Set X) = {x}

Tactic:
minimal_nonempty_open_eq_singleton ho hne ?_

Premises used: minimal_nonempty_open_eq_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
refine : ∀ t ⊆ (↑s : Set X), t.Nonempty → IsOpen[inst] t → t = (↑s : Set X)
⊢ ∃ (x : X), (↑s : Set X) = {x}

Tactic:
refine minimal_nonempty_open_eq_singleton ho hne ?_

Premises used: minimal_nonempty_open_eq_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
⊢ ∀ t ⊆ (↑s : Set X), t.Nonempty → IsOpen[inst] t → t = (↑s : Set X)

Tactic:
fun t hts htne hto => of_not_not fun hts' => ht ?_

Premises used: of_not_not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
refine :
  ∀ (t : Set X) (hts : t ⊆ (↑s : Set X)) (htne : t.Nonempty) (hto : IsOpen[inst] t) (hts' : ¬t = (↑s : Set X)),
    ∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
⊢ ∀ t ⊆ (↑s : Set X), t.Nonempty → IsOpen[inst] t → t = (↑s : Set X)

Tactic:
refine fun t hts htne hto => of_not_not fun hts' => ht ?_

Premises used: of_not_not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
t : Set X
hts : t ⊆ (↑s : Set X)
htne : t.Nonempty
hto : IsOpen[inst] t
hts' : ¬t = (↑s : Set X)
⊢ t.Finite

Tactic:
s.finite_toSet.subset hts

Premises used: Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
t : Set X
hts : t ⊆ (↑s : Set X)
htne : t.Nonempty
hto : IsOpen[inst] t
hts' : ¬t = (↑s : Set X)
lift :
  ∀ (t : Finset X) (hts : (↑t : Set X) ⊆ (↑s : Set X)) (htne : (↑t : Set X).Nonempty) (hto : IsOpen[inst] (↑t : Set X))
    (hts' : ¬(↑t : Set X) = (↑s : Set X)), ∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
⊢ ∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)

Tactic:
lift t to Finset X using s.finite_toSet.subset hts

Premises used: Finset, Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
t : Finset X
hts : (↑t : Set X) ⊆ (↑s : Set X)
htne : (↑t : Set X).Nonempty
hto : IsOpen[inst] (↑t : Set X)
hts' : ¬(↑t : Set X) = (↑s : Set X)
⊢ ∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)

Tactic:
⟨t, ssubset_iff_subset_ne.2 ⟨hts, mt Finset.coe_inj.2 hts'⟩, htne, hto⟩

Premises used: Iff.mpr, mt, Finset.coe_inj, And.intro, Exists.intro, ssubset_iff_subset_ne
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
t : Finset X
hts : (↑t : Set X) ⊆ (↑s : Set X)
htne : (↑t : Set X).Nonempty
hto : IsOpen[inst] (↑t : Set X)
hts' : ¬(↑t : Set X) = (↑s : Set X)
⊢ ∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)

Tactic:
exact ⟨t, ssubset_iff_subset_ne.2 ⟨hts, mt Finset.coe_inj.2 hts'⟩, htne, hto⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
inst_2 : Finite X
inst_3 : Nonempty X
⊢ ∃ (x : X), IsOpen[inst] {x}

Tactic:
let ⟨x, _, h⟩ := exists_isOpen_singleton_of_isOpen_finite (Set.toFinite _)
    univ_nonempty isOpen_univ
  ⟨x, h⟩

Premises used: Set.univ, Set.univ_nonempty, Exists, isOpen_univ, Set.toFinite, _private.0.exists_open_singleton_of_finite.match_1, Exists.intro, IsOpen, Singleton.singleton, exists_isOpen_singleton_of_isOpen_finite
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Injective f
hf' : Continuous[inst, inst_1] f
inst_2 : T0Space Y
⊢ T0Space X

Tactic:
⟨fun _ _ h => hf <| (h.map hf').eq⟩

Premises used: Inseparable.eq, T0Space.mk, Inseparable.map
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T0Space Y
f : X → Y
hf : IsEmbedding f
⊢ T0Space X

Tactic:
t0Space_of_injective_of_continuous hf.injective hf.continuous

Premises used: t0Space_of_injective_of_continuous, Topology.IsEmbedding.injective, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T0Space X
h : X ≃ₜ Y
⊢ T0Space Y

Tactic:
h.symm.isEmbedding.t0Space

Premises used: Topology.IsEmbedding.t0Space, Homeomorph.isEmbedding, Homeomorph.symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T0Space X
p : X → Prop
⊢ T0Space.{u_1} (Subtype p)

Tactic:
IsEmbedding.subtypeVal.t0Space

Premises used: Topology.IsEmbedding.t0Space, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun (a b : X) ↦ a ∉ closure[inst] {b} ∨ b ∉ closure[inst] {a}

Tactic:
simp only [t0Space_iff_not_inseparable, inseparable_iff_mem_closure, not_and_or]

Premises used: inseparable_iff_mem_closure, not_and_or, t0Space_iff_not_inseparable
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T0Space X
inst_3 : T0Space Y
⊢ T0Space (X × Y)

Tactic:
⟨fun _ _ h => Prod.ext (h.map continuous_fst).eq (h.map continuous_snd).eq⟩

Premises used: continuous_snd, continuous_fst, Inseparable.eq, T0Space.mk, Prod.ext, Inseparable.map
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_3
X : ι → Type u_4
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), T0Space.{u_4} (X i)
⊢ T0Space ((i : ι) → X i)

Tactic:
⟨fun _ _ h => funext fun i => (h.map (continuous_apply i)).eq⟩

Premises used: Inseparable.eq, T0Space.mk, funext, continuous_apply, Inseparable.map
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T0Space X
⊢ T0Space (ULift.{u_3, u_1} X)

Tactic:
IsEmbedding.uliftDown.t0Space

Premises used: Topology.IsEmbedding.t0Space, Topology.IsEmbedding.uliftDown
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
⊢ T0Space X

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

Premises used: T0Space.mk
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
refine : ∀ (x y : X) (hxy : Inseparable x y), x = y
⊢ T0Space X

Tactic:
refine ⟨fun x y hxy => ?_⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
x y : X
hxy : Inseparable x y
rcases : ∀ (s : Set X) (hxs : x ∈ s) (hys : y ∈ s) (hs : T0Space.{u_1} (↑s : Type u_1)), x = y
⊢ x = y

Tactic:
rcases h x y hxy with ⟨s, hxs, hys, hs⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
x y : X
hxy : Inseparable x y
s : Set X
hxs : x ∈ s
hys : y ∈ s
hs : T0Space.{u_1} (↑s : Type u_1)
⊢ x ∈ s

Tactic:
hxs
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
x y : X
hxy : Inseparable x y
s : Set X
hxs : x ∈ s
hys : y ∈ s
hs : T0Space.{u_1} (↑s : Type u_1)
lift : ∀ (x : { x : X // x ∈ s }) (hxy : Inseparable (↑x : X) y), (↑x : X) = y
⊢ x = y

Tactic:
lift x to s using hxs
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
y : X
s : Set X
hys : y ∈ s
hs : T0Space.{u_1} (↑s : Type u_1)
x : { x : X // x ∈ s }
hxy : Inseparable (↑x : X) y
⊢ y ∈ s

Tactic:
hys
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
y : X
s : Set X
hys : y ∈ s
hs : T0Space.{u_1} (↑s : Type u_1)
x : { x : X // x ∈ s }
hxy : Inseparable (↑x : X) y
lift : ∀ (y : { x : X // x ∈ s }) (hxy : Inseparable (↑x : X) (↑y : X)), (↑x : X) = (↑y : X)
⊢ (↑x : X) = y

Tactic:
lift y to s using hys
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
s : Set X
hs : T0Space.{u_1} (↑s : Type u_1)
x y : { x : X // x ∈ s }
hxy : Inseparable (↑x : X) (↑y : X)
⊢ Inseparable x y

Tactic:
rw [← subtype_inseparable_iff] at hxy

Premises used: subtype_inseparable_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
s : Set X
hs : T0Space.{u_1} (↑s : Type u_1)
x y : { x : X // x ∈ s }
hxy : Inseparable x y
⊢ (↑x : X) = (↑y : X)

Tactic:
congr_arg Subtype.val hxy.eq

Premises used: Inseparable.eq, congr_arg, Subtype.val
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
s : Set X
hs : T0Space.{u_1} (↑s : Type u_1)
x y : { x : X // x ∈ s }
hxy : Inseparable x y
⊢ (↑x : X) = (↑y : X)

Tactic:
exact congr_arg Subtype.val hxy.eq

Premises used: Inseparable.eq, congr_arg, Subtype.val
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x : X), ∃ (s : Set X), x ∈ s ∧ IsOpen[inst] s ∧ T0Space.{u_1} (↑s : Type u_1)
⊢ T0Space X

Tactic:
T0Space.of_cover fun x _ hxy =>
    let ⟨s, hxs, hso, hs⟩ := h x
    ⟨s, hxs, (hxy.mem_open_iff hso).1 hxs, hs⟩

Premises used: Membership.mem, Exists, Set.Elem, And, And.intro, Exists.intro, Iff.mp, T0Space.of_cover, T0Space, _private.0.T0Space.of_open_cover.match_1, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x y : X
h : x ⤳ y
⊢ y ⤳ x

Tactic:
specializes_symmetric h

Premises used: R0Space.specializes_symmetric
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x y : X
⊢ x ⤳ y ↔ y ⤳ x

Tactic:
⟨Specializes.symm, Specializes.symm⟩

Premises used: Specializes.symm, Iff.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x y : X
⊢ x ⤳ y ↔ Inseparable x y

Tactic:
⟨fun h ↦ h.antisymm h.symm, Inseparable.specializes⟩

Premises used: Specializes.symm, Specializes.antisymm, Inseparable.specializes, Iff.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : R0Space X
inst_2 : TopologicalSpace Y
f : Y → X
hf : IsInducing f
a b : Y
⊢ a ⤳ b → b ⤳ a

Tactic:
simpa only [← hf.specializes_iff] using Specializes.symm

Premises used: Specializes.symm, Topology.IsInducing.specializes_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : R0Space X
x y : X
p : X → Prop
⊢ R0Space.{u_1} { x : X // p x }

Tactic:
IsInducing.subtypeVal.r0Space

Premises used: Set.Mem, Topology.IsInducing.r0Space, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
h : ∀ (x_1 : X), Membership.mem (γ := Set X) (closure[inst] {x}) x_1 ↔ x_1 ∈ (𝓝 x).ker
⊢ closure[inst] {x} = (𝓝 x).ker

Tactic:
ext
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x x_1 : X
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) x_1 ↔ x_1 ∈ (𝓝 x).ker

Tactic:
simp [ker_nhds_eq_specializes, ← specializes_iff_mem_closure, specializes_comm]

Premises used: specializes_iff_mem_closure, ker_nhds_eq_specializes, specializes_comm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
⊢ IsCompact (X := X) (closure[inst] {x})

Tactic:
isCompact_of_finite_subcover fun U hUo hxU ↦ ?_

Premises used: isCompact_of_finite_subcover
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
refine :
  ∀ {ι : Type u_1} (U : ι → Set X) (hUo : ∀ (i : ι), IsOpen[inst] (U i))
    (hxU : Subset (α := Set X) (closure[inst] {x}) (⋃ (i : ι), U i)),
    ∃ (t : Finset ι), Subset (α := Set X) (closure[inst] {x}) (⋃ i ∈ t, U i)
⊢ IsCompact (X := X) (closure[inst] {x})

Tactic:
refine isCompact_of_finite_subcover fun U hUo hxU ↦ ?_

Premises used: isCompact_of_finite_subcover
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hxU : Subset (α := Set X) (closure[inst] {x}) (⋃ (i : ι), U i)
⊢ ∃ (i : ι), x ∈ U i

Tactic:
mem_iUnion.1 <| hxU <| subset_closure rfl

Premises used: subset_closure, Set.mem_iUnion, Iff.mp, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hxU : Subset (α := Set X) (closure[inst] {x}) (⋃ (i : ι), U i)
obtain : ∀ (i : ι) (hi : x ∈ U i), ∃ (t : Finset ι), Subset (α := Set X) (closure[inst] {x}) (⋃ i ∈ t, U i)
⊢ ∃ (t : Finset ι), Subset (α := Set X) (closure[inst] {x}) (⋃ i ∈ t, U i)

Tactic:
obtain ⟨i, hi⟩ : ∃ i, x ∈ U i := mem_iUnion.1 <| hxU <| subset_closure rfl

Premises used: subset_closure, Set.mem_iUnion, Iff.mp, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hxU : Subset (α := Set X) (closure[inst] {x}) (⋃ (i : ι), U i)
i : ι
hi : x ∈ U i
⊢ ∃ (t : Finset ι), Subset (α := Set X) (closure[inst] {x}) (⋃ i ∈ t, U i)

Tactic:
⟨{i}, fun y hy ↦ ?_⟩

Premises used: Exists.intro, Singleton.singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hxU : Subset (α := Set X) (closure[inst] {x}) (⋃ (i : ι), U i)
i : ι
hi : x ∈ U i
refine :
  ∀ (y : X) (hy : Membership.mem (γ := Set X) (closure[inst] {x}) y),
    Membership.mem (γ := Set X) (⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Finset ι) {i} i_1), U i_1) y
⊢ ∃ (t : Finset ι), Subset (α := Set X) (closure[inst] {x}) (⋃ i ∈ t, U i)

Tactic:
refine ⟨{i}, fun y hy ↦ ?_⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hxU : Subset (α := Set X) (closure[inst] {x}) (⋃ (i : ι), U i)
i : ι
hi : x ∈ U i
y : X
hy : Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ y ⤳ x

Tactic:
rw [← specializes_iff_mem_closure, specializes_comm] at hy

Premises used: specializes_iff_mem_closure, specializes_comm