awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
tfae_2_to_3 :
  ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
⊢ ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
tfae_2_to_3 :
  ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
⊢ RegularSpace X

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
tfae_2_to_3 :
  ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
⊢ ∀ (a : ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s), RegularSpace X

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
tfae_2_to_3 :
  ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
⊢ ∀ (a : ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s), RegularSpace X

Tactic:
tfae_have 3 → 1 := fun H => ⟨fun hs ha => (H _ _).mpr <| hs.closure_eq.symm ▸ ha⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
tfae_2_to_3 :
  ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
tfae_3_to_1 : ∀ (a : ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s), RegularSpace X
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s,
      ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x,
      ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
⊢ RegularSpace X

Tactic:
Iff.mpr ((regularSpace_TFAE X).out 0 4) h

Premises used: Iff.mpr, List.TFAE.out, regularSpace_TFAE, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
⊢ RegularSpace X

Tactic:
Iff.mpr ((regularSpace_TFAE X).out 0 5) h

Premises used: Iff.mpr, List.TFAE.out, regularSpace_TFAE, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : X → Sort u_3
p : (a : X) → ι a → Prop
s : (a : X) → ι a → Set X
h₁ : ∀ (a : X), (𝓝 a).HasBasis (p a) (s a)
h₂ : ∀ (a : X) (i : ι a), p a i → IsClosed[inst] (s a i)
⊢ RegularSpace X

Tactic:
.of_lift'_closure fun a => (h₁ a).lift'_closure_eq_self (h₂ a)

Premises used: Filter.HasBasis.lift'_closure_eq_self, RegularSpace.of_lift'_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
⊢ RegularSpace X

Tactic:
Iff.mpr ((regularSpace_TFAE X).out 0 3) h

Premises used: Iff.mpr, List.TFAE.out, regularSpace_TFAE, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
inst_2 : R1Space X
⊢ RegularSpace X

Tactic:
.of_hasBasis isCompact_isClosed_basis_nhds fun _ _ ⟨_, _, h⟩ ↦ h

Premises used: isCompact_isClosed_basis_nhds, RegularSpace.of_hasBasis, IsClosed, _private.0.instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space.match_1
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
⊢ RegularSpace X ↔ ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
⟨fun _ t ht a ha => RegularSpace.regular
    (h ▸ isOpen_generateFrom_of_mem ht).isClosed_compl
    (Set.notMem_compl_iff.mpr ha), fun h' => ⟨fun {t a} ht ha => ?_⟩⟩

Premises used: Iff.mpr, RegularSpace.regular, RegularSpace.mk, Set.notMem_compl_iff, Iff.intro
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
refine :
  ∀ (h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)) {t : Set X} {a : X} (ht : IsClosed[inst] t) (ha : a ∉ t),
    Disjoint (𝓝ˢ t) (𝓝 a)
⊢ RegularSpace X ↔ ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
refine ⟨fun _ t ht a ha => RegularSpace.regular
    (h ▸ isOpen_generateFrom_of_mem ht).isClosed_compl
    (Set.notMem_compl_iff.mpr ha), fun h' => ⟨fun {t a} ht ha => ?_⟩⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
t : Set X
a : X
ht : IsClosed[inst] t
ha : a ∉ t
obtain : ∀ (t : Set X) (ht : IsClosed[inst] tᶜ) (ha : a ∉ tᶜ), Disjoint (𝓝ˢ tᶜ) (𝓝 a)
⊢ Disjoint (𝓝ˢ t) (𝓝 a)

Tactic:
obtain ⟨t, rfl⟩ := compl_involutive.surjective t

Premises used: Function.Involutive.surjective, compl_involutive, rfl
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsClosed[inst] tᶜ
ha : a ∉ tᶜ
⊢ IsOpen[generateFrom s] t

Tactic:
rw [isClosed_compl_iff, h] at ht

Premises used: isClosed_compl_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsClosed[inst] tᶜ
ha : a ∉ tᶜ
ht₁ : IsOpen[generateFrom s] t
⊢ a ∉ tᶜ

Tactic:
rw [isClosed_compl_iff, h] at ht

Premises used: isClosed_compl_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsOpen[generateFrom s] t
ha : a ∉ tᶜ
⊢ a ∈ t

Tactic:
rw [Set.notMem_compl_iff] at ha

Premises used: Set.notMem_compl_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t_1 t : Set X
ht : t ∈ s
ha : a ∈ t
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
h' t ht a ha
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t_1 t : Set X
ht : t ∈ s
ha : a ∈ t
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
exact h' t ht a ha
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ha : Membership.mem (γ := Set X) univ a
⊢ Disjoint (𝓝ˢ univᶜ) (𝓝 a)

Tactic:
simp
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t t₁ t₂ : Set X
h_1 : GenerateOpen s t₁
h_2 : GenerateOpen s t₂
ih₁ : ∀ (ha : a ∈ t₁), Disjoint (𝓝ˢ t₁ᶜ) (𝓝 a)
ih₂ : ∀ (ha : a ∈ t₂), Disjoint (𝓝ˢ t₂ᶜ) (𝓝 a)
ha : a ∈ t₁ ∩ t₂
⊢ Disjoint (𝓝ˢ (t₁ ∩ t₂)ᶜ) (𝓝 a)

Tactic:
grind [compl_inter, nhdsSet_union, disjoint_sup_left]

Premises used: nhdsSet_union, Set.compl_inter, disjoint_sup_left
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
S : Set (Set X)
h_1 : ∀ s_1 ∈ S, GenerateOpen s s_1
ih : ∀ s ∈ S, ∀ (ha : a ∈ s), Disjoint (𝓝ˢ sᶜ) (𝓝 a)
ha : a ∈ ⋃₀ S
sUnion : ∀ (t : Set X) (ht : t ∈ S) (ha : a ∈ t), Disjoint (𝓝ˢ (⋃₀ S)ᶜ) (𝓝 a)
⊢ Disjoint (𝓝ˢ (⋃₀ S)ᶜ) (𝓝 a)

Tactic:
obtain ⟨t, ht, ha⟩ := ha
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t_1 : Set X
S : Set (Set X)
h_1 : ∀ s_1 ∈ S, GenerateOpen s s_1
ih : ∀ s ∈ S, ∀ (ha : a ∈ s), Disjoint (𝓝ˢ sᶜ) (𝓝 a)
t : Set X
ht : t ∈ S
ha : a ∈ t
sUnion : Disjoint (𝓝ˢ tᶜ) (𝓝 a)
⊢ Disjoint (𝓝ˢ (⋃₀ S)ᶜ) (𝓝 a)

Tactic:
grw [compl_sUnion, sInter_image, iInter₂_subset t ht]

Premises used: Set.iInter₂_subset, Set.compl_sUnion, Set.sInter_image
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t_1 : Set X
S : Set (Set X)
h_1 : ∀ s_1 ∈ S, GenerateOpen s s_1
ih : ∀ s ∈ S, ∀ (ha : a ∈ s), Disjoint (𝓝ˢ sᶜ) (𝓝 a)
t : Set X
ht : t ∈ S
ha : a ∈ t
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
ih t ht ha
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t_1 : Set X
S : Set (Set X)
h_1 : ∀ s_1 ∈ S, GenerateOpen s s_1
ih : ∀ s ∈ S, ∀ (ha : a ∈ s), Disjoint (𝓝ˢ sᶜ) (𝓝 a)
t : Set X
ht : t ∈ S
ha : a ∈ t
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
exact ih t ht ha
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (Set X)
h : inst = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ht : IsOpen[generateFrom s] t
ha : a ∈ t
basic : ∀ (t : Set X) (ht : t ∈ s) (ha : a ∈ t), Disjoint (𝓝ˢ tᶜ) (𝓝 a)
univ : ∀ (ha : Membership.mem (γ := Set X) Set.univ a), Disjoint (𝓝ˢ Set.univᶜ) (𝓝 a)
inter :
  ∀ (t₁ t₂ : Set X),
    GenerateOpen s t₁ →
      GenerateOpen s t₂ →
        ∀ (ih₁ : ∀ (ha : a ∈ t₁), Disjoint (𝓝ˢ t₁ᶜ) (𝓝 a)) (ih₂ : ∀ (ha : a ∈ t₂), Disjoint (𝓝ˢ t₂ᶜ) (𝓝 a))
          (ha : a ∈ t₁ ∩ t₂), Disjoint (𝓝ˢ (t₁ ∩ t₂)ᶜ) (𝓝 a)
sUnion :
  ∀ (S : Set (Set X)),
    (∀ s_1 ∈ S, GenerateOpen s s_1) →
      ∀ (ih : ∀ s ∈ S, ∀ (ha : a ∈ s), Disjoint (𝓝ˢ sᶜ) (𝓝 a)) (ha : a ∈ ⋃₀ S), Disjoint (𝓝ˢ (⋃₀ S)ᶜ) (𝓝 a)
⊢ Disjoint (𝓝ˢ tᶜ) (𝓝 a)

Tactic:
induction ht with
  | basic t ht => exact h' t ht a ha
  | univ => simp
  | inter t₁ t₂ _ _ ih₁ ih₂ => grind [compl_inter, nhdsSet_union, disjoint_sup_left]
  | sUnion S _ ih =>
    obtain ⟨t, ht, ha⟩ := ha
    grw [compl_sUnion, sInter_image, iInter₂_subset t ht]
    exact ih t ht ha

Premises used: nhdsSet_union, Set.univ, Set.iInter₂_subset, Set.sUnion, Set.compl_inter, Set.compl_sUnion, Set.sInter_image, disjoint_sup_left
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
⊢ RegularSpace X ↔ ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s

Tactic:
have h := (regularSpace_TFAE X).out 0 2
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
h : RegularSpace X ↔ ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
⊢ Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s

Tactic:
h.mp ‹_› _ _

Premises used: Iff.mp
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
h : RegularSpace X ↔ ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
⊢ Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s

Tactic:
exact h.mp ‹_› _ _

Premises used: Iff.mp
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
⊢ Disjoint (𝓝 x) (𝓝ˢ s) ↔ x ∉ closure[inst] s

Tactic:
disjoint_comm.trans disjoint_nhdsSet_nhds

Premises used: disjoint_comm, Iff.trans, disjoint_nhdsSet_nhds
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
x_1 x_2 : X
h : ¬x_1 ⤳ x_2
rwa : Disjoint (𝓝ˢ {x_1}) (𝓝 x_2)
rwa₁ : x_2 ∉ closure[inst] {x_1}
rwa₂ rwa₃ rwa₄ rwa₅ : ¬x_1 ⤳ x_2
⊢ Disjoint (𝓝 x_1) (𝓝 x_2)

Tactic:
rwa [← nhdsSet_singleton, disjoint_nhdsSet_nhds, ← specializes_iff_mem_closure]

Premises used: specializes_iff_mem_closure, nhdsSet_singleton, disjoint_nhdsSet_nhds
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
h : s ∈ 𝓝 x
⊢ RegularSpace X ↔ ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s

Tactic:
have h' := (regularSpace_TFAE X).out 0 3
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
h : s ∈ 𝓝 x
h' : RegularSpace X ↔ ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
⊢ ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s

Tactic:
h'.mp ‹_› _ _ h

Premises used: Iff.mp
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
s : Set X
h : s ∈ 𝓝 x
h' : RegularSpace X ↔ ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
⊢ ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s

Tactic:
exact h'.mp ‹_› _ _ h

Premises used: Iff.mp
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x ∧ IsClosed[inst] s) id

Tactic:
hasBasis_self.2 fun _ => exists_mem_nhds_isClosed_subset

Premises used: Iff.mpr, Filter.hasBasis_self, exists_mem_nhds_isClosed_subset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
⊢ (𝓝 x).lift' closure[inst] = 𝓝 x

Tactic:
(closed_nhds_basis x).lift'_closure_eq_self fun _ => And.right

Premises used: Filter.HasBasis.lift'_closure_eq_self, closed_nhds_basis, And.right
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
ι : Sort u_3
x : X
p : ι → Prop
s : ι → Set X
h : (𝓝 x).HasBasis p s
⊢ (𝓝 x).HasBasis p fun (i : ι) ↦ closure[inst] (s i)

Tactic:
lift'_nhds_closure x ▸ h.lift'_closure

Premises used: Eq.rec, lift'_nhds_closure, Filter.HasBasis.lift'_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x) closure[inst]

Tactic:
(𝓝 x).basis_sets.nhds_closure

Premises used: nhds, Filter.basis_sets, Filter.HasBasis.nhds_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ x ∈ s ∧ IsOpen[inst] s) closure[inst]

Tactic:
(nhds_basis_opens x).nhds_closure

Premises used: nhds_basis_opens, Filter.HasBasis.nhds_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
⊢ Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)

Tactic:
simpa [hK.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
      ← subset_interior_iff_mem_nhdsSet] using hU

Premises used: IsCompact.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet, subset_interior_iff_mem_nhdsSet
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
⊢ Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)

Tactic:
have hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ) := by
    simpa [hK.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
      ← subset_interior_iff_mem_nhdsSet] using hU
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
rcases :
  ∀ (V : Set X) (hVo : IsOpen[inst] V) (hKV : K ⊆ V) (W : Set X) (hVW : Disjoint V W) (hW : IsOpen[inst] W)
    (hUW : Uᶜ ⊆ W), ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U

Tactic:
rcases ((hasBasis_nhdsSet _).disjoint_iff (hasBasis_nhdsSet _)).1 hd
    with ⟨V, ⟨hVo, hKV⟩, W, ⟨hW, hUW⟩, hVW⟩

Premises used: hasBasis_nhdsSet, Filter.HasBasis.disjoint_iff, Iff.mp
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
V : Set X
hVo : IsOpen[inst] V
hKV : K ⊆ V
W : Set X
hVW : Disjoint V W
hW : IsOpen[inst] W
hUW : Uᶜ ⊆ W
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U

Tactic:
⟨V, hVo, hKV, Subset.trans ?_ (compl_subset_comm.1 hUW)⟩

Premises used: Set.Subset.trans, Set.compl_subset_comm, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
V : Set X
hVo : IsOpen[inst] V
hKV : K ⊆ V
W : Set X
hVW : Disjoint V W
hW : IsOpen[inst] W
hUW : Uᶜ ⊆ W
refine : closure[inst] V ⊆ Wᶜ
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U

Tactic:
refine ⟨V, hVo, hKV, Subset.trans ?_ (compl_subset_comm.1 hUW)⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
V : Set X
hVo : IsOpen[inst] V
hKV : K ⊆ V
W : Set X
hVW : Disjoint V W
hW : IsOpen[inst] W
hUW : Uᶜ ⊆ W
⊢ closure[inst] V ⊆ Wᶜ

Tactic:
closure_minimal hVW.subset_compl_right hW.isClosed_compl

Premises used: Disjoint.subset_compl_right, closure_minimal, IsOpen.isClosed_compl
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : U ∈ 𝓝ˢ K
hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)
V : Set X
hVo : IsOpen[inst] V
hKV : K ⊆ V
W : Set X
hVW : Disjoint V W
hW : IsOpen[inst] W
hUW : Uᶜ ⊆ W
⊢ closure[inst] V ⊆ Wᶜ

Tactic:
exact closure_minimal hVW.subset_compl_right hW.isClosed_compl

Premises used: Disjoint.subset_compl_right, closure_minimal, IsOpen.isClosed_compl
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).lift' closure[inst] = 𝓝ˢ K

Tactic:
le_antisymm (fun U hU ↦ ?_) (le_lift'_closure _)

Premises used: le_antisymm, Filter.le_lift'_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K : Set X
hK : IsCompact K
refine : ∀ (U : Set X) (hU : U ∈ 𝓝ˢ K), U ∈ (𝓝ˢ K).lift' closure[inst]
⊢ (𝓝ˢ K).lift' closure[inst] = 𝓝ˢ K

Tactic:
refine le_antisymm (fun U hU ↦ ?_) (le_lift'_closure _)

Premises used: le_antisymm, Filter.le_lift'_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
rcases : ∀ (V : Set X) (hVo : IsOpen[inst] V) (hKV : K ⊆ V) (hVU : closure[inst] V ⊆ U), U ∈ (𝓝ˢ K).lift' closure[inst]
⊢ U ∈ (𝓝ˢ K).lift' closure[inst]

Tactic:
rcases hK.exists_isOpen_closure_subset hU with ⟨V, hVo, hKV, hVU⟩

Premises used: IsCompact.exists_isOpen_closure_subset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
V : Set X
hVo : IsOpen[inst] V
hKV : K ⊆ V
hVU : closure[inst] V ⊆ U
⊢ U ∈ (𝓝ˢ K).lift' closure[inst]

Tactic:
mem_of_superset (mem_lift' <| hVo.mem_nhdsSet.2 hKV) hVU

Premises used: Iff.mpr, Filter.mem_lift', IsOpen.mem_nhdsSet, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : U ∈ 𝓝ˢ K
V : Set X
hVo : IsOpen[inst] V
hKV : K ⊆ V
hVU : closure[inst] V ⊆ U
⊢ U ∈ (𝓝ˢ K).lift' closure[inst]

Tactic:
exact mem_of_superset (mem_lift' <| hVo.mem_nhdsSet.2 hKV) hVU

Premises used: Iff.mpr, Filter.mem_lift', IsOpen.mem_nhdsSet, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
B : Set (Set X)
hB : IsTopologicalBasis B
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ x ∈ s ∧ s ∈ B) closure[inst]

Tactic:
simpa only [and_comm] using hB.nhds_hasBasis.nhds_closure

Premises used: and_comm, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis, Filter.HasBasis.nhds_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
B : Set (Set X)
hB : IsTopologicalBasis B
x : X
s : Set X
h : s ∈ 𝓝 x
⊢ ∃ t ∈ B, x ∈ t ∧ closure[inst] t ⊆ s

Tactic:
simpa only [exists_prop, and_assoc] using hB.nhds_hasBasis.nhds_closure.mem_iff.mp h

Premises used: Filter.HasBasis.mem_iff, exists_prop, and_assoc, Iff.mp, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis, Filter.HasBasis.nhds_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
rw : (comap f (𝓝 (f b))).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 (f b) ∧ IsClosed[inst] s) fun (i : Set X) ↦ f ⁻¹' id i
⊢ (𝓝 b).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 (f b) ∧ IsClosed[inst] s) fun (i : Set X) ↦ f ⁻¹' id i

Tactic:
rw [hf.nhds_eq_comap b]

Premises used: Topology.IsInducing.nhds_eq_comap
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (comap f (𝓝 (f b))).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 (f b) ∧ IsClosed[inst] s) fun (i : Set X) ↦ f ⁻¹' id i

Tactic:
(closed_nhds_basis _).comap _

Premises used: closed_nhds_basis, Filter.HasBasis.comap