awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (closed_nhds_basis _).comap _

Premises used: closed_nhds_basis, Filter.HasBasis.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
s : Set X
hs : s ∈ 𝓝 (f b) ∧ IsClosed[inst] s
⊢ IsClosed[inst_2] (f ⁻¹' id s)

Tactic:
hs.2.preimage hf.continuous

Premises used: And.right, IsClosed.preimage, Topology.IsInducing.continuous
-- 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
s : Set X
hs : s ∈ 𝓝 (f b) ∧ IsClosed[inst] s
⊢ IsClosed[inst_2] (f ⁻¹' id s)

Tactic:
exact hs.2.preimage hf.continuous

Premises used: And.right, IsClosed.preimage, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : RegularSpace X
f : Y → X
⊢ RegularSpace Y

Tactic:
letI := induced f ‹_›
  (IsInducing.induced f).regularSpace

Premises used: Topology.IsInducing.regularSpace, Topology.IsInducing.induced
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
a : X
rw :
  HasBasis (α := X) (⨅ (i : (↑T : Type u_3)), 𝓝 a)
    (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
          If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
            IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
              (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
    fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
    ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
      If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i
⊢ (𝓝 a).HasBasis
    (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
          If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
            IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
              (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
    fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
    ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
      If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i

Tactic:
rw [nhds_sInf, ← iInf_subtype'']

Premises used: nhds_sInf, iInf_subtype''
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
a : X
⊢ HasBasis (α := X) (⨅ (i : (↑T : Type u_3)), 𝓝 a)
    (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
          If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
            IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
              (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
    fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
    ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
      If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i

Tactic:
.iInf fun t : T => @closed_nhds_basis X t (h t t.2) a

Premises used: Filter.HasBasis.iInf, closed_nhds_basis
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
a : X
⊢ HasBasis (α := X) (⨅ (i : (↑T : Type u_3)), 𝓝 a)
    (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
          If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
            IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
              (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
    fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
    ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
      If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i

Tactic:
exact .iInf fun t : T => @closed_nhds_basis X t (h t t.2) a
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
⊢ ∀ (a : X),
    (𝓝 a).HasBasis
      (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
        If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
          ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
            If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
              IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
                (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
      fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
        If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i

Tactic:
have : ∀ a, (𝓝 a).HasBasis
      (fun If : Σ I : Set T, I → Set X =>
        If.1.Finite ∧ ∀ i : If.1, If.2 i ∈ @nhds X i a ∧ @IsClosed X i (If.2 i))
      fun If => ⋂ i : If.1, If.snd i := fun a ↦ by
    rw [nhds_sInf, ← iInf_subtype'']
    exact .iInf fun t : T => @closed_nhds_basis X t (h t t.2) a
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis
      (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
        If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
          ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
            If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
              IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
                (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
      fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
        If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i
⊢ RegularSpace X

Tactic:
.of_hasBasis this fun a If hIf => isClosed_iInter fun i => ?_

Premises used: RegularSpace.of_hasBasis, isClosed_iInter
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis
      (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
        If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
          ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
            If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
              IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
                (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
      fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
        If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i
refine :
  ∀ (a : X) (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X))
    (hIf :
      If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
        ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
          If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
            IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
              (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
    (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
    IsClosed[sInf T] (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i)
⊢ RegularSpace X

Tactic:
refine .of_hasBasis this fun a If hIf => isClosed_iInter fun i => ?_
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis
      (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
        If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
          ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
            If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
              IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
                (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
      fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
        If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i
a : X
If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)
hIf :
  If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
    ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
      If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
        IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
          (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i)
i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)
⊢ IsClosed[sInf T] (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i)

Tactic:
(hIf.2 i).2.mono (sInf_le (i : T).2)

Premises used: IsClosed.mono, And.right, sInf_le, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
T : Set (TopologicalSpace X)
h : ∀ t ∈ T, RegularSpace X
x : TopologicalSpace X := sInf T
this :
  ∀ (a : X),
    (𝓝 a).HasBasis
      (fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
        If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
          ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
            If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
              IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
                (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i))
      fun (If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)) ↦
      ⋂ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
        If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i
a : X
If : (I : Set (↑T : Type u_3)) × ((↑I : Type u_3) → Set X)
hIf :
  If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X).Finite ∧
    ∀ (i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)),
      If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i ∈ 𝓝 a ∧
        IsClosed[(↑(↑i : (↑T : Type u_3)) : TopologicalSpace X)]
          (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i)
i : (↑(If.fst (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X)) : Type u_3)
⊢ IsClosed[sInf T] (If.snd (β := fun (I : Set (↑T : Type u_3)) ↦ (↑I : Type u_3) → Set X) i)

Tactic:
exact (hIf.2 i).2.mono (sInf_le (i : T).2)

Premises used: IsClosed.mono, And.right, sInf_le, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Separation.Regular
Goal:
ι : Sort u_3
X : Type u_4
t : ι → TopologicalSpace X
h : ∀ (i : ι), RegularSpace X
⊢ RegularSpace X

Tactic:
regularSpace_sInf <| forall_mem_range.mpr h

Premises used: Iff.mpr, iInf, Set.forall_mem_range, regularSpace_sInf
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : RegularSpace X
h₂ : RegularSpace X
rw : RegularSpace X
⊢ RegularSpace X

Tactic:
rw [inf_eq_iInf]

Premises used: inf_eq_iInf
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : RegularSpace X
h₂ : RegularSpace X
⊢ RegularSpace X

Tactic:
regularSpace_iInf (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Premises used: Iff.mpr, Bool.forall_bool, regularSpace_iInf, And.intro
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : RegularSpace X
h₂ : RegularSpace X
⊢ RegularSpace X

Tactic:
exact regularSpace_iInf (Bool.forall_bool.2 ⟨h₂, h₁⟩)
-- 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
p : X → Prop
⊢ RegularSpace.{u_1} (Subtype p)

Tactic:
IsEmbedding.subtypeVal.isInducing.regularSpace

Premises used: Topology.IsEmbedding.isInducing, Topology.IsInducing.regularSpace, Topology.IsEmbedding.subtypeVal
-- 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
inst_2 : TopologicalSpace Y
inst_3 : RegularSpace Y
⊢ RegularSpace (X × Y)

Tactic:
(regularSpace_induced (@Prod.fst X Y)).inf (regularSpace_induced (@Prod.snd X Y))

Premises used: Prod.fst, RegularSpace.inf, regularSpace_induced, Prod.snd
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : RegularSpace X_1
x : X_1
s : Set X_1
ι : Type u_3
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), RegularSpace.{u_4} (X i)
⊢ RegularSpace ((i : ι) → X i)

Tactic:
regularSpace_iInf fun _ => regularSpace_induced _

Premises used: regularSpace_iInf, regularSpace_induced
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
hst : Disjoint s t
⊢ SeparatedNhds s t

Tactic:
simpa only [separatedNhds_iff_disjoint, hs.disjoint_nhdsSet_left, disjoint_nhds_nhdsSet,
    ht.closure_eq, disjoint_left] using hst

Premises used: Set.disjoint_left, IsClosed.closure_eq, IsCompact.disjoint_nhdsSet_left, separatedNhds_iff_disjoint, disjoint_nhds_nhdsSet
-- 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
inl : ∀ (empty_X : IsEmpty X), _root_.HasSeparatingCover s t
inr : ∀ (nonempty_X : Nonempty X), _root_.HasSeparatingCover s t
⊢ _root_.HasSeparatingCover s t

Tactic:
rcases isEmpty_or_nonempty X with empty_X | nonempty_X

Premises used: isEmpty_or_nonempty
-- 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
empty_X : IsEmpty X
inl : _root_.HasSeparatingCover ∅ t
⊢ _root_.HasSeparatingCover s t

Tactic:
rw [subset_eq_empty (t := s) (fun ⦃_⦄ _ ↦ trivial) (univ_eq_empty_iff.mpr empty_X)]

Premises used: Iff.mpr, trivial, Set.univ_eq_empty_iff, Set.subset_eq_empty
-- 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
empty_X : IsEmpty X
⊢ _root_.HasSeparatingCover ∅ t

Tactic:
hasSeparatingCovers_iff_separatedNhds.mpr (SeparatedNhds.empty_left t) |>.1

Premises used: Iff.mpr, hasSeparatingCovers_iff_separatedNhds, And.left, SeparatedNhds.empty_left
-- 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
empty_X : IsEmpty X
⊢ _root_.HasSeparatingCover ∅ t

Tactic:
exact hasSeparatingCovers_iff_separatedNhds.mpr (SeparatedNhds.empty_left t) |>.1

Premises used: Iff.mpr, hasSeparatingCovers_iff_separatedNhds, And.left, SeparatedNhds.empty_left
-- 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
a : X
inr :
  ∀
    (this :
      ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [LindelofSpace X] [RegularSpace X] (s_cl : IsClosed s)
        (t_cl : IsClosed t) (st_dis : Disjoint s t) (nonempty_X : Nonempty X) (a : X) (ains : a ∈ s),
        ∃ (n : Set X), IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n))
    (ains : a ∉ s), ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)
wlog :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [LindelofSpace X] [RegularSpace X] (s_cl : IsClosed s)
    (t_cl : IsClosed t) (st_dis : Disjoint s t) (nonempty_X : Nonempty X) (a : X) (ains : a ∈ s),
    ∃ (n : Set X), IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)
⊢ ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)

Tactic:
wlog ains : a ∈ s
-- 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
a : X
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [LindelofSpace X] [RegularSpace X] (s_cl : IsClosed s)
    (t_cl : IsClosed t) (st_dis : Disjoint s t) (nonempty_X : Nonempty X) (a : X) (ains : a ∈ s),
    ∃ (n : Set X), IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)
ains : a ∉ s
⊢ ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)

Tactic:
⟨∅, isOpen_empty, SeparatedNhds.empty_left t |>.disjoint_closure_left, fun a ↦ ains a⟩

Premises used: SeparatedNhds.disjoint_closure_left, And.intro, Exists.intro, SeparatedNhds.empty_left, EmptyCollection.emptyCollection, isOpen_empty
-- 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
a : X
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [LindelofSpace X] [RegularSpace X] (s_cl : IsClosed s)
    (t_cl : IsClosed t) (st_dis : Disjoint s t) (nonempty_X : Nonempty X) (a : X) (ains : a ∈ s),
    ∃ (n : Set X), IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)
ains : a ∉ s
⊢ ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)

Tactic:
exact ⟨∅, isOpen_empty, SeparatedNhds.empty_left t |>.disjoint_closure_left, fun a ↦ ains a⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
s t : Set X
inst_2 : LindelofSpace X
inst_3 : RegularSpace X
s_cl : IsClosed[inst_1] s
t_cl : IsClosed[inst_1] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
ains : a ∈ s
obtain :
  ∀ (n : Set X) (nna : n ∈ 𝓝 a) (ncl : IsClosed[inst_1] n) (nsubkc : n ⊆ tᶜ),
    ∃ (n : Set X), IsOpen[inst_1] n ∧ Disjoint (closure[inst_1] n) t ∧ (a ∈ s → a ∈ n)
⊢ ∃ (n : Set X), IsOpen[inst_1] n ∧ Disjoint (closure[inst_1] n) t ∧ (a ∈ s → a ∈ n)

Tactic:
obtain ⟨n, nna, ncl, nsubkc⟩ := ((regularSpace_TFAE X).out 0 3 :).mp ‹RegularSpace X› a tᶜ <|
      t_cl.compl_mem_nhds (disjoint_left.mp st_dis ains)

Premises used: Compl.compl, Set.disjoint_left, IsClosed.compl_mem_nhds, List.TFAE.out, Iff.mp, regularSpace_TFAE, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
s t : Set X
inst_2 : LindelofSpace X
inst_3 : RegularSpace X
s_cl : IsClosed[inst_1] s
t_cl : IsClosed[inst_1] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
ains : a ∈ s
n : Set X
nna : n ∈ 𝓝 a
ncl : IsClosed[inst_1] n
nsubkc : n ⊆ tᶜ
⊢ ∃ (n : Set X), IsOpen[inst_1] n ∧ Disjoint (closure[inst_1] n) t ∧ (a ∈ s → a ∈ n)

Tactic:
⟨interior n,
       isOpen_interior,
       disjoint_left.mpr fun ⦃_⦄ ain ↦
         nsubkc <| (IsClosed.closure_subset_iff ncl).mpr interior_subset ain,
       fun _ ↦ mem_interior_iff_mem_nhds.mpr nna⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, interior_subset, isOpen_interior, Set.disjoint_left, IsClosed.closure_subset_iff, And.intro, interior, Exists.intro
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
s t : Set X
inst_2 : LindelofSpace X
inst_3 : RegularSpace X
s_cl : IsClosed[inst_1] s
t_cl : IsClosed[inst_1] t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
ains : a ∈ s
n : Set X
nna : n ∈ 𝓝 a
ncl : IsClosed[inst_1] n
nsubkc : n ⊆ tᶜ
⊢ ∃ (n : Set X), IsOpen[inst_1] n ∧ Disjoint (closure[inst_1] n) t ∧ (a ∈ s → a ∈ n)

Tactic:
exact
      ⟨interior n,
       isOpen_interior,
       disjoint_left.mpr fun ⦃_⦄ ain ↦
         nsubkc <| (IsClosed.closure_subset_iff ncl).mpr interior_subset ain,
       fun _ ↦ mem_interior_iff_mem_nhds.mpr nna⟩
-- 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
⊢ ∀ (a : X), ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)

Tactic:
have (a : X) : ∃ n : Set X, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n) := by
    wlog ains : a ∈ s
    · exact ⟨∅, isOpen_empty, SeparatedNhds.empty_left t |>.disjoint_closure_left, fun a ↦ ains a⟩
    obtain ⟨n, nna, ncl, nsubkc⟩ := ((regularSpace_TFAE X).out 0 3 :).mp ‹RegularSpace X› a tᶜ <|
      t_cl.compl_mem_nhds (disjoint_left.mp st_dis ains)
    exact
      ⟨interior n,
       isOpen_interior,
       disjoint_left.mpr fun ⦃_⦄ ain ↦
         nsubkc <| (IsClosed.closure_subset_iff ncl).mpr interior_subset ain,
       fun _ ↦ mem_interior_iff_mem_nhds.mpr nna⟩
-- 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
this : ∀ (a : X), ∃ (n : Set X), IsOpen[inst] n ∧ Disjoint (closure[inst] n) t ∧ (a ∈ s → a ∈ n)
inr :
  ∀ (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), _root_.HasSeparatingCover s t
⊢ _root_.HasSeparatingCover s t

Tactic:
choose u u_open u_dis u_nhds using this