awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s ∩ t)

Tactic:
hs.inter_right <| ht.isClosed

Premises used: IsCompact.inter_right, IsCompact.isClosed
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
s : Set X
hs : IsCompact (closure[inst] s)
f : X → Y
hf : ContinuousOn f (closure[inst] s)
⊢ f '' closure[inst] s = closure[inst_1] (f '' s)

Tactic:
Subset.antisymm hf.image_closure <|
    closure_minimal (image_mono subset_closure) (hs.image_of_continuousOn hf).isClosed

Premises used: Set.Subset.antisymm, subset_closure, closure_minimal, Set.image_mono, IsCompact.image_of_continuousOn, ContinuousOn.image_closure, IsCompact.isClosed
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
mp : f x ≠ g x → ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
mpr : (∀ᶠ (x : X) in 𝓝 x, f x ≠ g x) → f x ≠ g x
⊢ f x ≠ g x ↔ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
mp :
  ∀ (Uf Ug : Set Y) (h₁U : IsOpen[inst_1] Uf) (h₂U : IsOpen[inst_1] Ug) (h₃U : f x ∈ Uf) (h₄U : g x ∈ Ug)
    (h₅U : Disjoint Uf Ug), ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
⊢ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

Tactic:
obtain ⟨Uf, Ug, h₁U, h₂U, h₃U, h₄U, h₅U⟩ := t2_separation hfg

Premises used: t2_separation
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x ∈ Uf
h₄U : g x ∈ Ug
h₅U : Disjoint Uf Ug
⊢ Uf ∩ Ug = ∅

Tactic:
rw [Set.disjoint_iff_inter_eq_empty] at h₅U

Premises used: Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : f x ≠ g x
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x ∈ Uf
h₄U : g x ∈ Ug
h₅U : Uf ∩ Ug = ∅
h : ∀ a ∈ f ⁻¹' Uf ∩ g ⁻¹' Ug, f a ≠ g a
⊢ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

Tactic:
filter_upwards [inter_mem
      (hf.preimage_mem_nhds (IsOpen.mem_nhds h₁U h₃U))
      (hg.preimage_mem_nhds (IsOpen.mem_nhds h₂U h₄U))]

Premises used: Filter.inter_mem, ContinuousAt.preimage_mem_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x_1 : X
f g : X → Y
hf : ContinuousAt f x_1
hg : ContinuousAt g x_1
hfg : f x_1 ≠ g x_1
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x_1 ∈ Uf
h₄U : g x_1 ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : x ∈ f ⁻¹' Uf ∩ g ⁻¹' Ug
⊢ f x ∈ Uf ∧ g x ∈ Ug

Tactic:
simp only [Set.mem_inter_iff, Set.mem_preimage] at hx

Premises used: Set.mem_inter_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x_1 : X
f g : X → Y
hf : ContinuousAt f x_1
hg : ContinuousAt g x_1
hfg : f x_1 ≠ g x_1
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x_1 ∈ Uf
h₄U : g x_1 ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : f x ∈ Uf ∧ g x ∈ Ug
h : ∀ (H : f x = g x), False
⊢ f x ≠ g x

Tactic:
by_contra H
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x_1 : X
f g : X → Y
hf : ContinuousAt f x_1
hg : ContinuousAt g x_1
hfg : f x_1 ≠ g x_1
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x_1 ∈ Uf
h₄U : g x_1 ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : f x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
⊢ g x ∈ Uf ∧ g x ∈ Ug

Tactic:
rw [H] at hx
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x_1 : X
f g : X → Y
hf : ContinuousAt f x_1
hg : ContinuousAt g x_1
hfg : f x_1 ≠ g x_1
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x_1 ∈ Uf
h₄U : g x_1 ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : f x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
hx₁ : g x ∈ Uf ∧ g x ∈ Ug
⊢ f x = g x

Tactic:
rw [H] at hx
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x_1 : X
f g : X → Y
hf : ContinuousAt f x_1
hg : ContinuousAt g x_1
hfg : f x_1 ≠ g x_1
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x_1 ∈ Uf
h₄U : g x_1 ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : g x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
⊢ g x ∈ Uf ∩ Ug

Tactic:
have : g x ∈ Uf ∩ Ug := hx
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x_1 : X
f g : X → Y
hf : ContinuousAt f x_1
hg : ContinuousAt g x_1
hfg : f x_1 ≠ g x_1
Uf Ug : Set Y
h₁U : IsOpen[inst_1] Uf
h₂U : IsOpen[inst_1] Ug
h₃U : f x_1 ∈ Uf
h₄U : g x_1 ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : g x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
this : g x ∈ Uf ∩ Ug
⊢ False

Tactic:
simp [h₅U] at this
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
mpr : ∀ (t : Set X) (h₁t : ∀ y ∈ t, f y ≠ g y) (h₂t : IsOpen[inst] t) (h₃t : x ∈ t), f x ≠ g x
⊢ f x ≠ g x

Tactic:
obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hfg

Premises used: eventually_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
t : Set X
h₁t : ∀ y ∈ t, f y ≠ g y
h₂t : IsOpen[inst] t
h₃t : x ∈ t
⊢ f x ≠ g x

Tactic:
h₁t x h₃t
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
t : Set X
h₁t : ∀ y ∈ t, f y ≠ g y
h₂t : IsOpen[inst] t
h₃t : x ∈ t
⊢ f x ≠ g x

Tactic:
exact h₁t x h₃t
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
mp : f =ᶠ[𝓝[≠] x] g → f =ᶠ[𝓝 x] g
mpr : f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
mp : f x = g x
⊢ f =ᶠ[𝓝 x] g

Tactic:
apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE hfg

Premises used: eventuallyEq_nhds_of_eventuallyEq_nhdsNE
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
mp : ∀ (hCon : ¬f x = g x), False
⊢ f x = g x

Tactic:
by_contra hCon
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
hCon : ¬f x = g x
⊢ ∀ᶠ (x : X) in 𝓝[≠] x, f x ≠ g x ∧ f x = g x

Tactic:
have h₁ := (eventually_nhdsWithin_of_eventually_nhds
        ((hf.ne_iff_eventually_ne hg).1 hCon)).and hfg
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
hCon : ¬f x = g x
h₁ : ∀ᶠ (x : X) in 𝓝[≠] x, f x ≠ g x ∧ f x = g x
⊢ ∅ ∉ 𝓝[≠] x

Tactic:
empty_notMem (𝓝[≠] x)

Premises used: Compl.compl, Filter.empty_notMem, nhdsWithin, Singleton.singleton
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
hCon : ¬f x = g x
h₁ : ∀ᶠ (x : X) in 𝓝[≠] x, f x ≠ g x ∧ f x = g x
⊢ ∅ ∉ 𝓝[≠] x

Tactic:
exact empty_notMem (𝓝[≠] x)

Premises used: Compl.compl, Filter.empty_notMem, nhdsWithin, Singleton.singleton
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
hCon : ¬f x = g x
h₁ : ∀ᶠ (x : X) in 𝓝[≠] x, f x ≠ g x ∧ f x = g x
⊢ ∅ ∉ 𝓝[≠] x

Tactic:
have h₂ : ∅ ∉ 𝓝[≠] x := by exact empty_notMem (𝓝[≠] x)
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
hCon : ¬f x = g x
h₁ : ∀ᶠ (x : X) in 𝓝[≠] x, f x ≠ g x ∧ f x = g x
h₂ : ∅ ∉ 𝓝[≠] x
⊢ Set.Nonempty.{u_1} (α := X) {x : X | f x ≠ g x ∧ f x = g x}

Tactic:
simp_all
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
hCon : ¬f x = g x
mp : ∀ (a : X) (ha : Membership.mem (γ := Set X) {x : X | f x ≠ g x ∧ f x = g x} a), False
⊢ False

Tactic:
obtain ⟨a, ha⟩ : {x | f x ≠ g x ∧ f x = g x}.Nonempty := by
      have h₁ := (eventually_nhdsWithin_of_eventually_nhds
        ((hf.ne_iff_eventually_ne hg).1 hCon)).and hfg
      have h₂ : ∅ ∉ 𝓝[≠] x := by exact empty_notMem (𝓝[≠] x)
      simp_all

Premises used: setOf, Ne, And, Set.Nonempty, Eq
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝[≠] x] g
hCon : ¬f x = g x
a : X
ha : Membership.mem (γ := Set X) {x : X | f x ≠ g x ∧ f x = g x} a
⊢ False

Tactic:
simp at ha
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝 x] g
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
hfg.filter_mono nhdsWithin_le_nhds

Premises used: Filter.EventuallyEq.filter_mono, nhdsWithin_le_nhds
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst_3 : (𝓝[≠] x).NeBot
hfg : f =ᶠ[𝓝 x] g
⊢ f =ᶠ[𝓝[≠] x] g

Tactic:
exact hfg.filter_mono nhdsWithin_le_nhds

Premises used: Filter.EventuallyEq.filter_mono, nhdsWithin_le_nhds
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
f : X → Y
h : Continuous[inst, inst_1] f
⊢ IsClosedMap f

Tactic:
fun _s hs => (hs.isCompact.image h).isClosed

Premises used: IsClosedMap, IsClosed.isCompact, IsCompact.image, IsCompact.isClosed
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
f : X → Y
h : Continuous[inst, inst_1] f
hf : Injective f
⊢ IsClosedEmbedding f

Tactic:
.of_continuous_injective_isClosedMap h hf h.isClosedMap

Premises used: Continuous.isClosedMap, Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
inst_3 : T2Space Y
f : X → Y
hsurj : Surjective f
hcont : Continuous[inst, inst_1] f
⊢ IsQuotientMap f

Tactic:
hcont.isClosedMap.isQuotientMap hcont hsurj

Premises used: Continuous.isClosedMap, IsClosedMap.isQuotientMap
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
mp : IsPreirreducible S → ∀ x ∈ S, S ⊆ closure[inst] {x}
mpr : (∀ x ∈ S, S ⊆ closure[inst] {x}) → IsPreirreducible S
⊢ IsPreirreducible S ↔ ∀ x ∈ S, S ⊆ closure[inst] {x}

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
mp : ∀ (e : y ∉ closure[inst] {x}), False
⊢ Membership.mem (γ := Set X) (closure[inst] {x}) y

Tactic:
by_contra e
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
e : y ∉ closure[inst] {x}
mp : ∀ (U V : Set X) (hU : IsOpen[inst] U) (hV : IsOpen[inst] V) (hxU : x ∈ U) (hyV : y ∈ V) (h' : Disjoint U V), False
⊢ False

Tactic:
obtain ⟨U, V, hU, hV, hxU, hyV, h'⟩ := r1_separation fun h => e h.specializes.mem_closure

Premises used: Specializes.mem_closure, Inseparable.specializes, r1_separation
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
e : y ∉ closure[inst] {x}
U V : Set X
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hxU : x ∈ U
hyV : y ∈ V
h' : Disjoint U V
⊢ False

Tactic:
((h U V hU hV ⟨x, hx, hxU⟩ ⟨y, hy, hyV⟩).mono inter_subset_right).not_disjoint h'

Premises used: Set.Nonempty.mono, And.intro, Exists.intro, Set.inter_subset_right, Set.Nonempty.not_disjoint
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
e : y ∉ closure[inst] {x}
U V : Set X
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hxU : x ∈ U
hyV : y ∈ V
h' : Disjoint U V
⊢ False

Tactic:
exact ((h U V hU hV ⟨x, hx, hxU⟩ ⟨y, hy, hyV⟩).mono inter_subset_right).not_disjoint h'

Premises used: Set.Nonempty.mono, And.intro, Exists.intro, Set.inter_subset_right, Set.Nonempty.not_disjoint
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst] {x}
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
mpr : ∀ (x : X) (hxs : x ∈ S) (hxu : x ∈ u), (S ∩ v).Nonempty → (S ∩ (u ∩ v)).Nonempty
⊢ (S ∩ u).Nonempty → (S ∩ v).Nonempty → (S ∩ (u ∩ v)).Nonempty

Tactic:
⟨x, hxs, hxu⟩
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst] {x}
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hxs : x ∈ S
hxu : x ∈ u
mpr : ∀ (y : X) (hys : y ∈ S) (hyv : y ∈ v), (S ∩ (u ∩ v)).Nonempty
⊢ (S ∩ v).Nonempty → (S ∩ (u ∩ v)).Nonempty

Tactic:
⟨y, hys, hyv⟩
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst] {x}
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hxs : x ∈ S
hxu : x ∈ u
y : X
hys : y ∈ S
hyv : y ∈ v
⊢ (S ∩ (u ∩ v)).Nonempty

Tactic:
⟨x, hxs, hxu, (specializes_iff_mem_closure.mpr (h x hxs hys)).mem_open hv hyv⟩

Premises used: Iff.mpr, Specializes.mem_open, specializes_iff_mem_closure, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
S : Set X
h : ∀ x ∈ S, S ⊆ closure[inst] {x}
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
x : X
hxs : x ∈ S
hxu : x ∈ u
y : X
hys : y ∈ S
hyv : y ∈ v
⊢ (S ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, hxs, hxu, (specializes_iff_mem_closure.mpr (h x hxs hys)).mem_open hv hyv⟩
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
S : Set X
⊢ IsPreirreducible S ↔ S.Subsingleton

Tactic:
simp [isPreirreducible_iff_forall_mem_subset_closure_singleton, Set.Subsingleton, eq_comm]

Premises used: eq_comm, Set.Subsingleton, isPreirreducible_iff_forall_mem_subset_closure_singleton
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
S : Set X
h : IsPreirreducible S
⊢ S.Subsingleton

Tactic:
isPreirreducible_iff_subsingleton.1 h

Premises used: Iff.mp, isPreirreducible_iff_subsingleton
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
S : Set X
rw : S.Nonempty ∧ IsPreirreducible S ↔ ∃ (x : X), S = {x}
rw₁ : S.Nonempty ∧ S.Subsingleton ↔ ∃ (x : X), S = {x}
rw₂ rw₃ : S.Nonempty ∧ S.Subsingleton ↔ S.Nonempty ∧ S.Subsingleton
⊢ IsIrreducible S ↔ ∃ (x : X), S = {x}

Tactic:
rw [IsIrreducible, isPreirreducible_iff_subsingleton,
    exists_eq_singleton_iff_nonempty_subsingleton]

Premises used: IsIrreducible, Set.exists_eq_singleton_iff_nonempty_subsingleton, isPreirreducible_iff_subsingleton
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_4
inst : TopologicalSpace X
inst_1 : PreirreducibleSpace X
inst_2 : Nontrivial X
inst_3 : T2Space X
⊢ False

Tactic:
(PreirreducibleSpace.isPreirreducible_univ (X := X)).subsingleton.not_nontrivial nontrivial_univ

Premises used: PreirreducibleSpace.isPreirreducible_univ, IsPreirreducible.subsingleton, Set.Subsingleton.not_nontrivial, Set.nontrivial_univ
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_4
⊢ Antitone (@T2Space X)

Tactic:
fun inst₁ inst₂ h_top h_t2 ↦ @T2Space.of_injective_continuous _ _ inst₁ inst₂
    h_t2 _ Function.injective_id <| continuous_id_of_le h_top

Premises used: continuous_id_of_le, T2Space.of_injective_continuous, Function.injective_id, Antitone
-- Module: Mathlib.Topology.Separation.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T35Space X
h : Cardinal.mk X < Cardinal.continuum
⊢ TotallySeparatedSpace X

Tactic:
totallySeparatedSpace_of_t0_of_basis_clopen <|
    CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum h

Premises used: CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum, totallySeparatedSpace_of_t0_of_basis_clopen
-- Module: Mathlib.Topology.Separation.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T35Space X
inst_2 : Countable X
⊢ TotallySeparatedSpace X

Tactic:
totallySeparatedSpace_of_cardinalMk_lt_continuum <|
    (Cardinal.mk_le_aleph0_iff.mpr inferInstance).trans_lt Cardinal.aleph0_lt_continuum

Premises used: Iff.mpr, CompletelyRegularSpace.totallySeparatedSpace_of_cardinalMk_lt_continuum, Cardinal.mk_le_aleph0_iff, inferInstance, LE.le.trans_lt, Cardinal.aleph0_lt_continuum
-- Module: Mathlib.Topology.Separation.Lemmas
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T35Space X
s : Set X
h : s.Countable
⊢ TotallySeparatedSpace.{u_1} (↑s : Type u_1)

Tactic:
have : _root_.Countable s := h
  inferInstanceAs (TotallySeparatedSpace s)

Premises used: _private.0.Set.Countable.totallySeparatedSpace._proof_1
-- Module: Mathlib.Topology.Separation.Lemmas
Goal:
X : Type u_1
inst : MetricSpace X
s : Set X
hs : s.Countable
rw : TotallyDisconnectedSpace.{u_1} (↑s : Type u_1)
⊢ IsTotallyDisconnected s

Tactic:
rw [← totallyDisconnectedSpace_subtype_iff]

Premises used: totallyDisconnectedSpace_subtype_iff
-- Module: Mathlib.Topology.Separation.Lemmas
Goal:
X : Type u_1
inst : MetricSpace X
s : Set X
hs : s.Countable
⊢ Countable.{u_1 + 1} (↑s : Type u_1)

Tactic:
have : Countable s := hs
-- Module: Mathlib.Topology.Separation.Lemmas
Goal:
X : Type u_1
inst : MetricSpace X
s : Set X
hs : s.Countable
this : Countable.{u_1 + 1} (↑s : Type u_1)
⊢ TotallyDisconnectedSpace.{u_1} (↑s : Type u_1)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
obtain : ∀ (hcst : Disjoint (closure ∅) t) (hsct : Disjoint ∅ (closure t)), Disjoint (nhdsSet ∅) (nhdsSet t)
inr : ∀ (a : α) (ha : a ∈ s), Disjoint (nhdsSet s) (nhdsSet t)
⊢ Disjoint (nhdsSet s) (nhdsSet t)

Tactic:
obtain (rfl | ⟨a, ha⟩) := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
t : Set α
hcst : Disjoint (closure ∅) t
hsct : Disjoint ∅ (closure t)
⊢ Disjoint (nhdsSet ∅) (nhdsSet t)

Tactic:
simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
t : Set α
hcst : Disjoint (closure ∅) t
hsct : Disjoint ∅ (closure t)
⊢ Disjoint (nhdsSet ∅) (nhdsSet t)

Tactic:
case inl => simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
obtain : ∀ (hcst : Disjoint (closure s) ∅) (hsct : Disjoint s (closure ∅)), Disjoint (nhdsSet s) (nhdsSet ∅)
inr : ∀ (b : α) (hb : b ∈ t), Disjoint (nhdsSet s) (nhdsSet t)
⊢ Disjoint (nhdsSet s) (nhdsSet t)

Tactic:
obtain (rfl | ⟨b, hb⟩) := t.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s : Set α
a : α
ha : a ∈ s
hcst : Disjoint (closure s) ∅
hsct : Disjoint s (closure ∅)
⊢ Disjoint (nhdsSet s) (nhdsSet ∅)

Tactic:
simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s : Set α
a : α
ha : a ∈ s
hcst : Disjoint (closure s) ∅
hsct : Disjoint s (closure ∅)
⊢ Disjoint (nhdsSet s) (nhdsSet ∅)

Tactic:
case inl => simp
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
inr : False
⊢ Disjoint (nhdsSet s) (nhdsSet t)

Tactic:
exfalso
-- Module: Mathlib.Topology.Separation.LinearUpperLowerSetTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : Topology.IsUpperSet α
s t : Set α
hcst : Disjoint (closure s) t
hsct : Disjoint s (closure t)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
inr :
  ∀ (ha : a ∈ s) (b : α) (hsct : Disjoint (α := Set α) {a} (closure {b}))
    (hcst : Disjoint (α := Set α) (closure {a}) {b}) (hb : b ∈ t), False
⊢ False

Tactic:
grewrite [← singleton_subset_iff.mpr ha, ← singleton_subset_iff.mpr hb] at hcst hsct

Premises used: Iff.mpr, Set.singleton_subset_iff