awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst] s
⊢ IsGδ s

Tactic:
PerfectlyNormalSpace.closed_gdelta hs

Premises used: PerfectlyNormalSpace.closed_gdelta
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
rw : ∀ (s : Set X), IsClosed[inst] s → y ∈ s → x ∈ s
⊢ y ⤳ x

Tactic:
rw [specializes_iff_forall_closed]

Premises used: specializes_iff_forall_closed
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
K : Set X
hK : IsClosed[inst] K
hyK : y ∈ K
⊢ IsGδ K

Tactic:
apply IsClosed.isGδ at hK

Premises used: IsClosed.isGδ
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
K : Set X
hyK : y ∈ K
hK : IsGδ K
obtain : ∀ (Ts : Set (Set X)) (hoTs : ∀ t ∈ Ts, IsOpen[inst] t) (hyK : y ∈ ⋂₀ Ts), x ∈ ⋂₀ Ts
⊢ x ∈ K

Tactic:
obtain ⟨Ts, hoTs, -, rfl⟩ := hK

Premises used: rfl
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
Ts : Set (Set X)
hoTs : ∀ t ∈ Ts, IsOpen[inst] t
hyK : y ∈ ⋂₀ Ts
⊢ ∀ t ∈ Ts, y ∈ t

Tactic:
rw [mem_sInter] at hyK ⊢

Premises used: Set.mem_sInter
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
Ts : Set (Set X)
hoTs : ∀ t ∈ Ts, IsOpen[inst] t
hyK : ∀ t ∈ Ts, y ∈ t
t : Set X
h : t ∈ Ts
⊢ x ∈ t

Tactic:
solve_by_elim [hxy.mem_open]

Premises used: Specializes.mem_open
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x y : X
h : x ≠ y
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
T2Space.t2 h

Premises used: T2Space.t2
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T2Space X ↔ Pairwise fun (x y : X) ↦ Disjoint (𝓝 x) (𝓝 y)

Tactic:
(t2Space_iff X).trans (forall₃_congr fun x y _ => ?_)

Premises used: forall₃_congr, Iff.trans, t2Space_iff
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
refine :
  ∀ (x y : X),
    x ≠ y →
      ((fun (x y : X) ↦ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) x y ↔
        (fun (x y : X) ↦ Disjoint (𝓝 x) (𝓝 y)) x y)
⊢ T2Space X ↔ Pairwise fun (x y : X) ↦ Disjoint (𝓝 x) (𝓝 y)

Tactic:
refine (t2Space_iff X).trans (forall₃_congr fun x y _ => ?_)

Premises used: forall₃_congr, Iff.trans, t2Space_iff
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ≠ y
⊢ (fun (x y : X) ↦ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) x y ↔
    (fun (x y : X) ↦ Disjoint (𝓝 x) (𝓝 y)) x y

Tactic:
simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens y), ← exists_and_left,
    and_assoc, and_comm, and_left_comm]

Premises used: exists_and_left, and_left_comm, and_comm, Filter.HasBasis.disjoint_iff, and_assoc, nhds_basis_opens
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x y : X
hd : Disjoint (𝓝 x) (𝓝 y)
he : x = y
⊢ False

Tactic:
simp [he, nhds_neBot.ne] at hd

Premises used: nhds_neBot, Filter.NeBot.ne
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
⊢ Pairwise.{u_1} (α := X) (Disjoint on 𝓝)

Tactic:
fun _ _ =>
  disjoint_nhds_nhds.2

Premises used: Iff.mpr, Pairwise, disjoint_nhds_nhds
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s : Set X
⊢ s.PairwiseDisjoint 𝓝

Tactic:
pairwise_disjoint_nhds.set_pairwise s

Premises used: Set.PairwiseDisjoint, pairwise_disjoint_nhds, Pairwise.set_pairwise
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
s : Set X
hs : s.Finite
⊢ ∃ (U : X → Set X), (∀ (x : X), x ∈ U x ∧ IsOpen[inst] (U x)) ∧ s.PairwiseDisjoint U

Tactic:
s.pairwiseDisjoint_nhds.exists_mem_filter_basis hs nhds_basis_opens

Premises used: Set.PairwiseDisjoint.exists_mem_filter_basis, Set.pairwiseDisjoint_nhds, nhds_basis_opens
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
⊢ T1Space X

Tactic:
t1Space_iff_disjoint_pure_nhds.mpr fun _ _ hne =>
    (disjoint_nhds_nhds.2 hne).mono_left <| pure_le_nhds _

Premises used: Iff.mpr, pure_le_nhds, Disjoint.mono_left, t1Space_iff_disjoint_pure_nhds, disjoint_nhds_nhds
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
⊢ R1Space X

Tactic:
⟨fun x y ↦ (eq_or_ne x y).imp specializes_of_eq disjoint_nhds_nhds.2⟩

Premises used: Iff.mpr, R1Space.mk, eq_or_ne, Or.imp, disjoint_nhds_nhds, specializes_of_eq
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T2Space.{u_1} (SeparationQuotient X) ↔ R1Space X

Tactic:
simp only [t2Space_iff_disjoint_nhds, Pairwise, surjective_mk.forall₂, ne_eq, mk_eq_mk,
    r1Space_iff_inseparable_or_disjoint_nhds, ← disjoint_comap_iff surjective_mk, comap_mk_nhds_mk,
    ← or_iff_not_imp_left]

Premises used: SeparationQuotient.mk_eq_mk, Filter.disjoint_comap_iff, SeparationQuotient.comap_mk_nhds_mk, r1Space_iff_inseparable_or_disjoint_nhds, ne_eq, t2Space_iff_disjoint_nhds, SeparationQuotient.surjective_mk, Classical.or_iff_not_imp_left, Pairwise, Function.Surjective.forall₂
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
⊢ T2Space.{u_1} (SeparationQuotient X)

Tactic:
t2Space_iff.2 ‹_›

Premises used: Iff.mpr, SeparationQuotient.t2Space_iff
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : T0Space X
⊢ T2Space X

Tactic:
t2Space_iff_disjoint_nhds.2 fun _x _y hne ↦ disjoint_nhds_nhds_iff_not_inseparable.2 fun hxy ↦
    hne hxy.eq

Premises used: Iff.mpr, Inseparable.eq, t2Space_iff_disjoint_nhds, disjoint_nhds_nhds_iff_not_inseparable
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
mp : T2Space X → T0Space X
mpr : T0Space X → T2Space X
⊢ T2Space X ↔ T0Space X

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
h : T2Space X
⊢ T0Space X

Tactic:
infer_instance
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
h : T0Space X
⊢ T2Space X

Tactic:
infer_instance
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T2Space X ↔ ∀ {x y : X}, (𝓝 x ⊓ 𝓝 y).NeBot → x = y

Tactic:
simp only [t2Space_iff_disjoint_nhds, disjoint_iff, neBot_iff, Ne, not_imp_comm, Pairwise]

Premises used: not_imp_comm, disjoint_iff, Filter.neBot_iff, Ne, t2Space_iff_disjoint_nhds, Pairwise
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x y : X
h : (𝓝 x ⊓ 𝓝 y).NeBot
⊢ x = y

Tactic:
t2_iff_nhds.mp ‹_› h

Premises used: Iff.mp, t2_iff_nhds
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T2Space X ↔ Pairwise fun (x y : X) ↦ ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V

Tactic:
simp only [t2Space_iff_disjoint_nhds, Filter.disjoint_iff, Pairwise]

Premises used: Filter.disjoint_iff, t2Space_iff_disjoint_nhds, Pairwise
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x y : X
h : x ≠ y
⊢ ∃ (u : Set X) (v : Set X), u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ Disjoint u v

Tactic:
let ⟨u, v, open_u, open_v, x_in, y_in, huv⟩ := t2_separation h
  ⟨u, v, open_u.mem_nhds x_in, open_v.mem_nhds y_in, huv⟩

Premises used: Disjoint, Membership.mem, Exists, nhds, _private.0.t2_separation_nhds.match_1, And, And.intro, IsOpen.mem_nhds, Exists.intro, t2_separation
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : T2Space X
x y : X
h : x ≠ y
⊢ ∃ (u : Set X) (v : Set X), u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v

Tactic:
simpa only [exists_prop, ← exists_and_left, and_comm, and_assoc, and_left_comm] using
    ((compact_basis_nhds x).disjoint_iff (compact_basis_nhds y)).1 (disjoint_nhds_nhds.2 h)

Premises used: Iff.mpr, exists_and_left, and_left_comm, and_comm, exists_prop, Filter.HasBasis.disjoint_iff, compact_basis_nhds, and_assoc, Iff.mp, disjoint_nhds_nhds
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ (∀ {x y : X}, (𝓝 x ⊓ 𝓝 y).NeBot → x = y) ↔
    ∀ {x y : X} (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓝 x → (↑f : Filter X) ≤ 𝓝 y → x = y

Tactic:
simp only [← exists_ultrafilter_iff, and_imp, le_inf_iff, exists_imp]

Premises used: and_imp, Filter.exists_ultrafilter_iff, le_inf_iff, exists_imp
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T2Space X ↔ IsClosed[instTopologicalSpaceProd] (diagonal X)

Tactic:
simp only [t2Space_iff_disjoint_nhds, ← isOpen_compl_iff, isOpen_iff_mem_nhds, Prod.forall,
    nhds_prod_eq, compl_diagonal_mem_prod, mem_compl_iff, mem_diagonal_iff, Pairwise]

Premises used: Set.mem_diagonal_iff, t2Space_iff_disjoint_nhds, Pairwise, Prod.forall, nhds_prod_eq, isOpen_iff_mem_nhds, Filter.compl_diagonal_mem_prod, isOpen_compl_iff, Set.mem_compl_iff
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)

Tactic:
t2_iff_isClosed_diagonal.mp ‹_›

Premises used: t2_iff_isClosed_diagonal, Iff.mp
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap π
rw : IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}
⊢ T2Space Y ↔ IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}

Tactic:
rw [t2_iff_isClosed_diagonal]

Premises used: t2_iff_isClosed_diagonal
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap π
⊢ IsOpenQuotientMap (Prod.map π π)

Tactic:
replace h := IsOpenQuotientMap.prodMap h h
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}

Tactic:
⟨fun H ↦ H.preimage h.continuous, fun H ↦ ?_⟩

Premises used: IsOpenQuotientMap.continuous, Iff.intro, IsClosed.preimage
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
refine :
  ∀ (H : IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}),
    IsClosed[instTopologicalSpaceProd] (diagonal Y)
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}

Tactic:
refine ⟨fun H ↦ H.preimage h.continuous, fun H ↦ ?_⟩
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
H : IsClosed[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}
simp_rw :
  ∀ (H : IsOpen[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}ᶜ), IsOpen[instTopologicalSpaceProd] (diagonal Y)ᶜ
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y)

Tactic:
simp_rw [← isOpen_compl_iff] at H ⊢

Premises used: isOpen_compl_iff
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
H : IsOpen[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}ᶜ
⊢ IsOpen[instTopologicalSpaceProd] (Prod.map π π '' {q : X × X | π q.1 = π q.2}ᶜ)

Tactic:
h.isOpenMap _ H

Premises used: IsOpenQuotientMap.isOpenMap
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
H : IsOpen[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}ᶜ
h₁ : (diagonal Y)ᶜ = Prod.map π π '' {q : X × X | π q.1 = π q.2}ᶜ
⊢ IsOpen[instTopologicalSpaceProd] (diagonal Y)ᶜ

Tactic:
convert! h.isOpenMap _ H

Premises used: IsOpenQuotientMap.isOpenMap
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
H : IsOpen[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}ᶜ
⊢ (diagonal Y)ᶜ = Prod.map π π '' {q : X × X | π q.1 = π q.2}ᶜ

Tactic:
(h.surjective.image_preimage _).symm

Premises used: Set.Mem, setOf, IsOpenQuotientMap.surjective, Set.diagonal, Set.preimage, Function.Surjective.image_preimage, Eq.symm, Not
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
H : IsOpen[instTopologicalSpaceProd] {q : X × X | π q.1 = π q.2}ᶜ
⊢ (diagonal Y)ᶜ = Prod.map π π '' {q : X × X | π q.1 = π q.2}ᶜ

Tactic:
exact (h.surjective.image_preimage _).symm

Premises used: IsOpenQuotientMap.surjective, Function.Surjective.image_preimage, Eq.symm
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
f : Y → X
l : Filter Y
a b : X
inst_2 : l.NeBot
ha : Tendsto f l (𝓝 a)
hb : Tendsto f l (𝓝 b)
⊢ a = b

Tactic:
(tendsto_nhds_unique_inseparable ha hb).eq

Premises used: Inseparable.eq, tendsto_nhds_unique_inseparable
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
f : Y → X
l : Filter Y
a b : X
h : l.NeBot
ha : Tendsto f l (𝓝 a)
hb : Tendsto f l (𝓝 b)
⊢ a = b

Tactic:
tendsto_nhds_unique ha hb

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
f g : Y → X
l : Filter Y
a b : X
inst_2 : l.NeBot
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
hfg : f =ᶠ[l] g
⊢ a = b

Tactic:
tendsto_nhds_unique (ha.congr' hfg) hb

Premises used: Filter.Tendsto.congr', tendsto_nhds_unique
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
f g : Y → X
l : Filter Y
a b : X
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
hfg : ∃ᶠ (x : Y) in l, f x = g x
⊢ a = b

Tactic:
have : ∃ᶠ z : X × X in 𝓝 (a, b), z.1 = z.2 := (ha.prodMk_nhds hb).frequently hfg
  not_not.1 fun hne => this (isClosed_diagonal.isOpen_compl.mem_nhds hne)

Premises used: IsClosed.isOpen_compl, Classical.not_not, Filter.Tendsto.frequently, IsOpen.mem_nhds, Iff.mp, Filter.Tendsto.prodMk_nhds
-- 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
⊢ 𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t

Tactic:
le_antisymm (nhdsSet_inter_le _ _) ?_

Premises used: le_antisymm, nhdsSet_inter_le
-- 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
refine : 𝓝ˢ s ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)
⊢ 𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t

Tactic:
refine le_antisymm (nhdsSet_inter_le _ _) ?_

Premises used: le_antisymm, nhdsSet_inter_le
-- 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
simp_rw : LE.le.{u_1} (α := Filter X) (⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2) (⨆ a ∈ s ∩ t, 𝓝 a)
⊢ 𝓝ˢ s ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)

Tactic:
simp_rw [hs.nhdsSet_inf_eq_biSup, ht.inf_nhdsSet_eq_biSup, nhdsSet, sSup_image]

Premises used: IsCompact.inf_nhdsSet_eq_biSup, sSup_image, IsCompact.nhdsSet_inf_eq_biSup, nhdsSet
-- 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
⊢ LE.le.{u_1} (α := Filter X) (⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2) (⨆ a ∈ s ∩ t, 𝓝 a)

Tactic:
iSup₂_le fun x hxs ↦ iSup₂_le fun y hyt ↦ ?_

Premises used: iSup₂_le, Set.Mem, setOf
-- 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
refine : ∀ (x : X) (hxs : x ∈ s) (y : X) (hyt : y ∈ t), 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a
⊢ LE.le.{u_1} (α := Filter X) (⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2) (⨆ a ∈ s ∩ t, 𝓝 a)

Tactic:
refine iSup₂_le fun x hxs ↦ iSup₂_le fun y hyt ↦ ?_

Premises used: iSup₂_le
-- 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
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
inl : ∀ (hyt : x ∈ t), 𝓝 x ⊓ 𝓝 x ≤ ⨆ a ∈ s ∩ t, 𝓝 a
inr : ∀ (hne : x ≠ y), 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a

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

Premises used: eq_or_ne, rfl
-- 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
x : X
hxs : x ∈ s
hyt : x ∈ t
⊢ 𝓝 x ⊓ 𝓝 x ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Tactic:
le_iSup₂_of_le x ⟨hxs, hyt⟩ (inf_idem _).le

Premises used: Eq.le, And.intro, le_iSup₂_of_le, inf_idem
-- 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
x : X
hxs : x ∈ s
hyt : x ∈ t
⊢ 𝓝 x ⊓ 𝓝 x ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Tactic:
exact le_iSup₂_of_le x ⟨hxs, hyt⟩ (inf_idem _).le

Premises used: Eq.le, le_iSup₂_of_le, inf_idem
-- 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
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
hne : x ≠ y
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Tactic:
(disjoint_nhds_nhds.mpr hne).eq_bot ▸ bot_le

Premises used: Iff.mpr, Set.Mem, Eq.rec, Eq.symm, bot_le, Disjoint.eq_bot, disjoint_nhds_nhds
-- 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
x : X
hxs : x ∈ s
y : X
hyt : y ∈ t
hne : x ≠ y
⊢ 𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a

Tactic:
exact (disjoint_nhds_nhds.mpr hne).eq_bot ▸ bot_le
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x : X
t : Set X
H1 : IsCompact t
H2 : x ∉ t
⊢ ∃ (U : Set X) (V : Set X), IsOpen[inst] U ∧ IsOpen[inst] V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V

Tactic:
simpa [SeparatedNhds] using SeparatedNhds.of_isCompact_isCompact_isClosed H1 isCompact_singleton
    isClosed_singleton <| disjoint_singleton_right.mpr H2

Premises used: Iff.mpr, Set.disjoint_singleton_right, isCompact_singleton, SeparatedNhds.of_isCompact_isCompact_isClosed, SeparatedNhds, isClosed_singleton
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x : X
t : Set X
H1 : IsCompact t
H2 : x ∉ t
⊢ Disjoint (𝓝ˢ t) (𝓝 x)

Tactic:
simpa using SeparatedNhds.disjoint_nhdsSet <| .of_isCompact_isCompact_isClosed H1
    isCompact_singleton isClosed_singleton <| disjoint_singleton_right.mpr H2

Premises used: Iff.mpr, Set.disjoint_singleton_right, SeparatedNhds.disjoint_nhdsSet
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x y : X
h : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
inl : (x, x) ∈ s ×ˢ s → ∀ (hx : (x, x).1 ∈ s) (hy : (x, x).2 ∈ s), ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2
inr : ∀ (hne : x ≠ y), ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2

Tactic:
rcases eq_or_ne x y with rfl | hne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x : X
h : (x, x) ∈ s ×ˢ s
hx : (x, x).1 ∈ s
hy : (x, x).2 ∈ s
inl : ∀ (u : Set X) (hu : u ∈ 𝓝 x) (hf : InjOn f u), ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2

Tactic:
rcases loc x hx with ⟨u, hu, hf⟩
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x : X
h : (x, x) ∈ s ×ˢ s
hx : (x, x).1 ∈ s
hy : (x, x).2 ∈ s
u : Set X
hu : u ∈ 𝓝 x
hf : InjOn f u
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2

Tactic:
Filter.mem_of_superset (prod_mem_nhds hu hu) <| forall_prod_set.2 hf

Premises used: Iff.mpr, prod_mem_nhds, Filter.Eventually, Set.forall_prod_set, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x : X
h : (x, x) ∈ s ×ˢ s
hx : (x, x).1 ∈ s
hy : (x, x).2 ∈ s
u : Set X
hu : u ∈ 𝓝 x
hf : InjOn f u
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2

Tactic:
exact Filter.mem_of_superset (prod_mem_nhds hu hu) <| forall_prod_set.2 hf

Premises used: prod_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x y : X
h : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
inr : ∀ᶠ (z : X × X) in 𝓝 (x, y), f z.1 ≠ f z.2
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2

Tactic:
suffices ∀ᶠ z in 𝓝 (x, y), f z.1 ≠ f z.2 from this.mono fun _ hne h ↦ absurd h hne
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x y : X
h : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ ∀ᶠ (z : X × X) in 𝓝 (x, y), f z.1 ≠ f z.2

Tactic:
(fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_

Premises used: IsClosed.isOpen_compl, Set.Mem, Filter.Eventually, setOf, ContinuousAt.prodMap', Set.diagonal, Set.preimage, IsOpen.mem_nhds, Not
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x_1 : X × X
x y : X
h : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
inr : Prod.map f f (x, y) ∈ (diagonal Y)ᶜ
⊢ ∀ᶠ (z : X × X) in 𝓝 (x, y), f z.1 ≠ f z.2

Tactic:
refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_

Premises used: IsClosed.isOpen_compl, ContinuousAt.prodMap', IsOpen.mem_nhds