awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
u : (a : X) → Set X
u_open : ∀ (a : X), IsOpen[inst] (u a)
u_dis : ∀ (a : X), Disjoint (closure[inst] (u a)) t
u_nhds : ∀ a ∈ s, a ∈ u a
inr : ∀ (f : ℕ → X) (f_cov : s ⊆ ⋃ (n : ℕ), u (f n)), _root_.HasSeparatingCover s t
⊢ _root_.HasSeparatingCover s t

Tactic:
obtain ⟨f, f_cov⟩ := s_cl.isLindelof.indexed_countable_subcover
    u u_open (fun a ainh ↦ mem_iUnion.mpr ⟨a, u_nhds a ainh⟩)

Premises used: Iff.mpr, Set.mem_iUnion, IsClosed.isLindelof, IsLindelof.indexed_countable_subcover, Exists.intro
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
u : (a : X) → Set X
u_open : ∀ (a : X), IsOpen[inst] (u a)
u_dis : ∀ (a : X), Disjoint (closure[inst] (u a)) t
u_nhds : ∀ a ∈ s, a ∈ u a
f : ℕ → X
f_cov : s ⊆ ⋃ (n : ℕ), u (f n)
⊢ _root_.HasSeparatingCover s t

Tactic:
⟨u ∘ f, f_cov, fun n ↦ ⟨u_open (f n), u_dis (f n)⟩⟩

Premises used: Function.comp, HasSeparatingCover, And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : LindelofSpace X
inst_2 : RegularSpace X
s_cl : IsClosed[inst] s
t_cl : IsClosed[inst] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
u : (a : X) → Set X
u_open : ∀ (a : X), IsOpen[inst] (u a)
u_dis : ∀ (a : X), Disjoint (closure[inst] (u a)) t
u_nhds : ∀ a ∈ s, a ∈ u a
f : ℕ → X
f_cov : s ⊆ ⋃ (n : ℕ), u (f n)
⊢ _root_.HasSeparatingCover s t

Tactic:
exact ⟨u ∘ f, f_cov, fun n ↦ ⟨u_open (f n), u_dis (f n)⟩⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x y : X
h : ¬Inseparable x y
rcases :
  ∀ (U₁ U₂ : Set X) (U₁_op : IsOpen[inst] U₁) (U₂_op : IsOpen[inst] U₂) (x_in : x ∈ U₁) (y_in : y ∈ U₂)
    (H : Disjoint U₁ U₂),
    ∃ U₁ ∈ 𝓝 x,
      ∃ V₁ ∈ 𝓝 x,
        ∃ U₂ ∈ 𝓝 y,
          ∃ V₂ ∈ 𝓝 y,
            IsClosed[inst] V₁ ∧
              IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
rcases r1_separation h with ⟨U₁, U₂, U₁_op, U₂_op, x_in, y_in, H⟩

Premises used: r1_separation
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x y : X
h : ¬Inseparable x y
U₁ U₂ : Set X
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
rcases :
  ∀ (V₁ : Set X) (V₁_in : V₁ ∈ 𝓝 x) (V₁_closed : IsClosed[inst] V₁) (h₁ : V₁ ⊆ U₁),
    ∃ U₁ ∈ 𝓝 x,
      ∃ V₁ ∈ 𝓝 x,
        ∃ U₂ ∈ 𝓝 y,
          ∃ V₂ ∈ 𝓝 y,
            IsClosed[inst] V₁ ∧
              IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
rcases exists_mem_nhds_isClosed_subset (U₁_op.mem_nhds x_in) with ⟨V₁, V₁_in, V₁_closed, h₁⟩

Premises used: IsOpen.mem_nhds, exists_mem_nhds_isClosed_subset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x y : X
h : ¬Inseparable x y
U₁ U₂ : Set X
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set X
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed[inst] V₁
h₁ : V₁ ⊆ U₁
rcases :
  ∀ (V₂ : Set X) (V₂_in : V₂ ∈ 𝓝 y) (V₂_closed : IsClosed[inst] V₂) (h₂ : V₂ ⊆ U₂),
    ∃ U₁ ∈ 𝓝 x,
      ∃ V₁ ∈ 𝓝 x,
        ∃ U₂ ∈ 𝓝 y,
          ∃ V₂ ∈ 𝓝 y,
            IsClosed[inst] V₁ ∧
              IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
rcases exists_mem_nhds_isClosed_subset (U₂_op.mem_nhds y_in) with ⟨V₂, V₂_in, V₂_closed, h₂⟩

Premises used: IsOpen.mem_nhds, exists_mem_nhds_isClosed_subset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x y : X
h : ¬Inseparable x y
U₁ U₂ : Set X
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set X
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed[inst] V₁
h₁ : V₁ ⊆ U₁
V₂ : Set X
V₂_in : V₂ ∈ 𝓝 y
V₂_closed : IsClosed[inst] V₂
h₂ : V₂ ⊆ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
⟨U₁, mem_of_superset V₁_in h₁, V₁, V₁_in, U₂, mem_of_superset V₂_in h₂, V₂, V₂_in,
    V₁_closed, V₂_closed, U₁_op, U₂_op, h₁, h₂, H⟩

Premises used: And.intro, Exists.intro, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x y : X
h : ¬Inseparable x y
U₁ U₂ : Set X
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set X
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed[inst] V₁
h₁ : V₁ ⊆ U₁
V₂ : Set X
V₂_in : V₂ ∈ 𝓝 y
V₂_closed : IsClosed[inst] V₂
h₂ : V₂ ⊆ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
exact ⟨U₁, mem_of_superset V₁_in h₁, V₁, V₁_in, U₂, mem_of_superset V₂_in h₂, V₂, V₂_in,
    V₁_closed, V₂_closed, U₁_op, U₂_op, h₁, h₂, H⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
h_KU : K ⊆ U
⊢ ∃ (L : Set X), IsCompact L ∧ IsClosed[inst] L ∧ K ⊆ interior L ∧ L ⊆ U

Tactic:
let ⟨L, L_comp, KL, LU⟩ := exists_compact_between hK hU h_KU
  ⟨closure L, L_comp.closure, isClosed_closure, KL.trans <| interior_mono subset_closure,
    L_comp.closure_subset_of_isOpen hU LU⟩

Premises used: exists_compact_between, _private.0.exists_compact_closed_between.match_1, interior_mono, subset_closure, Exists, IsCompact.closure, HasSubset.Subset.trans, HasSubset.Subset, IsClosed, And, closure, IsCompact.closure_subset_of_isOpen, And.intro, interior, Exists.intro, isClosed_closure, IsCompact
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K : Set X
hK : IsCompact K
⊢ ∀ ⦃s t : Set X⦄,
    s ⊆ t →
      (∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ s) → ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ t

Tactic:
grind
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K : Set X
hK : IsCompact K
rw : ∀ (i : Set X), IsOpen[inst] i ∧ K ⊆ i → ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ i
⊢ (𝓝ˢ K).HasBasis (fun (L : Set X) ↦ L ∈ 𝓝ˢ K ∧ IsCompact L ∧ IsClosed[inst] L) id

Tactic:
rw [hasBasis_self, (hasBasis_nhdsSet _).forall_iff (by grind)]

Premises used: hasBasis_nhdsSet, Filter.hasBasis_self, Filter.HasBasis.forall_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
this : ∀ (hU : IsOpen[inst] U) (h_KU : K ⊆ U), ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ U
⊢ IsOpen[inst] U ∧ K ⊆ U → ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ U

Tactic:
⟨hU, h_KU⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
h_KU : K ⊆ U
obtain :
  ∀ (L : Set X) (hL : IsCompact L) (hL' : IsClosed[inst] L) (hKL : K ⊆ interior L) (hLU : L ⊆ U),
    ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ U

Tactic:
obtain ⟨L, hL, hL', hKL, hLU⟩ := exists_compact_closed_between hK hU h_KU

Premises used: exists_compact_closed_between
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hL' : IsClosed[inst] L
hKL : K ⊆ interior L
hLU : L ⊆ U
rwa rwa₁ rwa₂ rwa₃ : K ⊆ interior L
⊢ L ∈ 𝓝ˢ K

Tactic:
rwa [← subset_interior_iff_mem_nhdsSet]

Premises used: subset_interior_iff_mem_nhdsSet
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hL' : IsClosed[inst] L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ U

Tactic:
exact ⟨L, by rwa [← subset_interior_iff_mem_nhdsSet], ⟨hL, hL'⟩, hLU⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
rcases :
  ∀ (L : Set X) (L_compact : IsCompact L) (L_closed : IsClosed[inst] L) (KL : K ⊆ interior L) (LU : L ⊆ U),
    ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U ∧ IsCompact (closure[inst] V)
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U ∧ IsCompact (closure[inst] V)

Tactic:
rcases exists_compact_closed_between hK hU hKU with ⟨L, L_compact, L_closed, KL, LU⟩

Premises used: exists_compact_closed_between
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed[inst] L
KL : K ⊆ interior L
LU : L ⊆ U
⊢ closure[inst] (interior L) ⊆ L

Tactic:
apply (closure_mono interior_subset).trans (le_of_eq L_closed.closure_eq)

Premises used: interior_subset, IsClosed.closure_eq, HasSubset.Subset.trans, closure_mono, le_of_eq
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed[inst] L
KL : K ⊆ interior L
LU : L ⊆ U
⊢ closure[inst] (interior L) ⊆ L

Tactic:
have A : closure (interior L) ⊆ L := by
    apply (closure_mono interior_subset).trans (le_of_eq L_closed.closure_eq)
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed[inst] L
KL : K ⊆ interior L
LU : L ⊆ U
A : closure[inst] (interior L) ⊆ L
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U ∧ IsCompact (closure[inst] V)

Tactic:
⟨interior L, isOpen_interior, KL, A.trans LU, ?_⟩

Premises used: isOpen_interior, HasSubset.Subset.trans, And.intro, interior, Exists.intro
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed[inst] L
KL : K ⊆ interior L
LU : L ⊆ U
A : closure[inst] (interior L) ⊆ L
refine : IsCompact (closure[inst] (interior L))
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U ∧ IsCompact (closure[inst] V)

Tactic:
refine ⟨interior L, isOpen_interior, KL, A.trans LU, ?_⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed[inst] L
KL : K ⊆ interior L
LU : L ⊆ U
A : closure[inst] (interior L) ⊆ L
⊢ IsCompact (closure[inst] (interior L))

Tactic:
L_compact.closure_of_subset interior_subset

Premises used: interior_subset, IsCompact.closure_of_subset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed[inst] L
KL : K ⊆ interior L
LU : L ⊆ U
A : closure[inst] (interior L) ⊆ L
⊢ IsCompact (closure[inst] (interior L))

Tactic:
exact L_compact.closure_of_subset interior_subset

Premises used: interior_subset, IsCompact.closure_of_subset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
a : closure[inst] s ⊆ nhdsKer s
a₁ : nhdsKer s ⊆ closure[inst] s
⊢ closure[inst] s = nhdsKer s

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
a : closure[inst] s ⊆ ((𝓝ˢ s).lift' closure[inst]).ker
⊢ closure[inst] s ⊆ nhdsKer s

Tactic:
rw [nhdsKer, ← hs.lift'_closure_nhdsSet]

Premises used: nhdsKer, IsCompact.lift'_closure_nhdsSet
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
⊢ closure[inst] s ⊆ ((𝓝ˢ s).lift' closure[inst]).ker

Tactic:
simp +contextual [Filter.lift', Filter.lift, closure_mono, subset_of_mem_nhdsSet]

Premises used: subset_of_mem_nhdsSet, closure_mono, Filter.lift', Filter.lift
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
a : ∀ (hy' : y ∉ closure[inst] s), False
⊢ y ∈ closure[inst] s

Tactic:
by_contra! hy'
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
hy' : y ∉ closure[inst] s
⊢ ∃ s_1 ∈ 𝓝ˢ s, ∃ t ∈ 𝓝 y, Disjoint s_1 t

Tactic:
rw [← _root_.disjoint_nhdsSet_nhds, Filter.disjoint_iff] at hy'

Premises used: Filter.disjoint_iff, disjoint_nhdsSet_nhds
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
hy' : ∃ s_1 ∈ 𝓝ˢ s, ∃ t ∈ 𝓝 y, Disjoint s_1 t
a : ∀ (t : Set X) (hts : t ∈ 𝓝ˢ s) (t' : Set X) (ht'y : t' ∈ 𝓝 y) (H : Disjoint t t'), False
⊢ False

Tactic:
obtain ⟨t, hts, t', ht'y, H⟩ := hy'
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
t : Set X
hts : t ∈ 𝓝ˢ s
t' : Set X
ht'y : t' ∈ 𝓝 y
H : Disjoint t t'
⊢ False

Tactic:
Set.disjoint_iff.mp H ⟨hy t hts, mem_of_mem_nhds ht'y⟩

Premises used: Set.Mem, mem_of_mem_nhds, And.intro, Iff.mp, Set.disjoint_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
t : Set X
hts : t ∈ 𝓝ˢ s
t' : Set X
ht'y : t' ∈ 𝓝 y
H : Disjoint t t'
⊢ False

Tactic:
exact Set.disjoint_iff.mp H ⟨hy t hts, mem_of_mem_nhds ht'y⟩

Premises used: mem_of_mem_nhds, And.intro, Iff.mp, Set.disjoint_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T25Space X
x y : X
h : Disjoint ((𝓝 x).lift' closure[inst]) ((𝓝 y).lift' closure[inst])
hxy : x = y
⊢ False

Tactic:
simp [hxy, nhds_neBot.ne] at h

Premises used: nhds_neBot, Filter.NeBot.ne
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T25Space X
⊢ T2Space X

Tactic:
t2Space_iff_disjoint_nhds.2 fun _ _ hne =>
    (disjoint_lift'_closure_nhds.2 hne).mono (le_lift'_closure _) (le_lift'_closure _)

Premises used: Iff.mpr, nhds, t2Space_iff_disjoint_nhds, Filter.le_lift'_closure, disjoint_lift'_closure_nhds, Disjoint.mono
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T25Space X
x y : X
h : x ≠ y
⊢ ∃ s ∈ 𝓝 x, ∃ t ∈ 𝓝 y, Disjoint (closure[inst] s) (closure[inst] t)

Tactic:
((𝓝 x).basis_sets.lift'_closure.disjoint_iff (𝓝 y).basis_sets.lift'_closure).1 <|
    disjoint_lift'_closure_nhds.2 h

Premises used: Iff.mpr, nhds, Filter.HasBasis.disjoint_iff, Filter.basis_sets, Iff.mp, disjoint_lift'_closure_nhds, Filter.HasBasis.lift'_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T25Space X
x y : X
h : x ≠ y
⊢ ∃ (u : Set X),
    x ∈ u ∧ IsOpen[inst] u ∧ ∃ (v : Set X), y ∈ v ∧ IsOpen[inst] v ∧ Disjoint (closure[inst] u) (closure[inst] v)

Tactic:
simpa only [exists_prop, and_assoc] using
    ((nhds_basis_opens x).lift'_closure.disjoint_iff (nhds_basis_opens y).lift'_closure).1
      (disjoint_lift'_closure_nhds.2 h)

Premises used: Iff.mpr, exists_prop, Filter.HasBasis.disjoint_iff, and_assoc, Iff.mp, disjoint_lift'_closure_nhds, nhds_basis_opens, Filter.HasBasis.lift'_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T25Space Y
f : X → Y
hf : IsEmbedding f
⊢ T25Space X

Tactic:
.of_injective_continuous hf.injective hf.continuous

Premises used: Topology.IsEmbedding.injective, T25Space.of_injective_continuous, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T25Space X
h : X ≃ₜ Y
⊢ T25Space Y

Tactic:
h.symm.isEmbedding.t25Space

Premises used: Topology.IsEmbedding.t25Space, Homeomorph.isEmbedding, Homeomorph.symm
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T25Space X
p : X → Prop
⊢ T25Space.{u_1} { x : X // p x }

Tactic:
IsEmbedding.subtypeVal.t25Space

Premises used: Topology.IsEmbedding.t25Space, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T0Space X
inst_2 : RegularSpace X
⊢ T3Space X

Tactic:
⟨⟩

Premises used: T3Space.mk
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
mp : T3Space X → T0Space X
mpr : T0Space X → T3Space X
⊢ T3Space X ↔ T0Space X

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
h : T3Space X
⊢ T0Space X

Tactic:
infer_instance
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
h : T0Space X
⊢ T3Space X

Tactic:
infer_instance
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
⊢ T25Space X

Tactic:
⟨fun x y hne => ?_⟩

Premises used: T25Space.mk
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
refine : ∀ (x y : X) (hne : x ≠ y), Disjoint ((𝓝 x).lift' closure[inst]) ((𝓝 y).lift' closure[inst])
⊢ T25Space X

Tactic:
refine ⟨fun x y hne => ?_⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
x y : X
hne : x ≠ y
rw : Disjoint (𝓝 x) (𝓝 y)
⊢ Disjoint ((𝓝 x).lift' closure[inst]) ((𝓝 y).lift' closure[inst])

Tactic:
rw [lift'_nhds_closure, lift'_nhds_closure]

Premises used: lift'_nhds_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
x y : X
hne : x ≠ y
⊢ x ∉ closure[inst] {y} ∨ y ∉ closure[inst] {x}

Tactic:
have : x ∉ closure {y} ∨ y ∉ closure {x} :=
    (t0Space_iff_or_notMem_closure X).mp inferInstance hne
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
x y : X
hne : x ≠ y
this : x ∉ closure[inst] {y} ∨ y ∉ closure[inst] {x}
⊢ Disjoint (𝓝 x) (𝓝 y) ∨ Disjoint (𝓝 y) (𝓝 x)

Tactic:
simp only [← disjoint_nhds_nhdsSet, nhdsSet_singleton] at this

Premises used: disjoint_nhds_nhdsSet, nhdsSet_singleton
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
x y : X
hne : x ≠ y
this : Disjoint (𝓝 x) (𝓝 y) ∨ Disjoint (𝓝 y) (𝓝 x)
⊢ Disjoint (𝓝 x) (𝓝 y)

Tactic:
this.elim id fun h => h.symm

Premises used: id, Disjoint.symm, Or.elim
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
x y : X
hne : x ≠ y
this : Disjoint (𝓝 x) (𝓝 y) ∨ Disjoint (𝓝 y) (𝓝 x)
⊢ Disjoint (𝓝 x) (𝓝 y)

Tactic:
exact this.elim id fun h => h.symm

Premises used: id, Disjoint.symm, Or.elim
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T3Space Y
f : X → Y
hf : IsEmbedding f
⊢ T3Space X

Tactic:
{ toT0Space := hf.t0Space
    toRegularSpace := hf.isInducing.regularSpace }

Premises used: Topology.IsEmbedding.t0Space, Topology.IsEmbedding.isInducing, T3Space.mk, Topology.IsInducing.regularSpace
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T3Space X
h : X ≃ₜ Y
⊢ T3Space Y

Tactic:
h.symm.isEmbedding.t3Space

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.t3Space, Homeomorph.symm
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
p : X → Prop
⊢ T3Space.{u_1} (Subtype p)

Tactic:
IsEmbedding.subtypeVal.t3Space

Premises used: Topology.IsEmbedding.t3Space, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
⊢ T3Space (ULift.{u_3, u_1} X)

Tactic:
IsEmbedding.uliftDown.t3Space

Premises used: Topology.IsEmbedding.uliftDown, Topology.IsEmbedding.t3Space
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T3Space X
inst_3 : T3Space Y
⊢ T3Space (X × Y)

Tactic:
⟨⟩

Premises used: T3Space.mk
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_3
X : ι → Type u_4
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), T3Space.{u_4} (X i)
⊢ T3Space ((i : ι) → X i)

Tactic:
⟨⟩

Premises used: T3Space.mk
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T3Space X
x y : X
h : x ≠ y
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂

Tactic:
disjoint_nested_nhds_of_not_inseparable (mt Inseparable.eq h)

Premises used: disjoint_nested_nhds_of_not_inseparable, mt, Inseparable.eq
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set (SeparationQuotient X)
a : SeparationQuotient X
hs : IsClosed s
ha : a ∉ s
rcases : ∀ (a : X) (ha : SeparationQuotient.mk a ∉ s), Disjoint (𝓝ˢ s) (𝓝 (SeparationQuotient.mk a))
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
rcases surjective_mk a with ⟨a, rfl⟩

Premises used: SeparationQuotient.surjective_mk, rfl