awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : y ⤳ x
⊢ Membership.mem (γ := Set X) (⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Finset ι) {i} i_1), U i_1) y

Tactic:
simpa using hy.mem_open (hUo i) hi

Premises used: Specializes.mem_open
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
⊢ coclosedCompact X ≤ cofinite

Tactic:
le_cofinite_iff_compl_singleton_mem.2 fun _ ↦
    compl_mem_coclosedCompact.2 isCompact_closure_singleton

Premises used: Iff.mpr, Filter.le_cofinite_iff_compl_singleton_mem, isCompact_closure_singleton, Filter.compl_mem_coclosedCompact
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
s : Set X
⊢ IsBounded s ↔ IsCompact (closure[inst] s)

Tactic:
compl_mem_coclosedCompact

Premises used: Set.Mem, Bornology.IsBounded, Filter.compl_mem_coclosedCompact, Bornology.IsCobounded
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
s : Set X
hs : s.Finite
⊢ IsCompact (closure[inst] s)

Tactic:
let _ : Bornology X := .relativelyCompact X
  Bornology.relativelyCompact.isBounded_iff.1 hs.isBounded

Premises used: Bornology.relativelyCompact.isBounded_iff, Set.Finite.isBounded, Iff.mp, Bornology.relativelyCompact
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
⊢ IsClosed[inst] {x}

Tactic:
T1Space.t1 x

Premises used: T1Space.t1
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
⊢ IsOpen[inst] {x}ᶜ

Tactic:
isClosed_singleton.isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
⊢ IsOpen[inst] {y : X | y ≠ x}

Tactic:
isOpen_compl_singleton

Premises used: Set.Mem, setOf, isOpen_compl_singleton, Set.singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : One X
inst_3 : TopologicalSpace Y
f : Y → X
hf : Continuous[inst_3, inst] f
⊢ IsOpen[inst_3] (mulSupport f)

Tactic:
isOpen_ne.preimage hf

Premises used: Set.Mem, setOf, Set.preimage, isOpen_ne, Function.mulSupport, IsOpen.preimage, Not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
h : x ≠ y
⊢ 𝓝[{y}ᶜ] x = 𝓝 x

Tactic:
isOpen_ne.nhdsWithin_eq h

Premises used: IsOpen.nhdsWithin_eq, Set.Mem, setOf, isOpen_ne, Set.singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
h : x ≠ y
s : Set X
rw : {y}ᶜ ∈ 𝓝[s] x
⊢ 𝓝[s \ {y}] x = 𝓝[s] x

Tactic:
rw [diff_eq, inter_comm, nhdsWithin_inter_of_mem]

Premises used: Set.diff_eq, nhdsWithin_inter_of_mem, Set.inter_comm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ {y}ᶜ ∈ 𝓝[s] x

Tactic:
mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)

Premises used: mem_nhdsWithin_of_mem_nhds, isOpen_ne, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ {y}ᶜ ∈ 𝓝[s] x

Tactic:
exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)

Premises used: mem_nhdsWithin_of_mem_nhds, isOpen_ne, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
inl : 𝓝[≠] x ≤ 𝓝[≠] x
inr : ∀ (hy : x ≠ y), 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x

Tactic:
rcases eq_or_ne x y with rfl | hy

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
⊢ 𝓝[≠] x ≤ 𝓝[≠] x

Tactic:
Eq.le rfl

Premises used: Eq.le, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
⊢ 𝓝[≠] x ≤ 𝓝[≠] x

Tactic:
exact Eq.le rfl

Premises used: Eq.le, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
hy : x ≠ y
inr : 𝓝[≠] x ≤ 𝓝 x
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x

Tactic:
rw [Ne.nhdsWithin_compl_singleton hy]

Premises used: Ne.nhdsWithin_compl_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝 x

Tactic:
nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝 x

Tactic:
exact nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
⊢ IsOpen[inst] {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y}

Tactic:
isOpen_iff_mem_nhds.mpr fun a ha => ?_

Premises used: Iff.mpr, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
refine :
  ∀ (a : X) (ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a),
    {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} ∈ 𝓝 a
⊢ IsOpen[inst] {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y}

Tactic:
refine isOpen_iff_mem_nhds.mpr fun a ha => ?_

Premises used: Iff.mpr, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
h : ∀ (b : X) (hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x), ∀ᶠ (y : X) in 𝓝[≠] b, p y
⊢ {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} ∈ 𝓝 a

Tactic:
filter_upwards [eventually_nhds_nhdsWithin.mpr ha] with b hb

Premises used: Iff.mpr, eventually_nhds_nhdsWithin
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
h : ∀ (hb : ∀ᶠ (x : X) in 𝓝[≠] a, p x), ∀ᶠ (y : X) in 𝓝[≠] a, p y
h₁ : ∀ (h : a ≠ b), ∀ᶠ (y : X) in 𝓝[≠] b, p y
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
rcases eq_or_ne a b 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
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
hb : ∀ᶠ (x : X) in 𝓝[≠] a, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] a, p y

Tactic:
hb
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
hb : ∀ᶠ (x : X) in 𝓝[≠] a, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] a, p y

Tactic:
exact hb
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
h : a ≠ b
⊢ ∀ᶠ (x : X) in 𝓝 b, p x

Tactic:
rw [h.symm.nhdsWithin_compl_singleton] at hb

Premises used: Ne.symm, Ne.nhdsWithin_compl_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
h : a ≠ b
hb₁ : ∀ᶠ (x : X) in 𝓝 b, p x
⊢ a ≠ b

Tactic:
rw [h.symm.nhdsWithin_compl_singleton] at hb

Premises used: Ne.symm, Ne.nhdsWithin_compl_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
b : X
hb : ∀ᶠ (x : X) in 𝓝 b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
hb.filter_mono nhdsWithin_le_nhds

Premises used: Filter.Eventually.filter_mono, nhdsWithin_le_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
b : X
hb : ∀ᶠ (x : X) in 𝓝 b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
exact hb.filter_mono nhdsWithin_le_nhds

Premises used: Filter.Eventually.filter_mono, nhdsWithin_le_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : s.Finite
rw : IsClosed[inst] (⋃ x ∈ s, {x})
⊢ IsClosed[inst] s

Tactic:
rw [← biUnion_of_singleton s]

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed[inst] (⋃ x ∈ s, {x})

Tactic:
hs.isClosed_biUnion fun i _ => isClosed_singleton

Premises used: isClosed_singleton, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed[inst] (⋃ x ∈ s, {x})

Tactic:
exact hs.isClosed_biUnion fun i _ => isClosed_singleton

Premises used: isClosed_singleton, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : x ≠ y
rcases : ∀ (a : Set X) (ab : a ∈ b) (xa : x ∈ a) (ha : a ⊆ {y_1 : X | y_1 ≠ y}), ∃ a ∈ b, x ∈ a ∧ y ∉ a
⊢ ∃ a ∈ b, x ∈ a ∧ y ∉ a

Tactic:
rcases hb.isOpen_iff.1 isOpen_ne x h with ⟨a, ab, xa, ha⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, isOpen_ne, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : x ≠ y
a : Set X
ab : a ∈ b
xa : x ∈ a
ha : a ⊆ {y_1 : X | y_1 ≠ y}
⊢ ∃ a ∈ b, x ∈ a ∧ y ∉ a

Tactic:
⟨a, ab, xa, fun h => ha h rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : x ≠ y
a : Set X
ab : a ∈ b
xa : x ∈ a
ha : a ⊆ {y_1 : X | y_1 ≠ y}
⊢ ∃ a ∈ b, x ∈ a ∧ y ∉ a

Tactic:
exact ⟨a, ab, xa, fun h => ha h rfl⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Finset X
⊢ IsClosed[inst] (↑s : Set X)

Tactic:
s.finite_toSet.isClosed

Premises used: Finset.finite_toSet, Set.Finite.isClosed
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
x : CofiniteTopology X
⊢ Eq (α := Set (CofiniteTopology X)) {x} univ ∨ Set.Finite (α := CofiniteTopology X) {x}

Tactic:
simp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ T1Space X

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ ∀ (x : X), IsClosed[inst] {x}

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}

Tactic:
tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
⊢ ∀ (x : X), IsClosed[inst] {x}

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
⊢ ∀ (x : X), IsOpen[inst] {x}ᶜ

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
⊢ (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ

Tactic:
2 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
⊢ (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ

Tactic:
simp only [isOpen_compl_iff]

Premises used: isOpen_compl_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
⊢ (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ

Tactic:
tfae_have 2 ↔ 3 := by
    simp only [isOpen_compl_iff]
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ ∀ (x : X), IsOpen[inst] {x}ᶜ

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ

Tactic:
5 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ

Tactic:
forall_comm.trans ?_

Premises used: forall_comm, Iff.trans
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
refine : (∀ (b a : X), a ≠ b → {b}ᶜ ∈ 𝓝 a) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ

Tactic:
refine forall_comm.trans ?_

Premises used: forall_comm, Iff.trans
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ (∀ (b a : X), a ≠ b → {b}ᶜ ∈ 𝓝 a) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ

Tactic:
simp only [isOpen_iff_mem_nhds, mem_compl_iff, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, isOpen_iff_mem_nhds, Set.mem_compl_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ

Tactic:
tfae_have 5 ↔ 3 := by
    refine forall_comm.trans ?_
    simp only [isOpen_iff_mem_nhds, mem_compl_iff, mem_singleton_iff]
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s

Tactic:
5 ↔ 6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s

Tactic:
simp only [← subset_compl_singleton_iff, exists_mem_subset_iff]

Premises used: Set.subset_compl_singleton_iff, Filter.exists_mem_subset_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s

Tactic:
tfae_have 5 ↔ 6 := by
    simp only [← subset_compl_singleton_iff, exists_mem_subset_iff]
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
⊢ ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
⊢ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U

Tactic:
7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U

Tactic:
5 ↔ 7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U

Tactic:
simp only [(nhds_basis_opens _).mem_iff, subset_compl_singleton_iff, and_assoc,
      and_left_comm]

Premises used: Set.subset_compl_singleton_iff, Filter.HasBasis.mem_iff, and_left_comm, and_assoc, nhds_basis_opens
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U

Tactic:
tfae_have 5 ↔ 7 := by
    simp only [(nhds_basis_opens _).mem_iff, subset_compl_singleton_iff, and_assoc,
      and_left_comm]
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
⊢ ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
⊢ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)

Tactic:
8

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)

Tactic:
5 ↔ 8

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)

Tactic:
simp only [← principal_singleton, disjoint_principal_right]

Premises used: Filter.principal_singleton, Filter.disjoint_principal_right