awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x y : X
h : ¬Inseparable x y
U₁ U₂ : Set X
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
have rcases : ∀ (V₁ : Set X) (V₁_in : V₁ ∈ 𝓝 x) (V₁_closed : IsClosed[inst] V₁) (h₁ : V₁ ⊆ U₁),
  ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
Tactic: rcases exists_mem_nhds_isClosed_subset (U₁_op.mem_nhds x_in) with ⟨V₁, V₁_in, V₁_closed, h₁⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
x y : X
h : ¬Inseparable x y
U₁ U₂ : Set X
U₁_op : IsOpen[inst] U₁
U₂_op : IsOpen[inst] U₂
x_in : x ∈ U₁
y_in : y ∈ U₂
H : Disjoint U₁ U₂
V₁ : Set X
V₁_in : V₁ ∈ 𝓝 x
V₁_closed : IsClosed[inst] V₁
h₁ : V₁ ⊆ U₁
⊢ ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
have rcases : ∀ (V₂ : Set X) (V₂_in : V₂ ∈ 𝓝 y) (V₂_closed : IsClosed[inst] V₂) (h₂ : V₂ ⊆ U₂),
  ∃ U₁ ∈ 𝓝 x,
    ∃ V₁ ∈ 𝓝 x,
      ∃ U₂ ∈ 𝓝 y,
        ∃ V₂ ∈ 𝓝 y,
          IsClosed[inst] V₁ ∧ IsClosed[inst] V₂ ∧ IsOpen[inst] U₁ ∧ IsOpen[inst] U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
Tactic: rcases exists_mem_nhds_isClosed_subset (U₂_op.mem_nhds y_in) with ⟨V₂, V₂_in, V₂_closed, h₂⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).HasBasis (fun (L : Set X) ↦ L ∈ 𝓝ˢ K ∧ IsCompact L ∧ IsClosed[inst] L) id
have rw : ∀ (i : Set X), IsOpen[inst] i ∧ K ⊆ i → ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ i
Tactic: rw [hasBasis_self, (hasBasis_nhdsSet _).forall_iff (by grind)]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
⊢ IsOpen[inst] U ∧ K ⊆ U → ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ U
have this : ∀ (hU : IsOpen[inst] U) (h_KU : K ⊆ U), ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ U
Tactic: ⟨hU, h_KU⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
h_KU : K ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ U
have obtain : ∀ (L : Set X) (hL : IsCompact L) (hL' : IsClosed[inst] L) (hKL : K ⊆ interior L) (hLU : L ⊆ U),
  ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst] r) ∧ r ⊆ U
Tactic: obtain ⟨L, hL, hL', hKL, hLU⟩ := exists_compact_closed_between hK hU h_KU
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U ∧ IsCompact (closure[inst] V)
have rcases : ∀ (L : Set X) (L_compact : IsCompact L) (L_closed : IsClosed[inst] L) (KL : K ⊆ interior L) (LU : L ⊆ U),
  ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U ∧ IsCompact (closure[inst] V)
Tactic: rcases exists_compact_closed_between hK hU hKU with ⟨L, L_compact, L_closed, KL, LU⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed[inst] L
KL : K ⊆ interior L
LU : L ⊆ U
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U ∧ IsCompact (closure[inst] V)
have A : closure[inst] (interior L) ⊆ L
Tactic: have A : closure (interior L) ⊆ L := by
    apply (closure_mono interior_subset).trans (le_of_eq L_closed.closure_eq)
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
inst_2 : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed[inst] L
KL : K ⊆ interior L
LU : L ⊆ U
A : closure[inst] (interior L) ⊆ L
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ closure[inst] V ⊆ U ∧ IsCompact (closure[inst] V)
have refine : IsCompact (closure[inst] (interior L))
Tactic: refine ⟨interior L, isOpen_interior, KL, A.trans LU, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
⊢ closure[inst] s = nhdsKer s
have a : closure[inst] s ⊆ nhdsKer s
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
a : closure[inst] s ⊆ nhdsKer s
⊢ closure[inst] s = nhdsKer s
have a₁ : nhdsKer s ⊆ closure[inst] s
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
⊢ closure[inst] s ⊆ nhdsKer s
have a : closure[inst] s ⊆ ((𝓝ˢ s).lift' closure[inst]).ker
Tactic: rw [nhdsKer, ← hs.lift'_closure_nhdsSet]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
⊢ y ∈ closure[inst] s
have a : ∀ (hy' : y ∉ closure[inst] s), False
Tactic: by_contra! hy'
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
hy' : y ∉ closure[inst] s
⊢ False
have hy'₁ : ∃ s_1 ∈ 𝓝ˢ s, ∃ t ∈ 𝓝 y, Disjoint s_1 t
Tactic: rw [← _root_.disjoint_nhdsSet_nhds, Filter.disjoint_iff] at hy'
Cleared hypotheses: hy'
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
hy' : ∃ s_1 ∈ 𝓝ˢ s, ∃ t ∈ 𝓝 y, Disjoint s_1 t
⊢ False
have a : ∀ (t : Set X) (hts : t ∈ 𝓝ˢ s) (t' : Set X) (ht'y : t' ∈ 𝓝 y) (H : Disjoint t t'), False
Tactic: obtain ⟨t, hts, t', ht'y, H⟩ := hy'
Cleared hypotheses: hy'
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
⊢ T3Space X ↔ T0Space X
have mp : T3Space X → T0Space X
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : RegularSpace X
mp : T3Space X → T0Space X
⊢ T3Space X ↔ T0Space X
have mpr : T0Space X → T3Space X
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
⊢ T25Space X
have refine : ∀ (x y : X) (hne : x ≠ y), Disjoint ((𝓝 x).lift' closure[inst]) ((𝓝 y).lift' closure[inst])
Tactic: refine ⟨fun x y hne => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
x y : X
hne : x ≠ y
⊢ Disjoint ((𝓝 x).lift' closure[inst]) ((𝓝 y).lift' closure[inst])
have rw : Disjoint (𝓝 x) (𝓝 y)
Tactic: rw [lift'_nhds_closure, lift'_nhds_closure]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
x y : X
hne : x ≠ y
⊢ Disjoint (𝓝 x) (𝓝 y)
have this : x ∉ closure[inst] {y} ∨ y ∉ closure[inst] {x}
Tactic: have : x ∉ closure {y} ∨ y ∉ closure {x} :=
    (t0Space_iff_or_notMem_closure X).mp inferInstance hne
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T3Space X
x y : X
hne : x ≠ y
this : x ∉ closure[inst] {y} ∨ y ∉ closure[inst] {x}
⊢ Disjoint (𝓝 x) (𝓝 y)
have this₁ : Disjoint (𝓝 x) (𝓝 y) ∨ Disjoint (𝓝 y) (𝓝 x)
Tactic: simp only [← disjoint_nhds_nhdsSet, nhdsSet_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : RegularSpace X
s : Set (SeparationQuotient X)
a : SeparationQuotient X
hs : IsClosed s
ha : a ∉ s
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
have rcases : ∀ (a : X) (ha : SeparationQuotient.mk a ∉ s), Disjoint (𝓝ˢ s) (𝓝 (SeparationQuotient.mk a))
Tactic: rcases surjective_mk a with ⟨a, rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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 (𝓝ˢ s) (𝓝 (SeparationQuotient.mk a))
have rw : Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (𝓝 a)
Tactic: rw [← disjoint_comap_iff surjective_mk, comap_mk_nhds_mk, comap_mk_nhdsSet]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ s ⊆ u ∧ closure[inst] u ⊆ t
have this : Disjoint s tᶜ
Tactic: have : Disjoint s tᶜ := Set.disjoint_left.mpr fun x hxs hxt => hxt (hst hxs)
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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ᶜ
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ s ⊆ u ∧ closure[inst] u ⊆ t
have 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
Tactic: rcases normal_separation hs (isClosed_compl_iff.2 ht) this with
    ⟨s', t', hs', ht', hss', htt', hs't'⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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
have refine : s' ⊆ t'ᶜ
Tactic: refine ⟨s', hs', hss', Subset.trans (closure_minimal ?_ (isClosed_compl_iff.2 ht'))
    (compl_subset_comm.1 htt')⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
u s : Set X
h : s ∈ 𝓝ˢ u
hu : IsClosed[inst] u
⊢ ∃ t ∈ 𝓝ˢ u, IsClosed[inst] t ∧ t ⊆ s
have obtain : ∀ (o : Set X) (ho_open : IsOpen[inst] o) (huo : u ⊆ o) (hos : o ⊆ s), ∃ t ∈ 𝓝ˢ u, IsClosed[inst] t ∧ t ⊆ s
Tactic: obtain ⟨o, ho_open, huo, hos⟩ := mem_nhdsSet_iff_exists.mp h
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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
⊢ ∃ t ∈ 𝓝ˢ u, IsClosed[inst] t ∧ t ⊆ s
have obtain : ∀ (v : Set X) (hv_open : IsOpen[inst] v) (huv : u ⊆ v) (hcvo : closure[inst] v ⊆ o),
  ∃ t ∈ 𝓝ˢ u, IsClosed[inst] t ∧ t ⊆ s
Tactic: obtain ⟨v, hv_open, huv, hcvo⟩ := normal_exists_closure_subset hu ho_open huo
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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
have refine : closure[inst] v ∈ 𝓝ˢ u
Tactic: refine ⟨closure v, ?_, isClosed_closure, hcvo.trans hos⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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 s t
have H : 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)
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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 (𝓝ˢ s) (𝓝ˢ t)
have rw : Disjoint (𝓝ˢ (mk ⁻¹' s)) (𝓝ˢ (mk ⁻¹' t))
Tactic: rw [← disjoint_comap_iff surjective_mk, comap_mk_nhdsSet, comap_mk_nhdsSet]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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
have refine : ∀ (s t : Set X) (hd₁ : Disjoint (closure[inst] s) t) (hd₂ : Disjoint s (closure[inst] t)), Disjoint (𝓝ˢ s) (𝓝ˢ t)
Tactic: refine ⟨fun s t hd₁ hd₂ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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 (𝓝ˢ s) (𝓝ˢ t)
have simp : Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))
Tactic: simp only [he.isInducing.nhdsSet_eq_comap]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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)))
have refine_1 : Disjoint (closure[inst_1] (e '' s)) (e '' t)
Tactic: refine disjoint_comap (completely_normal ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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)
⊢ Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))
have refine_2 : Disjoint (e '' s) (closure[inst_1] (e '' t))
Tactic: refine disjoint_comap (completely_normal ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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 (closure[inst_1] (e '' s)) (e '' t)
have refine_1 : e '' t ⊆ (closure[inst_1] (e '' s))ᶜ
Tactic: rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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))ᶜ
⊢ Disjoint (closure[inst_1] (e '' s)) (e '' t)
have refine_1₁ : t ⊆ e ⁻¹' (closure[inst_1] (e '' s))ᶜ
Tactic: rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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))ᶜ
⊢ Disjoint (closure[inst_1] (e '' s)) (e '' t)
have refine_1₂ : t ⊆ (e ⁻¹' closure[inst_1] (e '' s))ᶜ
Tactic: rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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))ᶜ
⊢ Disjoint (closure[inst_1] (e '' s)) (e '' t)
have refine_1₃ : t ⊆ (closure[inst] s)ᶜ
Tactic: rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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 (e '' s) (closure[inst_1] (e '' t))
have refine_2 : 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]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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))ᶜ
⊢ Disjoint (e '' s) (closure[inst_1] (e '' t))
have refine_2₁ : s ⊆ e ⁻¹' (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]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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))ᶜ
⊢ Disjoint (e '' s) (closure[inst_1] (e '' t))
have refine_2₂ : s ⊆ (e ⁻¹' 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]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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))ᶜ
⊢ Disjoint (e '' s) (closure[inst_1] (e '' t))
have refine_2₃ : s ⊆ (closure[inst] t)ᶜ
Tactic: rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl,
      ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ CompletelyNormalSpace X ↔ ∀ (s : Set X), IsOpen[inst] s → NormalSpace.{u_1} (↑s : Type u_1)
have 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)
Tactic: refine ⟨fun _ _ _ => inferInstance, fun h => ⟨fun s t hSt hsT => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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)ᶜ
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have he : IsOpen[inst] e
Tactic: have he : IsOpen e := (isClosed_closure.inter isClosed_closure).isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have h₁ : NormalSpace.{u_1} (↑e : Type u_1)
Tactic: specialize h e he
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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)
have 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
Tactic: rw [disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
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 (𝓝ˢ s) (𝓝ˢ t)
have 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)
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⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
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)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
have 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)
Tactic: obtain ⟨U, V, hU, hV, hsU, htV, hUV⟩ := normal_separation
    (isClosed_closure.preimage continuous_subtype_val)
    (isClosed_closure.preimage continuous_subtype_val) hst