awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hst :
  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)
obtain :
  ∀ (U V : Set { x : X // x ∈ e }) (hU : IsOpen[instTopologicalSpaceSubtype] U)
    (hV : IsOpen[instTopologicalSpaceSubtype] V) (hsU : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U)
    (htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V) (hUV : Disjoint U V), Disjoint (𝓝ˢ s) (𝓝ˢ t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
obtain ⟨U, V, hU, hV, hsU, htV, hUV⟩ := normal_separation
    (isClosed_closure.preimage continuous_subtype_val)
    (isClosed_closure.preimage continuous_subtype_val) hst

Premises used: continuous_subtype_val, normal_separation, IsClosed.preimage, isClosed_closure
-- 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)
hst :
  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)
U V : Set { x : X // x ∈ e }
hU : IsOpen[instTopologicalSpaceSubtype] U
hV : IsOpen[instTopologicalSpaceSubtype] V
hsU : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
hUV : Disjoint U V
⊢ ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = U

Tactic:
rw [Topology.IsInducing.subtypeVal.isOpen_iff] at hU hV

Premises used: Topology.IsInducing.isOpen_iff, Topology.IsInducing.subtypeVal
-- 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)
hst :
  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)
U V : Set { x : X // x ∈ e }
hU : IsOpen[instTopologicalSpaceSubtype] U
hV : IsOpen[instTopologicalSpaceSubtype] V
hsU : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
hUV : Disjoint U V
hU₁ : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = U
⊢ ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = V

Tactic:
rw [Topology.IsInducing.subtypeVal.isOpen_iff] at hU hV

Premises used: Topology.IsInducing.isOpen_iff, Topology.IsInducing.subtypeVal
-- 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)
hst :
  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)
U V : Set { x : X // x ∈ e }
hU : IsOpen[instTopologicalSpaceSubtype] U
hV : IsOpen[instTopologicalSpaceSubtype] V
hsU : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
hUV : Disjoint U V
hU₁ : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = U
hV₁ : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = V
⊢ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U

Tactic:
rw [Topology.IsInducing.subtypeVal.isOpen_iff] at hU hV

Premises used: Topology.IsInducing.isOpen_iff, Topology.IsInducing.subtypeVal
-- 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)
hst :
  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)
U V : Set { x : X // x ∈ e }
hU : IsOpen[instTopologicalSpaceSubtype] U
hV : IsOpen[instTopologicalSpaceSubtype] V
hsU : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
hUV : Disjoint U V
hU₁ : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = U
hV₁ : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = V
hsU₁ : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
⊢ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V

Tactic:
rw [Topology.IsInducing.subtypeVal.isOpen_iff] at hU hV

Premises used: Topology.IsInducing.isOpen_iff, Topology.IsInducing.subtypeVal
-- 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)
hst :
  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)
U V : Set { x : X // x ∈ e }
hU : IsOpen[instTopologicalSpaceSubtype] U
hV : IsOpen[instTopologicalSpaceSubtype] V
hsU : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
hUV : Disjoint U V
hU₁ : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = U
hV₁ : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = V
hsU₁ : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
htV₁ : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
⊢ Disjoint U V

Tactic:
rw [Topology.IsInducing.subtypeVal.isOpen_iff] at hU hV

Premises used: Topology.IsInducing.isOpen_iff, Topology.IsInducing.subtypeVal
-- 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)
hst :
  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)
U V : Set { x : X // x ∈ e }
hU : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = U
hV : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = V
hsU : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s ⊆ U
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
hUV : Disjoint U V
obtain :
  ∀ (U : Set X) (hU : IsOpen[inst] U)
    (hsU :
      Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
        (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U))
    (hUV : Disjoint (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U) V), Disjoint (𝓝ˢ s) (𝓝ˢ t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
obtain ⟨U, hU, rfl⟩ := hU

Premises used: rfl
-- 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)
hst :
  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)
V : Set { x : X // x ∈ e }
hV : ∃ (t : Set X), IsOpen[inst] t ∧ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' t = V
htV : Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t ⊆ V
U : Set X
hU : IsOpen[inst] U
hsU :
  Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
hUV : Disjoint (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U) V
obtain :
  ∀ (V : Set X) (hV : IsOpen[inst] V)
    (htV :
      Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
        (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V))
    (hUV :
      Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
        (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)),
    Disjoint (𝓝ˢ s) (𝓝ˢ t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
obtain ⟨V, hV, rfl⟩ := hV

Premises used: rfl
-- 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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU :
  Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
V : Set X
hV : IsOpen[inst] V
htV :
  Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
rw : SeparatedNhds s t
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
rw [← separatedNhds_iff_disjoint]

Premises used: separatedNhds_iff_disjoint
-- 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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU :
  Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] s)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
V : Set X
hV : IsOpen[inst] V
htV :
  Subset (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' closure[inst] t)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
rw :
  ∀ (hsU : closure[inst] s ∩ e ⊆ U ∩ e) (V : Set X) (hV : IsOpen[inst] V) (htV : closure[inst] t ∩ e ⊆ V ∩ e)
    (hUV :
      Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
        (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)),
    SeparatedNhds s t
⊢ SeparatedNhds s t

Tactic:
rw [Subtype.preimage_val_subset_preimage_val_iff, inter_comm e, inter_comm e] at hsU htV

Premises used: Set.inter_comm, Subtype.preimage_val_subset_preimage_val_iff
-- 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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
⊢ SeparatedNhds s t

Tactic:
⟨U ∩ e, V ∩ e, hU.inter he, hV.inter he, ?_, ?_, ?_⟩

Premises used: Inter.inter, And.intro, IsOpen.inter, Exists.intro, SeparatedNhds
-- 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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
refine_1 : s ⊆ U ∩ e
refine_2 : t ⊆ V ∩ e
refine_3 : Disjoint (U ∩ e) (V ∩ e)
⊢ SeparatedNhds s t

Tactic:
refine ⟨U ∩ e, V ∩ e, hU.inter he, hV.inter 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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
x : X
hx : x ∈ s
⊢ x ∈ U ∩ e

Tactic:
hsU ⟨subset_closure hx, fun h => hsT.notMem_of_mem_left hx h.2⟩

Premises used: subset_closure, And.right, And.intro, Disjoint.notMem_of_mem_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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
x : X
hx : x ∈ s
⊢ x ∈ U ∩ e

Tactic:
exact hsU ⟨subset_closure hx, fun h => hsT.notMem_of_mem_left hx h.2⟩

Premises used: subset_closure, And.right, And.intro, Disjoint.notMem_of_mem_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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
x : X
hx : x ∈ t
⊢ x ∈ V ∩ e

Tactic:
htV ⟨subset_closure hx, fun h => hSt.notMem_of_mem_left h.1 hx⟩

Premises used: subset_closure, And.left, And.intro, Disjoint.notMem_of_mem_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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
x : X
hx : x ∈ t
⊢ x ∈ V ∩ e

Tactic:
exact htV ⟨subset_closure hx, fun h => hSt.notMem_of_mem_left h.1 hx⟩

Premises used: subset_closure, And.left, And.intro, Disjoint.notMem_of_mem_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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  Disjoint (α := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U)
    (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
refine_3 :
  ∀
    (hUV :
      ∀ ⦃a : { x : X // x ∈ e }⦄,
        Membership.mem (γ := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U) a →
          a ∉ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V)
    ⦃a : X⦄, a ∈ U ∩ e → a ∉ V ∩ e
⊢ Disjoint (U ∩ e) (V ∩ e)

Tactic:
rw [disjoint_left] at hUV ⊢

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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  ∀ ⦃a : { x : X // x ∈ e }⦄,
    Membership.mem (γ := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U) a →
      a ∉ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V
x : X
hxU : x ∈ U ∩ e
hxV : x ∈ V ∩ e
⊢ False

Tactic:
@hUV ⟨x, hxU.2⟩ hxU.1 hxV.1

Premises used: And.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)
hst :
  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)
U : Set X
hU : IsOpen[inst] U
hsU : closure[inst] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst] V
htV : closure[inst] t ∩ e ⊆ V ∩ e
hUV :
  ∀ ⦃a : { x : X // x ∈ e }⦄,
    Membership.mem (γ := Set { x : X // x ∈ e }) (Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' U) a →
      a ∉ Subtype.val (p := fun (x : X) ↦ x ∈ e) ⁻¹' V
x : X
hxU : x ∈ U ∩ e
hxV : x ∈ V ∩ e
⊢ False

Tactic:
exact @hUV ⟨x, hxU.2⟩ hxU.1 hxV.1

Premises used: And.left
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ CompletelyNormalSpace X ↔ ∀ (s : Set X), NormalSpace.{u_1} (↑s : Type u_1)

Tactic:
⟨fun _ _ => inferInstance, fun h =>
    completelyNormalSpace_iff_forall_isOpen_normalSpace.2 fun s _ => h s⟩

Premises used: Iff.mpr, inferInstance, Iff.intro, completelyNormalSpace_iff_forall_isOpen_normalSpace
-- 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
⊢ CompletelyNormalSpace X

Tactic:
.of_forall_normalSpace fun _ => .of_regularSpace_secondCountableTopology

Premises used: NormalSpace.of_regularSpace_secondCountableTopology, CompletelyNormalSpace.of_forall_normalSpace
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T5Space Y
e : X → Y
he : IsEmbedding e
⊢ CompletelyNormalSpace X

Tactic:
have := he.completelyNormalSpace
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T5Space Y
e : X → Y
he : IsEmbedding e
this : CompletelyNormalSpace X
⊢ ∀ ⦃s t : Set X⦄, Disjoint (closure[inst] s) t → Disjoint s (closure[inst] t) → Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
completely_normal

Premises used: 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 : T5Space Y
e : X → Y
he : IsEmbedding e
this : CompletelyNormalSpace X
⊢ ∀ ⦃s t : Set X⦄, Disjoint (closure[inst] s) t → Disjoint s (closure[inst] t) → Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
exact completely_normal

Premises used: 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 : T5Space X
h : X ≃ₜ Y
⊢ T5Space Y

Tactic:
h.symm.isClosedEmbedding.t5Space

Premises used: Topology.IsEmbedding.t5Space, Topology.IsClosedEmbedding.toIsEmbedding, Homeomorph.symm, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T5Space X
p : X → Prop
⊢ T5Space.{u_1} { x : X // p x }

Tactic:
IsEmbedding.subtypeVal.t5Space

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

Tactic:
IsEmbedding.uliftDown.t5Space

Premises used: Topology.IsEmbedding.t5Space, Topology.IsEmbedding.uliftDown
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T5Space X ↔ ∀ (s : Set X), T4Space.{u_1} (↑s : Type u_1)

Tactic:
⟨fun _ _ => inferInstance, fun h => t5Space_iff_forall_isOpen_t4Space.2 fun s _ => h s⟩

Premises used: Iff.mpr, inferInstance, Iff.intro, t5Space_iff_forall_isOpen_t4Space
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
inst_2 : R0Space X
rwa : T1Space.{u_1} (SeparationQuotient X)
rwa₁ rwa₂ rwa₃ rwa₄ : R0Space X
⊢ ∀ (x : SeparationQuotient X), IsClosed (X := SeparationQuotient X) {x}

Tactic:
rwa [((t1Space_TFAE (SeparationQuotient X)).out 1 0 :), SeparationQuotient.t1Space_iff]

Premises used: SeparationQuotient.t1Space_iff, t1Space_TFAE, List.TFAE.out, SeparationQuotient, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Regular
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompletelyNormalSpace X
inst_2 : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
rw : Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (𝓝ˢ (SeparationQuotient.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