awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
E : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
h₁ : ContinuousOn g₁ s
h₂ : ContinuousOn g₂ s
he : s.restrict (π := fun (a : A) ↦ X) (p ∘ g₁) = s.restrict (π := fun (a : A) ↦ X) (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
rw :
  ∀ (h₁ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₁))
    (h₂ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₂))
    (he : s.restrict (π := fun (a : A) ↦ X) (p ∘ g₁) = s.restrict (π := fun (a : A) ↦ X) (p ∘ g₂)) {a : A} (has : a ∈ s)
    (ha : g₁ a = g₂ a), s.restrict (π := fun (a : A) ↦ E) g₁ = s.restrict (π := fun (a : A) ↦ E) g₂
⊢ s.restrict (π := fun (a : A) ↦ E) g₁ = s.restrict (π := fun (a : A) ↦ E) g₂

Tactic:
rw [continuousOn_iff_continuous_restrict] at h₁ h₂

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
E : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
h₁ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₁)
h₂ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₂)
he : s.restrict (π := fun (a : A) ↦ X) (p ∘ g₁) = s.restrict (π := fun (a : A) ↦ X) (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
rw :
  ∀ (hs : PreconnectedSpace.{u_3} (↑s : Type u_3))
    (h₁ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₁))
    (h₂ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₂))
    (he : s.restrict (π := fun (a : A) ↦ X) (p ∘ g₁) = s.restrict (π := fun (a : A) ↦ X) (p ∘ g₂)) {a : A} (has : a ∈ s)
    (ha : g₁ a = g₂ a), s.restrict (π := fun (a : A) ↦ E) g₁ = s.restrict (π := fun (a : A) ↦ E) g₂
⊢ s.restrict (π := fun (a : A) ↦ E) g₁ = s.restrict (π := fun (a : A) ↦ E) g₂

Tactic:
rw [isPreconnected_iff_preconnectedSpace] at hs

Premises used: isPreconnected_iff_preconnectedSpace
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
E : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : PreconnectedSpace.{u_3} (↑s : Type u_3)
h₁ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₁)
h₂ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₂)
he : s.restrict (π := fun (a : A) ↦ X) (p ∘ g₁) = s.restrict (π := fun (a : A) ↦ X) (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ s.restrict (π := fun (a : A) ↦ E) g₁ = s.restrict (π := fun (a : A) ↦ E) g₂

Tactic:
sep.eq_of_comp_eq inj h₁ h₂ he ⟨a, has⟩ ha

Premises used: Subtype.mk, IsSeparatedMap.eq_of_comp_eq
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
E : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : PreconnectedSpace.{u_3} (↑s : Type u_3)
h₁ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₁)
h₂ : Continuous[instTopologicalSpaceSubtype, inst] (s.restrict (π := fun (a : A) ↦ E) g₂)
he : s.restrict (π := fun (a : A) ↦ X) (p ∘ g₁) = s.restrict (π := fun (a : A) ↦ X) (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ s.restrict (π := fun (a : A) ↦ E) g₁ = s.restrict (π := fun (a : A) ↦ E) g₂

Tactic:
exact sep.eq_of_comp_eq inj h₁ h₂ he ⟨a, has⟩ ha

Premises used: Subtype.mk, IsSeparatedMap.eq_of_comp_eq
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
E : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace A
p : E → X
g : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
inst_2 : PreconnectedSpace A
cont : Continuous[inst_1, inst] g
he : ∀ (a a' : A), p (g a) = p (g a')
a a' : A
⊢ g a = g a'

Tactic:
congr_fun (sep.eq_of_comp_eq inj cont continuous_const (funext fun a ↦ he a a') a' rfl) a

Premises used: continuous_const, funext, IsSeparatedMap.eq_of_comp_eq, congr_fun, rfl
-- Module: Mathlib.Topology.SeparatedMap
Goal:
X : Type u_1
E : Type u_2
A : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace A
p : E → X
s : Set A
g : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
cont : ContinuousOn g s
he : ∀ a ∈ s, ∀ a' ∈ s, p (g a) = p (g a')
a a' : A
ha : a ∈ s
ha' : a' ∈ s
⊢ g a = g a'

Tactic:
sep.eqOn_of_comp_eqOn inj hs cont continuous_const.continuousOn
    (fun a ha ↦ he a ha a' ha') ha' rfl ha

Premises used: Continuous.continuousOn, continuous_const, IsSeparatedMap.eqOn_of_comp_eqOn, rfl
-- Module: Mathlib.Topology.Separation.AlexandrovDiscrete
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
h : ∀ (x : X), x ∈ nhdsKer s ↔ x ∈ s
⊢ nhdsKer s = s

Tactic:
ext
-- Module: Mathlib.Topology.Separation.AlexandrovDiscrete
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x : X
⊢ x ∈ nhdsKer s ↔ x ∈ s

Tactic:
simp [mem_nhdsKer_iff_specializes]

Premises used: mem_nhdsKer_iff_specializes
-- Module: Mathlib.Topology.Separation.AlexandrovDiscrete
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : AlexandrovDiscrete X
inst_2 : T1Space X
⊢ DiscreteTopology X

Tactic:
simp [discreteTopology_iff_nhds, ← principal_nhdsKer_singleton]

Premises used: principal_nhdsKer_singleton, discreteTopology_iff_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ T0Space X ↔ ∀ (x y : X), Inseparable x y → x = y

Tactic:
⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩

Premises used: _private.0.t0Space_iff_inseparable.match_1, T0Space.mk, Iff.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun (x y : X) ↦ ¬Inseparable x y

Tactic:
simp only [t0Space_iff_inseparable, Ne, not_imp_not, Pairwise]

Premises used: t0Space_iff_inseparable, Ne, Pairwise, not_imp_not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
x y : X
h : Inseparable x y
⊢ x = y

Tactic:
T0Space.t0 h

Premises used: T0Space.t0
-- 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
f : X → Y
hf : IsInducing f
⊢ Injective f

Tactic:
fun _ _ h =>
  (hf.inseparable_iff.1 <| .of_eq h).eq

Premises used: Inseparable.of_eq, Inseparable.eq, Iff.mp, Function.Injective, Topology.IsInducing.inseparable_iff
-- 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
f : X → Y
hf : IsInducing f
⊢ IsEmbedding f

Tactic:
⟨hf, hf.injective⟩

Premises used: Topology.IsInducing.injective, Topology.IsEmbedding.mk
-- 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
f : X → Y
⊢ IsEmbedding f ↔ IsInducing f

Tactic:
⟨IsEmbedding.isInducing, IsInducing.isEmbedding⟩

Premises used: Topology.IsEmbedding.isInducing, Topology.IsInducing.isEmbedding, Iff.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ T0Space X ↔ Injective.{u + 1, u + 1} (α := X) 𝓝

Tactic:
t0Space_iff_inseparable X

Premises used: t0Space_iff_inseparable, Function.Injective, Inseparable
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
⊢ Injective.{u_1 + 1, u_1 + 1} (α := X) 𝓝

Tactic:
(t0Space_iff_nhds_injective X).1 ‹_›

Premises used: t0Space_iff_nhds_injective, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
x y : X
⊢ Inseparable x y ↔ x = y

Tactic:
nhds_injective.eq_iff

Premises used: Function.Injective.eq_iff, nhds_injective, Inseparable
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
a b : X
⊢ 𝓝 a = 𝓝 b ↔ a = b

Tactic:
nhds_injective.eq_iff

Premises used: Function.Injective.eq_iff, nhds_injective
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
⊢ Eq.{u_1 + 1} (α := (x y : X) → Prop) Inseparable Eq

Tactic:
funext₂ fun _ _ => propext inseparable_iff_eq

Premises used: funext₂, inseparable_iff_eq, propext
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : ∀ s ∈ b, x ∈ s ↔ y ∈ s
⊢ (𝓝 y).HasBasis (fun (t : Set X) ↦ t ∈ b ∧ y ∈ t) fun (t : Set X) ↦ t

Tactic:
hb.nhds_hasBasis

Premises used: TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : ∀ s ∈ b, x ∈ s ↔ y ∈ s
h₁ : ∀ (x_1 : Set X), x_1 ∈ b ∧ x ∈ x_1 ↔ x_1 ∈ b ∧ y ∈ x_1
⊢ (𝓝 y).HasBasis (fun (t : Set X) ↦ t ∈ b ∧ x ∈ t) fun (t : Set X) ↦ t

Tactic:
convert! hb.nhds_hasBasis using 2

Premises used: TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : ∀ s ∈ b, x ∈ s ↔ y ∈ s
x_1 : Set X
⊢ x_1 ∈ b ∧ x ∈ x_1 ↔ x_1 ∈ b ∧ y ∈ x_1

Tactic:
and_congr_right (h _)

Premises used: and_congr_right
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : ∀ s ∈ b, x ∈ s ↔ y ∈ s
x_1 : Set X
⊢ x_1 ∈ b ∧ x ∈ x_1 ↔ x_1 ∈ b ∧ y ∈ x_1

Tactic:
exact and_congr_right (h _)

Premises used: and_congr_right
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
⊢ x = y ↔ ∀ s ∈ b, x ∈ s ↔ y ∈ s

Tactic:
inseparable_iff_eq.symm.trans hb.inseparable_iff

Premises used: TopologicalSpace.IsTopologicalBasis.inseparable_iff, inseparable_iff_eq, Iff.trans, Iff.symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u
inst : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun (x y : X) ↦ ∃ (U : Set X), IsOpen[inst] U ∧ Xor (x ∈ U) (y ∈ U)

Tactic:
simp only [t0Space_iff_not_inseparable, xor_iff_not_iff, not_forall, exists_prop,
    inseparable_iff_forall_isOpen, Pairwise]

Premises used: xor_iff_not_iff, inseparable_iff_forall_isOpen, exists_prop, t0Space_iff_not_inseparable, Pairwise, Classical.not_forall
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
x y : X
h : x ≠ y
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ Xor (x ∈ U) (y ∈ U)

Tactic:
(t0Space_iff_exists_isOpen_xor_mem X).1 ‹_› h

Premises used: t0Space_iff_exists_isOpen_xor_mem, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
⊢ T0Space.{u_1} (SeparationQuotient X)

Tactic:
⟨fun x y => Quotient.inductionOn₂' x y fun _ _ h =>
    SeparationQuotient.mk_eq_mk.2 <| SeparationQuotient.isInducing_mk.inseparable_iff.1 h⟩

Premises used: Quotient.inductionOn₂', T0Space.mk
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsClosed[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
⊢ s.Subsingleton

Tactic:
fun x hx y hy => of_not_not fun hxy => ?_

Premises used: Set.Subsingleton, of_not_not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsClosed[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
refine : ∀ (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y), False
⊢ s.Subsingleton

Tactic:
refine fun x hx y hy => of_not_not fun hxy => ?_

Premises used: of_not_not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsClosed[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
rcases : ∀ (U : Set X) (hUo : IsOpen[inst] U) (hU : Xor (x ∈ U) (y ∈ U)), False
⊢ False

Tactic:
rcases exists_isOpen_xor_mem hxy with ⟨U, hUo, hU⟩

Premises used: exists_isOpen_xor_mem
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsClosed[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst] U
hU : Xor (x ∈ U) (y ∈ U)
inr :
  ∀
    (this :
      ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s)
        (hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y)
        (U : Set X) (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False)
    (h : ¬(x ∈ U ∧ y ∉ U)), False
wlog :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s)
    (hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y)
    (U : Set X) (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False
⊢ False

Tactic:
wlog h : x ∈ U ∧ y ∉ U
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsClosed[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst] U
hU : Xor (x ∈ U) (y ∈ U)
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s)
    (hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y)
    (U : Set X) (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False
h : ¬(x ∈ U ∧ y ∉ U)
⊢ False

Tactic:
this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Or.symm
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsClosed[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst] U
hU : Xor (x ∈ U) (y ∈ U)
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s)
    (hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y)
    (U : Set X) (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False
h : ¬(x ∈ U ∧ y ∉ U)
⊢ False

Tactic:
refine this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Or.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 : IsClosed[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[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)
h : x ∈ U ∧ y ∉ U
⊢ x ∈ U

Tactic:
obtain ⟨hxU, hyU⟩ := h
-- 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 : IsClosed[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[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)
h : x ∈ U ∧ y ∉ U
hxU : x ∈ U
⊢ y ∉ U

Tactic:
obtain ⟨hxU, hyU⟩ := h
-- 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 : IsClosed[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[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) diff_subset ⟨y, hy, hyU⟩ (hs.sdiff 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 : IsClosed[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[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:
(this.symm.subset hx).2 hxU

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 : IsClosed[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[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 (this.symm.subset hx).2 hxU

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 : IsClosed[inst] s
hne : s.Nonempty
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst] t → t = s
⊢ ∃ (x : X), s = {x}

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

Premises used: Iff.mpr, Set.exists_eq_singleton_iff_nonempty_subsingleton, And.intro, minimal_nonempty_closed_subsingleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
inst_2 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
obtain :
  ∀ (V : Set X) (Vsub : V ⊆ S) (Vne : V.Nonempty) (Vcls : IsClosed[inst] V)
    (hV : ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V), ∃ x ∈ S, IsClosed[inst] {x}
⊢ ∃ x ∈ S, IsClosed[inst] {x}

Tactic:
obtain ⟨V, Vsub, Vne, Vcls, hV⟩ := hS.exists_minimal_nonempty_closed_subset hne

Premises used: IsClosed.exists_minimal_nonempty_closed_subset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
inst_2 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
V : Set X
Vsub : V ⊆ S
Vne : V.Nonempty
Vcls : IsClosed[inst] V
hV : ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V
rcases :
  ∀ (x : X) (Vsub : {x} ⊆ S) (Vne : Set.Nonempty (α := X) {x}) (Vcls : IsClosed[inst] {x})
    (hV : ∀ V' ⊆ {x}, V'.Nonempty → IsClosed[inst] V' → V' = {x}), ∃ x ∈ S, IsClosed[inst] {x}
⊢ ∃ x ∈ S, IsClosed[inst] {x}

Tactic:
rcases minimal_nonempty_closed_eq_singleton Vcls Vne hV with ⟨x, rfl⟩

Premises used: minimal_nonempty_closed_eq_singleton, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
inst_2 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
x : X
Vsub : {x} ⊆ S
Vne : Set.Nonempty (α := X) {x}
Vcls : IsClosed[inst] {x}
hV : ∀ V' ⊆ {x}, V'.Nonempty → IsClosed[inst] V' → V' = {x}
⊢ ∃ x ∈ S, IsClosed[inst] {x}

Tactic:
⟨x, Vsub (mem_singleton x), Vcls⟩

Premises used: Set.mem_singleton, And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
inst_2 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
x : X
Vsub : {x} ⊆ S
Vne : Set.Nonempty (α := X) {x}
Vcls : IsClosed[inst] {x}
hV : ∀ V' ⊆ {x}, V'.Nonempty → IsClosed[inst] V' → V' = {x}
⊢ ∃ x ∈ S, IsClosed[inst] {x}

Tactic:
exact ⟨x, Vsub (mem_singleton x), Vcls⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsOpen[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
⊢ s.Subsingleton

Tactic:
fun x hx y hy => of_not_not fun hxy => ?_

Premises used: Set.Subsingleton, of_not_not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsOpen[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
refine : ∀ (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y), False
⊢ s.Subsingleton

Tactic:
refine fun x hx y hy => of_not_not fun hxy => ?_

Premises used: of_not_not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsOpen[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
rcases : ∀ (U : Set X) (hUo : IsOpen[inst] U) (hU : Xor (x ∈ U) (y ∈ U)), False
⊢ False

Tactic:
rcases exists_isOpen_xor_mem hxy with ⟨U, hUo, hU⟩

Premises used: exists_isOpen_xor_mem
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsOpen[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst] U
hU : Xor (x ∈ U) (y ∈ U)
inr :
  ∀
    (this :
      ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsOpen s)
        (hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y)
        (U : Set X) (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False)
    (h : ¬(x ∈ U ∧ y ∉ U)), False
wlog :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsOpen s)
    (hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y) (U : Set X)
    (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False
⊢ False

Tactic:
wlog h : x ∈ U ∧ y ∉ U
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsOpen[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst] U
hU : Xor (x ∈ U) (y ∈ U)
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsOpen s)
    (hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y) (U : Set X)
    (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False
h : ¬(x ∈ U ∧ y ∉ U)
⊢ False

Tactic:
this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Or.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
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst] U
hU : Xor (x ∈ U) (y ∈ U)
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsOpen s)
    (hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y) (U : Set X)
    (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False
h : ¬(x ∈ U ∧ y ∉ U)
⊢ False

Tactic:
exact this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Or.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)
h : x ∈ U ∧ y ∉ U
⊢ x ∈ U

Tactic:
obtain ⟨hxU, hyU⟩ := h
-- 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)
h : x ∈ U ∧ y ∉ U
hxU : x ∈ U
⊢ y ∉ U

Tactic:
obtain ⟨hxU, hyU⟩ := h