awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι), T1Space.{u_4} (X i)
⊢ T1Space ((i : ι) → X i)

Tactic:
⟨fun f => univ_pi_singleton f ▸ isClosed_set_pi fun _ _ => isClosed_singleton⟩

Premises used: Eq.rec, isClosed_set_pi, T1Space.mk, Set.univ_pi_singleton, isClosed_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
⊢ T1Space (ULift.{u_3, u_1} X)

Tactic:
IsEmbedding.uliftDown.t1Space

Premises used: Topology.IsEmbedding.uliftDown, Topology.IsEmbedding.t1Space
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
⊢ T0Space X

Tactic:
(t1Space_iff_t0Space_and_r0Space.mp ‹T1Space X›).left

Premises used: And.left, Iff.mp, t1Space_iff_t0Space_and_r0Space
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
⊢ {x}ᶜ ∈ 𝓝 y ↔ y ≠ x

Tactic:
isOpen_compl_singleton.mem_nhds_iff

Premises used: Set.Mem, setOf, isOpen_compl_singleton, IsOpen.mem_nhds_iff, Set.singleton, Not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
h : y ≠ x
⊢ {x}ᶜ ∈ 𝓝 y

Tactic:
compl_singleton_mem_nhds_iff.mpr h

Premises used: Iff.mpr, compl_singleton_mem_nhds_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
⊢ Eq (α := Set X) (closure[inst] {x}) {x}

Tactic:
isClosed_singleton.closure_eq

Premises used: IsClosed.closure_eq, isClosed_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : s.Subsingleton
inl : ∀ (hs : Set.Subsingleton.{u_1} (α := X) ∅), IsClosed[inst] ∅
inr : ∀ (x : X) (hs : Set.Subsingleton (α := X) {x}), IsClosed[inst] {x}
⊢ IsClosed[inst] s

Tactic:
rcases hs.eq_empty_or_singleton with rfl | ⟨x, rfl⟩

Premises used: Set.Subsingleton.eq_empty_or_singleton, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
hs : Set.Subsingleton.{u_1} (α := X) ∅
⊢ IsClosed[inst] ∅

Tactic:
isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
hs : Set.Subsingleton.{u_1} (α := X) ∅
⊢ IsClosed[inst] ∅

Tactic:
exact isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
hs : Set.Subsingleton (α := X) {x}
⊢ IsClosed[inst] {x}

Tactic:
isClosed_singleton

Premises used: isClosed_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
hs : Set.Subsingleton (α := X) {x}
⊢ IsClosed[inst] {x}

Tactic:
exact isClosed_singleton

Premises used: isClosed_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : s.Subsingleton
⊢ closure[inst] s = s

Tactic:
hs.isClosed.closure_eq

Premises used: Set.Subsingleton.isClosed, IsClosed.closure_eq
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs rwa rwa₁ rwa₂ rwa₃ : s.Subsingleton
⊢ (closure[inst] s).Subsingleton

Tactic:
rwa [hs.closure_eq]

Premises used: Set.Subsingleton.closure_eq
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
⊢ (closure[inst] s).Subsingleton ↔ s.Subsingleton

Tactic:
⟨fun h => h.anti subset_closure, fun h => h.closure⟩

Premises used: subset_closure, Iff.intro, Set.Subsingleton.anti, Set.Subsingleton.closure
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
y : Y
s : Set X
h : IsClosed[inst] s
h2s : s.Nonempty
simp_rw : IsClosed[inst_1] ((fun (a : X) ↦ y) '' s)
simp_rw₁ : IsClosed[inst_1] {y}
⊢ IsClosed[inst_1] (const X y '' s)

Tactic:
simp_rw [const, h2s.image_const, isClosed_singleton]

Premises used: Set.Nonempty.image_const, Function.const, isClosed_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x : X
⊢ IsClosedMap (Y := X × Y) fun (y : Y) ↦ (x, y)

Tactic:
fun _K hK ↦ Set.singleton_prod ▸ isClosed_singleton.prod hK

Premises used: Eq.rec, Set.singleton_prod, IsClosedMap, IsClosed.prod, isClosed_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
y : Y
⊢ IsClosedMap (Y := X × Y) fun (x : X) ↦ (x, y)

Tactic:
fun _K hK ↦ Set.prod_singleton ▸ hK.prod isClosed_singleton

Premises used: Eq.rec, IsClosedMap, Set.prod_singleton, IsClosed.prod, isClosed_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
⊢ 𝓝[insert y s] x = 𝓝[s] x

Tactic:
le_antisymm (Filter.le_def.2 fun t ht => ?_) (nhdsWithin_mono x <| subset_insert y s)

Premises used: Iff.mpr, le_antisymm, Set.subset_insert, nhdsWithin_mono, Filter.le_def
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
refine : ∀ (t : Set X) (ht : t ∈ 𝓝[s] x), t ∈ 𝓝[insert y s] x
⊢ 𝓝[insert y s] x = 𝓝[s] x

Tactic:
refine le_antisymm (Filter.le_def.2 fun t ht => ?_) (nhdsWithin_mono x <| subset_insert y s)

Premises used: Iff.mpr, le_antisymm, Set.subset_insert, nhdsWithin_mono, Filter.le_def
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
obtain : ∀ (o : Set X) (ho : IsOpen[inst] o) (hxo : x ∈ o) (host : o ∩ s ⊆ t), t ∈ 𝓝[insert y s] x
⊢ t ∈ 𝓝[insert y s] x

Tactic:
obtain ⟨o, ho, hxo, host⟩ := mem_nhdsWithin.mp ht

Premises used: mem_nhdsWithin, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen[inst] o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ t ∈ 𝓝[insert y s] x

Tactic:
mem_nhdsWithin.mpr ⟨o \ {y}, ho.sdiff isClosed_singleton, ⟨hxo, hxy⟩, ?_⟩

Premises used: Iff.mpr, mem_nhdsWithin, SDiff.sdiff, IsOpen.sdiff, And.intro, Exists.intro, Singleton.singleton, isClosed_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen[inst] o
hxo : x ∈ o
host : o ∩ s ⊆ t
refine : o \ {y} ∩ insert y s ⊆ t
⊢ t ∈ 𝓝[insert y s] x

Tactic:
refine mem_nhdsWithin.mpr ⟨o \ {y}, ho.sdiff isClosed_singleton, ⟨hxo, hxy⟩, ?_⟩

Premises used: Iff.mpr, mem_nhdsWithin, SDiff.sdiff, IsOpen.sdiff, And.intro, Exists.intro, Singleton.singleton, isClosed_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen[inst] o
hxo : x ∈ o
host : o ∩ s ⊆ t
rw : o \ {y} ∩ s ⊆ t
⊢ o \ {y} ∩ insert y s ⊆ t

Tactic:
rw [inter_insert_of_notMem <| notMem_diff_of_mem (mem_singleton y)]

Premises used: Set.mem_singleton, Set.inter_insert_of_notMem, Set.notMem_diff_of_mem
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen[inst] o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ o \ {y} ∩ s ⊆ t

Tactic:
(inter_subset_inter diff_subset Subset.rfl).trans host

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.inter_subset_inter, Set.Subset.rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen[inst] o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ o \ {y} ∩ s ⊆ t

Tactic:
exact (inter_subset_inter diff_subset Subset.rfl).trans host

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.inter_subset_inter, Set.Subset.rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
inl : ∀ (hu : t ⊆ insert x s), insert x s ∈ 𝓝[t] x
inr : ∀ (h : x ≠ y), insert x s ∈ 𝓝[t] x
⊢ insert x s ∈ 𝓝[t] x

Tactic:
rcases eq_or_ne x y with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s t : Set X
hu : t ⊆ insert x s
⊢ insert x s ∈ 𝓝[t] x

Tactic:
mem_of_superset self_mem_nhdsWithin hu

Premises used: self_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s t : Set X
hu : t ⊆ insert x s
⊢ insert x s ∈ 𝓝[t] x

Tactic:
exact mem_of_superset self_mem_nhdsWithin hu

Premises used: self_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[t] x

Tactic:
nhdsWithin_mono x hu ?_

Premises used: nhdsWithin_mono
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
inr : insert x s ∈ 𝓝[insert y s] x
⊢ insert x s ∈ 𝓝[t] x

Tactic:
refine nhdsWithin_mono x hu ?_

Premises used: nhdsWithin_mono
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
inr : insert x s ∈ 𝓝[s] x
⊢ insert x s ∈ 𝓝[insert y s] x

Tactic:
rw [nhdsWithin_insert_of_ne h]

Premises used: nhdsWithin_insert_of_ne
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[s] x

Tactic:
mem_of_superset self_mem_nhdsWithin (subset_insert x s)

Premises used: self_mem_nhdsWithin, Set.subset_insert, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
s t : Set X
hu : t ⊆ insert y s
h : x ≠ y
⊢ insert x s ∈ 𝓝[s] x

Tactic:
exact mem_of_superset self_mem_nhdsWithin (subset_insert x s)

Premises used: self_mem_nhdsWithin, Set.subset_insert, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
simp_rw : ∀ (h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t), ∀ᶠ (x_1 : X) in 𝓝 x, x_1 ∈ insert x s ↔ x_1 ∈ insert x t
⊢ insert x s =ᶠ[𝓝 x] insert x t

Tactic:
simp_rw [eventuallyEq_set] at h ⊢

Premises used: Filter.eventuallyEq_set
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
simp_rw : ∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, x_1 ∈ insert x s ↔ x_1 ∈ insert x t

Tactic:
simp_rw [← union_singleton, ← nhdsWithin_univ, ← compl_union_self {x},
    nhdsWithin_union, eventually_sup, nhdsWithin_singleton,
    eventually_pure, union_singleton, mem_insert_iff, true_or, and_true]

Premises used: nhdsWithin_singleton, and_true, nhdsWithin_univ, true_or, nhdsWithin_union, Set.compl_union_self, Filter.eventually_pure, Filter.eventually_sup, Set.mem_insert_iff, Singleton.singleton, Set.union_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x y_1 : X
h : ∀ᶠ (x : X) in 𝓝[{y_1}ᶜ] x, x ∈ s ↔ x ∈ t
y : X
⊢ (y ∈ s ↔ y ∈ t) → (y = x ∨ y ∈ s ↔ y = x ∨ y ∈ t)

Tactic:
or_congr (Iff.rfl)

Premises used: or_congr, Iff.rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
h₁ :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x_1 : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ s ↔ x ∈ t) x} x_1 →
          Membership.mem (γ := Set X) {x_2 : X | (fun (x_3 : X) ↦ x_3 = x ∨ x_3 ∈ s ↔ x_3 = x ∨ x_3 ∈ t) x_2} x_1}
      a
h₂ h₃ : ∀ (y : X), (y ∈ s ↔ y ∈ t) → (y = x ∨ y ∈ s ↔ y = x ∨ y ∈ t)
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t

Tactic:
filter_upwards [nhdsWithin_compl_singleton_le x y h] with y using or_congr (Iff.rfl)

Premises used: or_congr, Iff.rfl, nhdsWithin_compl_singleton_le
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
⊢ (𝓝 x).ker = {x}

Tactic:
simp [ker_nhds_eq_specializes]

Premises used: ker_nhds_eq_specializes
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
x : X
h : (𝓝 x).HasBasis p s
rw : (𝓝 x).ker = {x}
rw₁ rw₂ : Eq (α := Set X) {x} {x}
⊢ Eq (α := Set X) (⋂ (i : ι), ⋂ (_ : p i), s i) {x}

Tactic:
rw [← h.ker, ker_nhds]

Premises used: Filter.HasBasis.ker, ker_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
rw : s ⊆ {x}ᶜ ↔ x ∉ s
rw₁ rw₂ : x ∉ s ↔ x ∉ s
⊢ {x}ᶜ ∈ 𝓝ˢ s ↔ x ∉ s

Tactic:
rw [isOpen_compl_singleton.mem_nhdsSet, subset_compl_singleton_iff]

Premises used: Set.subset_compl_singleton_iff, isOpen_compl_singleton, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t

Tactic:
⟨?_, fun h => monotone_nhdsSet h⟩

Premises used: Iff.intro, monotone_nhdsSet
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
refine : 𝓝ˢ s ≤ 𝓝ˢ t → s ⊆ t
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t

Tactic:
refine ⟨?_, fun h => monotone_nhdsSet h⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
h : ∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s
x : X
hx : x ∈ s
⊢ {x}ᶜ ∈ 𝓝ˢ t → {x}ᶜ ∈ 𝓝ˢ s

Tactic:
specialize h {x}ᶜ

Premises used: Compl.compl, Singleton.singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : {x}ᶜ ∈ 𝓝ˢ t → {x}ᶜ ∈ 𝓝ˢ s
⊢ x ∉ t → x ∉ s

Tactic:
simp_rw [compl_singleton_mem_nhdsSet_iff] at h

Premises used: compl_singleton_mem_nhdsSet_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
by_contra : ∀ (hxt : x ∉ t), False
⊢ x ∈ t

Tactic:
by_contra hxt
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
hxt : x ∉ t
⊢ False

Tactic:
h hxt hx
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
hxt : x ∉ t
⊢ False

Tactic:
exact h hxt hx
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
simp_rw : 𝓝ˢ s ≤ 𝓝ˢ t ∧ 𝓝ˢ t ≤ 𝓝ˢ s ↔ s ≤ t ∧ t ≤ s
⊢ 𝓝ˢ s = 𝓝ˢ t ↔ s = t

Tactic:
simp_rw [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ∧ 𝓝ˢ t ≤ 𝓝ˢ s ↔ s ≤ t ∧ t ≤ s

Tactic:
and_congr nhdsSet_le_iff nhdsSet_le_iff

Premises used: nhdsSet_le_iff, and_congr
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ∧ 𝓝ˢ t ≤ 𝓝ˢ s ↔ s ≤ t ∧ t ≤ s

Tactic:
exact and_congr nhdsSet_le_iff nhdsSet_le_iff

Premises used: nhdsSet_le_iff, and_congr
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
⊢ Injective.{u_1 + 1, u_1 + 1} (α := Set X) 𝓝ˢ

Tactic:
fun _ _ hst =>
  nhdsSet_inj_iff.mp hst

Premises used: nhdsSet_inj_iff, Iff.mp, Function.Injective
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
⊢ StrictMono.{u_1, u_1} (α := Set X) 𝓝ˢ

Tactic:
monotone_nhdsSet.strictMono_of_injective injective_nhdsSet

Premises used: injective_nhdsSet, Monotone.strictMono_of_injective, monotone_nhdsSet
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x : X
rw : 𝓝ˢ {x} ≤ 𝓝ˢ s ↔ x ∈ s
rw₁ : {x} ⊆ s ↔ x ∈ s
rw₂ rw₃ : x ∈ s ↔ x ∈ s
⊢ 𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s

Tactic:
rw [← nhdsSet_singleton, nhdsSet_le_iff, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, nhdsSet_le_iff, nhdsSet_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : Dense s
x : X
inst_2 : (𝓝[≠] x).NeBot
⊢ Dense (s \ {x})

Tactic:
hs.inter_of_isOpen_right (dense_compl_singleton x) isOpen_compl_singleton

Premises used: Set.Mem, Set.diff, setOf, isOpen_compl_singleton, Dense.inter_of_isOpen_right, dense_compl_singleton, Not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
⊢ Dense (s \ (↑∅ : Set X))

Tactic:
simpa using hs
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a : X
s_1 : Finset X
h : a ∉ s_1
ih : Dense (s \ (↑s_1 : Set X))
insert : Dense ((s \ (↑s_1 : Set X)) \ {a})
⊢ Dense (s \ (↑(Insert.insert a s_1) : Set X))

Tactic:
rw [Finset.coe_insert, ← union_singleton, ← diff_diff]

Premises used: Set.diff_diff, Finset.coe_insert, Set.union_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a : X
s_1 : Finset X
h : a ∉ s_1
ih : Dense (s \ (↑s_1 : Set X))
⊢ Dense ((s \ (↑s_1 : Set X)) \ {a})

Tactic:
ih.diff_singleton _

Premises used: Dense.diff_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a : X
s_1 : Finset X
h : a ∉ s_1
ih : Dense (s \ (↑s_1 : Set X))
⊢ Dense ((s \ (↑s_1 : Set X)) \ {a})

Tactic:
exact ih.diff_singleton _

Premises used: Dense.diff_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Finset X
empty : Dense (s \ (↑∅ : Set X))
insert :
  ∀ (a : X) (s_1 : Finset X),
    a ∉ s_1 → ∀ (ih : Dense (s \ (↑s_1 : Set X))), Dense (s \ (↑(Insert.insert a s_1) : Set X))
⊢ Dense (s \ (↑t : Set X))

Tactic:
induction t using Finset.induction_on with
  | empty => simpa using hs
  | insert _ _ _ ih =>
    rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
    exact ih.diff_singleton _

Premises used: Insert.insert, Set.diff_diff, Finset.coe_insert, Set.union_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Finset X
empty : Dense (s \ (↑∅ : Set X))
insert :
  ∀ (a : X) (s_1 : Finset X),
    a ∉ s_1 → ∀ (ih : Dense (s \ (↑s_1 : Set X))), Dense (s \ (↑(Insert.insert a s_1) : Set X))
⊢ Dense (s \ (↑t : Set X))

Tactic:
classical
  induction t using Finset.induction_on with
  | empty => simpa using hs
  | insert _ _ _ ih =>
    rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
    exact ih.diff_singleton _

Premises used: Insert.insert, Set.diff_diff, Finset.coe_insert, Set.union_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ Dense (s \ (↑(ht.toFinset (s := t)) : Set X))

Tactic:
hs.diff_finset ht.toFinset

Premises used: Dense.diff_finset, Set.Finite.toFinset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
h : t = (↑(ht.toFinset (s := t)) : Set X)
⊢ Dense (s \ t)

Tactic:
convert! hs.diff_finset ht.toFinset

Premises used: Dense.diff_finset, Set.Finite.toFinset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ t = (↑(ht.toFinset (s := t)) : Set X)

Tactic:
(Finite.coe_toFinset _).symm

Premises used: Set.Finite.coe_toFinset, Eq.symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ t = (↑(ht.toFinset (s := t)) : Set X)

Tactic:
exact (Finite.coe_toFinset _).symm

Premises used: Set.Finite.coe_toFinset, Eq.symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
f : X → Y
x : X
y : Y
h : Tendsto f (𝓝 x) (𝓝 y)
⊢ f x = y

Tactic:
by_contra fun hfa : f x ≠ y =>
    have fact₁ : {f x}ᶜ ∈ 𝓝 y := compl_singleton_mem_nhds hfa.symm
    have fact₂ : Tendsto f (pure x) (𝓝 y) := h.comp (tendsto_id'.2 <| pure_le_nhds x)
    fact₂ fact₁ (Eq.refl <| f x)

Premises used: Iff.mpr, pure_le_nhds, Filter.tendsto_id', Ne.symm, compl_singleton_mem_nhds, by_contra, Eq.refl, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
Y : Type u_2
X : Type u_3
inst : TopologicalSpace Y
inst_1 : T1Space Y
g : X → Y
l : Filter X
b₁ b₂ : Y
hg : Tendsto g l (𝓝 b₁)
hb : b₁ ≠ b₂
⊢ ∀ᶠ (z : X) in l, g z ≠ b₂

Tactic:
hg.eventually (isOpen_compl_singleton.eventually_mem hb)

Premises used: Set.Mem, IsOpen.eventually_mem, setOf, isOpen_compl_singleton, Set.singleton, Filter.Tendsto.eventually, Not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
g : X → Y
x : X
y : Y
hg1 : ContinuousAt g x
hg2 : g x ≠ y
⊢ ∀ᶠ (z : X) in 𝓝 x, g z ≠ y

Tactic:
hg1.tendsto.eventually_ne hg2

Premises used: Filter.Tendsto.eventually_ne, ContinuousAt.tendsto
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
a b : X
h : a ≠ b
⊢ ∀ᶠ (x : X) in 𝓝 a, x ≠ b

Tactic:
IsOpen.eventually_mem isOpen_ne h

Premises used: Set.Mem, IsOpen.eventually_mem, isOpen_ne, Not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
a b : X
s : Set X
h : a ≠ b
⊢ ∀ᶠ (x : X) in 𝓝[s] a, x ≠ b

Tactic:
Filter.Eventually.filter_mono nhdsWithin_le_nhds <| eventually_ne_nhds h

Premises used: Filter.Eventually.filter_mono, eventually_ne_nhds, nhdsWithin_le_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
nth_rw : (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (x : X) in 𝓝[s] a, p x

Tactic:
nth_rw 2 [← eventually_eventually_nhdsWithin]

Premises used: eventually_eventually_nhdsWithin
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
mp : (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
mpr : (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x

Tactic:
constructor