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
s : Set (SeparationQuotient X)
hs : IsClosed s
a : X
ha : SeparationQuotient.mk a ∉ s
rw : Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (𝓝 a)
⊢ Disjoint (𝓝ˢ s) (𝓝 (SeparationQuotient.mk a))

Tactic:
rw [← disjoint_comap_iff surjective_mk, comap_mk_nhds_mk, comap_mk_nhdsSet]

Premises used: Filter.disjoint_comap_iff, SeparationQuotient.comap_mk_nhds_mk, SeparationQuotient.surjective_mk, SeparationQuotient.comap_mk_nhdsSet
-- 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)
hs : IsClosed s
a : X
ha : SeparationQuotient.mk a ∉ s
⊢ Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (𝓝 a)

Tactic:
RegularSpace.regular (hs.preimage continuous_mk) ha

Premises used: SeparationQuotient.continuous_mk, RegularSpace.regular, IsClosed.preimage
-- 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)
hs : IsClosed s
a : X
ha : SeparationQuotient.mk a ∉ s
⊢ Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (𝓝 a)

Tactic:
exact RegularSpace.regular (hs.preimage continuous_mk) ha

Premises used: SeparationQuotient.continuous_mk, RegularSpace.regular, IsClosed.preimage
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
H1 : IsClosed[inst] s
H2 : IsClosed[inst] t
H3 : Disjoint s t
⊢ SeparatedNhds s t

Tactic:
NormalSpace.normal s t H1 H2 H3

Premises used: NormalSpace.normal
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hd : Disjoint s t
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
(normal_separation hs ht hd).disjoint_nhdsSet

Premises used: SeparatedNhds.disjoint_nhdsSet, normal_separation
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsOpen[inst] t
hst : s ⊆ t
⊢ Disjoint s tᶜ

Tactic:
have : Disjoint s tᶜ := Set.disjoint_left.mpr fun x hxs hxt => hxt (hst hxs)
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsOpen[inst] t
hst : s ⊆ t
this : Disjoint s tᶜ
rcases :
  ∀ (s' t' : Set X) (hs' : IsOpen[inst] s') (ht' : IsOpen[inst] t') (hss' : s ⊆ s') (htt' : tᶜ ⊆ t')
    (hs't' : Disjoint s' t'), ∃ (u : Set X), IsOpen[inst] u ∧ s ⊆ u ∧ closure[inst] u ⊆ t
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ s ⊆ u ∧ closure[inst] u ⊆ t

Tactic:
rcases normal_separation hs (isClosed_compl_iff.2 ht) this with
    ⟨s', t', hs', ht', hss', htt', hs't'⟩

Premises used: Iff.mpr, normal_separation, isClosed_compl_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsOpen[inst] t
hst : s ⊆ t
this : Disjoint s tᶜ
s' t' : Set X
hs' : IsOpen[inst] s'
ht' : IsOpen[inst] t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ s ⊆ u ∧ closure[inst] u ⊆ t

Tactic:
⟨s', hs', hss', Subset.trans (closure_minimal ?_ (isClosed_compl_iff.2 ht'))
    (compl_subset_comm.1 htt')⟩

Premises used: Iff.mpr, Set.Subset.trans, closure_minimal, Set.compl_subset_comm, And.intro, Exists.intro, Iff.mp, isClosed_compl_iff
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsOpen[inst] t
hst : s ⊆ t
this : Disjoint s tᶜ
s' t' : Set X
hs' : IsOpen[inst] s'
ht' : IsOpen[inst] t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
refine : s' ⊆ t'ᶜ
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ s ⊆ u ∧ closure[inst] u ⊆ t

Tactic:
refine ⟨s', hs', hss', Subset.trans (closure_minimal ?_ (isClosed_compl_iff.2 ht'))
    (compl_subset_comm.1 htt')⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsOpen[inst] t
hst : s ⊆ t
this : Disjoint s tᶜ
s' t' : Set X
hs' : IsOpen[inst] s'
ht' : IsOpen[inst] t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ s' ⊆ t'ᶜ

Tactic:
fun x hxs hxt => hs't'.le_bot ⟨hxs, hxt⟩

Premises used: Disjoint.le_bot, Set.Mem, setOf, Set.Subset, And.intro, Not
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsOpen[inst] t
hst : s ⊆ t
this : Disjoint s tᶜ
s' t' : Set X
hs' : IsOpen[inst] s'
ht' : IsOpen[inst] t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ s' ⊆ t'ᶜ

Tactic:
exact fun x hxs hxt => hs't'.le_bot ⟨hxs, hxt⟩

Premises used: Disjoint.le_bot, And.intro
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
u s : Set X
h : s ∈ 𝓝ˢ u
hu : IsClosed[inst] u
obtain : ∀ (o : Set X) (ho_open : IsOpen[inst] o) (huo : u ⊆ o) (hos : o ⊆ s), ∃ t ∈ 𝓝ˢ u, IsClosed[inst] t ∧ t ⊆ s
⊢ ∃ t ∈ 𝓝ˢ u, IsClosed[inst] t ∧ t ⊆ s

Tactic:
obtain ⟨o, ho_open, huo, hos⟩ := mem_nhdsSet_iff_exists.mp h

Premises used: mem_nhdsSet_iff_exists, Iff.mp
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
u s : Set X
h : s ∈ 𝓝ˢ u
hu : IsClosed[inst] u
o : Set X
ho_open : IsOpen[inst] o
huo : u ⊆ o
hos : o ⊆ s
obtain :
  ∀ (v : Set X) (hv_open : IsOpen[inst] v) (huv : u ⊆ v) (hcvo : closure[inst] v ⊆ o),
    ∃ t ∈ 𝓝ˢ u, IsClosed[inst] t ∧ t ⊆ s
⊢ ∃ t ∈ 𝓝ˢ u, IsClosed[inst] t ∧ t ⊆ s

Tactic:
obtain ⟨v, hv_open, huv, hcvo⟩ := normal_exists_closure_subset hu ho_open huo

Premises used: normal_exists_closure_subset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
u s : Set X
h : s ∈ 𝓝ˢ u
hu : IsClosed[inst] u
o : Set X
ho_open : IsOpen[inst] o
huo : u ⊆ o
hos : o ⊆ s
v : Set X
hv_open : IsOpen[inst] v
huv : u ⊆ v
hcvo : closure[inst] v ⊆ o
⊢ ∃ t ∈ 𝓝ˢ u, IsClosed[inst] t ∧ t ⊆ s

Tactic:
⟨closure v, ?_, isClosed_closure, hcvo.trans hos⟩

Premises used: HasSubset.Subset.trans, closure, And.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
u s : Set X
h : s ∈ 𝓝ˢ u
hu : IsClosed[inst] u
o : Set X
ho_open : IsOpen[inst] o
huo : u ⊆ o
hos : o ⊆ s
v : Set X
hv_open : IsOpen[inst] v
huv : u ⊆ v
hcvo : closure[inst] v ⊆ o
refine : closure[inst] v ∈ 𝓝ˢ u
⊢ ∃ t ∈ 𝓝ˢ u, IsClosed[inst] t ∧ t ⊆ s

Tactic:
refine ⟨closure v, ?_, isClosed_closure, hcvo.trans hos⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
u s : Set X
h : s ∈ 𝓝ˢ u
hu : IsClosed[inst] u
o : Set X
ho_open : IsOpen[inst] o
huo : u ⊆ o
hos : o ⊆ s
v : Set X
hv_open : IsOpen[inst] v
huv : u ⊆ v
hcvo : closure[inst] v ⊆ o
⊢ closure[inst] v ∈ 𝓝ˢ u

Tactic:
mem_of_superset (mem_nhdsSet_iff_exists.mpr ⟨v, hv_open, huv, subset_rfl⟩) subset_closure

Premises used: Iff.mpr, subset_closure, mem_nhdsSet_iff_exists, And.intro, Exists.intro, subset_rfl, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
u s : Set X
h : s ∈ 𝓝ˢ u
hu : IsClosed[inst] u
o : Set X
ho_open : IsOpen[inst] o
huo : u ⊆ o
hos : o ⊆ s
v : Set X
hv_open : IsOpen[inst] v
huv : u ⊆ v
hcvo : closure[inst] v ⊆ o
⊢ closure[inst] v ∈ 𝓝ˢ u

Tactic:
exact mem_of_superset (mem_nhdsSet_iff_exists.mpr ⟨v, hv_open, huv, subset_rfl⟩) subset_closure

Premises used: Iff.mpr, subset_closure, mem_nhdsSet_iff_exists, And.intro, Exists.intro, subset_rfl, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
u : Set X
hu : IsClosed[inst] u
⊢ (𝓝ˢ u).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝ˢ u ∧ IsClosed[inst] s) id

Tactic:
hasBasis_self.2 fun _ ht ↦ exists_mem_nhdsSet_isClosed_subset ht hu

Premises used: Iff.mpr, exists_mem_nhdsSet_isClosed_subset, Filter.hasBasis_self
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
u : Set X
hu : IsClosed[inst] u
⊢ (𝓝ˢ u).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝ˢ u ∧ IsClosed[inst] s) id

Tactic:
refine hasBasis_self.2 fun _ ht ↦ exists_mem_nhdsSet_isClosed_subset ht hu

Premises used: Iff.mpr, exists_mem_nhdsSet_isClosed_subset, Filter.hasBasis_self
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
u : Set X
hu : IsClosed[inst] u
⊢ (𝓝ˢ u).lift' closure[inst] = 𝓝ˢ u

Tactic:
(closed_nhdsSet_basis u hu).lift'_closure_eq_self fun _ ↦ And.right

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

Tactic:
lift'_nhdsSet_closure u hu ▸ h.lift'_closure

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

Tactic:
(𝓝ˢ u).basis_sets.nhdsSet_closure hu

Premises used: Filter.HasBasis.nhdsSet_closure, Filter.basis_sets, nhdsSet
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X → Y
hf : IsClosedEmbedding f
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
⊢ SeparatedNhds (f '' s) (f '' t)

Tactic:
have H : SeparatedNhds (f '' s) (f '' t) :=
      NormalSpace.normal (f '' s) (f '' t) (hf.isClosedMap s hs) (hf.isClosedMap t ht)
        (disjoint_image_of_injective hf.injective hst)
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X → Y
hf : IsClosedEmbedding f
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
H : SeparatedNhds (f '' s) (f '' t)
⊢ SeparatedNhds s t

Tactic:
(H.preimage hf.continuous).mono (subset_preimage_image _ _) (subset_preimage_image _ _)

Premises used: SeparatedNhds.mono, SeparatedNhds.preimage, Topology.IsClosedEmbedding.continuous, Set.subset_preimage_image
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X → Y
hf : IsClosedEmbedding f
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hst : Disjoint s t
H : SeparatedNhds (f '' s) (f '' t)
⊢ SeparatedNhds s t

Tactic:
exact (H.preimage hf.continuous).mono (subset_preimage_image _ _) (subset_preimage_image _ _)

Premises used: SeparatedNhds.mono, SeparatedNhds.preimage, Topology.IsClosedEmbedding.continuous, Set.subset_preimage_image
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace X
h : X ≃ₜ Y
⊢ NormalSpace Y

Tactic:
h.symm.isClosedEmbedding.normalSpace

Premises used: Topology.IsClosedEmbedding.normalSpace, Homeomorph.symm, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : RegularSpace X
inst_2 : SecondCountableTopology X
⊢ NormalSpace X

Tactic:
of_regularSpace_lindelofSpace

Premises used: NormalSpace.of_regularSpace_lindelofSpace
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : NormalSpace X
⊢ T4Space X

Tactic:
⟨⟩

Premises used: T4Space.mk
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T4Space X
s : Set X
a : X
hs : IsClosed[inst] s
hxs : a ∉ s
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
simpa only [nhdsSet_singleton] using (normal_separation hs isClosed_singleton
    (disjoint_singleton_right.mpr hxs)).disjoint_nhdsSet

Premises used: Iff.mpr, Set.disjoint_singleton_right, SeparatedNhds.disjoint_nhdsSet, normal_separation, nhdsSet_singleton, isClosed_singleton
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T4Space X
h : X ≃ₜ Y
⊢ T4Space Y

Tactic:
h.symm.isClosedEmbedding.t4Space

Premises used: Topology.IsClosedEmbedding.t4Space, Homeomorph.symm, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T4Space X
⊢ T4Space (ULift.{u_3, u_1} X)

Tactic:
IsClosedEmbedding.uliftDown.t4Space

Premises used: Topology.IsClosedEmbedding.t4Space, Topology.IsClosedEmbedding.uliftDown
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set (SeparationQuotient X)
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
rw : Disjoint (𝓝ˢ (mk ⁻¹' s)) (𝓝ˢ (mk ⁻¹' t))
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
rw [← disjoint_comap_iff surjective_mk, comap_mk_nhdsSet, comap_mk_nhdsSet]

Premises used: Filter.disjoint_comap_iff, SeparationQuotient.surjective_mk, SeparationQuotient.comap_mk_nhdsSet
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set (SeparationQuotient X)
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ Disjoint (𝓝ˢ (mk ⁻¹' s)) (𝓝ˢ (mk ⁻¹' t))

Tactic:
disjoint_nhdsSet_nhdsSet (hs.preimage continuous_mk) (ht.preimage continuous_mk)
      (hd.preimage mk)

Premises used: SeparationQuotient.continuous_mk, disjoint_nhdsSet_nhdsSet, SeparationQuotient.mk, IsClosed.preimage, Disjoint.preimage
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set (SeparationQuotient X)
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ Disjoint (𝓝ˢ (mk ⁻¹' s)) (𝓝ˢ (mk ⁻¹' t))

Tactic:
exact disjoint_nhdsSet_nhdsSet (hs.preimage continuous_mk) (ht.preimage continuous_mk)
      (hd.preimage mk)

Premises used: SeparationQuotient.continuous_mk, disjoint_nhdsSet_nhdsSet, SeparationQuotient.mk, IsClosed.preimage, Disjoint.preimage
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hd rwa rwa₁ rwa₂ rwa₃ : Disjoint s t
⊢ Disjoint (closure[inst] s) t

Tactic:
rwa [hs.closure_eq]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
s t : Set X
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hd rwa rwa₁ rwa₂ rwa₃ : Disjoint s t
⊢ Disjoint s (closure[inst] t)

Tactic:
rwa [ht.closure_eq]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
⊢ CompletelyNormalSpace X

Tactic:
⟨fun s t hd₁ hd₂ => ?_⟩

Premises used: CompletelyNormalSpace.mk
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
refine :
  ∀ (s t : Set X) (hd₁ : Disjoint (closure[inst] s) t) (hd₂ : Disjoint s (closure[inst] t)), Disjoint (𝓝ˢ s) (𝓝ˢ t)
⊢ CompletelyNormalSpace X

Tactic:
refine ⟨fun s t hd₁ hd₂ => ?_⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure[inst] s) t
hd₂ : Disjoint s (closure[inst] t)
simp : Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
simp only [he.isInducing.nhdsSet_eq_comap]

Premises used: Topology.IsEmbedding.isInducing, Topology.IsInducing.nhdsSet_eq_comap
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure[inst] s) t
hd₂ : Disjoint s (closure[inst] t)
⊢ Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))

Tactic:
disjoint_comap (completely_normal ?_ ?_)

Premises used: Filter.disjoint_comap, CompletelyNormalSpace.completely_normal
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure[inst] s) t
hd₂ : Disjoint s (closure[inst] t)
refine_1 : Disjoint (closure[inst_1] (e '' s)) (e '' t)
refine_2 : Disjoint (e '' s) (closure[inst_1] (e '' t))
⊢ Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))

Tactic:
refine disjoint_comap (completely_normal ?_ ?_)

Premises used: Filter.disjoint_comap, CompletelyNormalSpace.completely_normal
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure[inst] s) t
hd₂ : Disjoint s (closure[inst] t)
refine_1 : e '' t ⊆ (closure[inst_1] (e '' s))ᶜ
refine_1₁ : t ⊆ e ⁻¹' (closure[inst_1] (e '' s))ᶜ
refine_1₂ : t ⊆ (e ⁻¹' closure[inst_1] (e '' s))ᶜ
refine_1₃ : t ⊆ (closure[inst] s)ᶜ
refine_1₄ refine_1₅ refine_1₆ refine_1₇ : Disjoint (closure[inst] s) t
⊢ Disjoint (closure[inst_1] (e '' s)) (e '' t)

Tactic:
rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]

Premises used: Set.subset_compl_iff_disjoint_left, Set.image_subset_iff, Set.preimage_compl, Topology.IsEmbedding.closure_eq_preimage_closure_image
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompletelyNormalSpace Y
e : X → Y
he : IsEmbedding e
s t : Set X
hd₁ : Disjoint (closure[inst] s) t
hd₂ : Disjoint s (closure[inst] t)
refine_2 : e '' s ⊆ (closure[inst_1] (e '' t))ᶜ
refine_2₁ : s ⊆ e ⁻¹' (closure[inst_1] (e '' t))ᶜ
refine_2₂ : s ⊆ (e ⁻¹' closure[inst_1] (e '' t))ᶜ
refine_2₃ : s ⊆ (closure[inst] t)ᶜ
refine_2₄ refine_2₅ refine_2₆ refine_2₇ : Disjoint s (closure[inst] t)
⊢ Disjoint (e '' s) (closure[inst_1] (e '' t))

Tactic:
rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_right]

Premises used: Set.subset_compl_iff_disjoint_right, Set.image_subset_iff, Set.preimage_compl, Topology.IsEmbedding.closure_eq_preimage_closure_image
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
p : X → Prop
⊢ CompletelyNormalSpace.{u_1} { x : X // p x }

Tactic:
IsEmbedding.subtypeVal.completelyNormalSpace

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

Tactic:
IsEmbedding.uliftDown.completelyNormalSpace

Premises used: Topology.IsEmbedding.uliftDown, Topology.IsEmbedding.completelyNormalSpace
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ CompletelyNormalSpace X ↔ ∀ (s : Set X), IsOpen[inst] s → NormalSpace.{u_1} (↑s : Type u_1)

Tactic:
⟨fun _ _ _ => inferInstance, fun h => ⟨fun s t hSt hsT => ?_⟩⟩

Premises used: inferInstance, Iff.intro, CompletelyNormalSpace.mk
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
refine :
  ∀ (h : ∀ (s : Set X), IsOpen[inst] s → NormalSpace.{u_1} (↑s : Type u_1)) (s t : Set X)
    (hSt : Disjoint (closure[inst] s) t) (hsT : Disjoint s (closure[inst] t)), Disjoint (𝓝ˢ s) (𝓝ˢ t)
⊢ CompletelyNormalSpace X ↔ ∀ (s : Set X), IsOpen[inst] s → NormalSpace.{u_1} (↑s : Type u_1)

Tactic:
refine ⟨fun _ _ _ => inferInstance, fun h => ⟨fun s t hSt hsT => ?_⟩⟩
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[inst] s → NormalSpace.{u_1} (↑s : Type u_1)
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
⊢ IsOpen[inst] e

Tactic:
have he : IsOpen e := (isClosed_closure.inter isClosed_closure).isOpen_compl
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[inst] s → NormalSpace.{u_1} (↑s : Type u_1)
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
⊢ NormalSpace.{u_1} (↑e : Type u_1)

Tactic:
specialize h e he
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
rw :
  ∀ ⦃a : { x : X // x ∈ e }⦄,
    Membership.mem (γ := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s) a →
      a ∉ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t
⊢ Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)

Tactic:
rw [disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
x : { x : X // x ∈ e }
hxs : Membership.mem (γ := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s) x
hxt : Membership.mem (γ := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t) x
⊢ False

Tactic:
x.2 ⟨hxs, hxt⟩

Premises used: And.intro, Subtype.property
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
x : { x : X // x ∈ e }
hxs : Membership.mem (γ := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s) x
hxt : Membership.mem (γ := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t) x
⊢ False

Tactic:
exact x.2 ⟨hxs, hxt⟩

Premises used: And.intro, Subtype.property
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst] s) t
hsT : Disjoint s (closure[inst] t)
e : Set X := (closure[inst] s ∩ closure[inst] t)ᶜ
he : IsOpen[inst] e
h : NormalSpace.{u_1} (↑e : Type u_1)
⊢ Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)

Tactic:
have hst : Disjoint (((↑) : e → X) ⁻¹' closure s) (((↑) : e → X) ⁻¹' closure t) := by
    rw [disjoint_left]
    intro x hxs hxt
    exact x.2 ⟨hxs, hxt⟩