awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
y : Y
hys : y ∉ interior s
hxy : Inseparable (f x) y
⊢ False

Tactic:
hys <| (hxy.mem_open_iff isOpen_interior).1 ?_

Premises used: isOpen_interior, Iff.mp, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
y : Y
hys : y ∉ interior s
hxy : Inseparable (f x) y
refine : f x ∈ interior s
⊢ False

Tactic:
refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_

Premises used: isOpen_interior, Iff.mp, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
y : Y
hys : y ∉ interior s
hxy : Inseparable (f x) y
rwa rwa₁ rwa₂ rwa₃ : s ∈ 𝓝 (f x)
⊢ f x ∈ interior s

Tactic:
rwa [mem_interior_iff_mem_nhds]

Premises used: mem_interior_iff_mem_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
obtain :
  ∀ (U V : Set Y) (Uo : IsOpen[inst_1] U) (Vo : IsOpen[inst_1] V) (hxU : {f x} ⊆ U) (hV : f '' K \ interior s ⊆ V)
    (hd : Disjoint U V), ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s

Tactic:
obtain ⟨U, V, Uo, Vo, hxU, hV, hd⟩ : SeparatedNhds {f x} (f '' K \ interior s) := by
    simp_rw [separatedNhds_iff_disjoint, nhdsSet_singleton, hc.disjoint_nhdsSet_right,
      disjoint_nhds_nhds_iff_not_inseparable]
    rintro y ⟨-, hys⟩ hxy
    refine hys <| (hxy.mem_open_iff isOpen_interior).1 ?_
    rwa [mem_interior_iff_mem_nhds]

Premises used: SDiff.sdiff, interior, SeparatedNhds, Set.image, Singleton.singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s

Tactic:
⟨K \ f ⁻¹' V, diff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩

Premises used: SDiff.sdiff, Filter.diff_mem, Set.preimage, And.intro, IsCompact.diff, Exists.intro, IsOpen.preimage
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
refine_1 : (f ⁻¹' V)ᶜ ∈ 𝓝 x
refine_2 : ∀ (y : X) (hy : y ∈ K \ f ⁻¹' V), f y ∈ s
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s

Tactic:
refine ⟨K \ f ⁻¹' V, diff_mem hKx ?_, hKc.diff <| Vo.preimage hf, fun y hy ↦ ?_⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x_1 : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x_1)
hKc : IsCompact K
hKx : K ∈ 𝓝 x_1
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x_1} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
x : X
hx : x ∈ f ⁻¹' U
⊢ x ∈ (f ⁻¹' V)ᶜ

Tactic:
Set.disjoint_left.1 hd hx

Premises used: Set.Mem, Set.disjoint_left, setOf, Set.preimage, Iff.mp, Not
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
h : ∀ (a : X), Membership.mem (γ := Set X) {x : X | x ∈ f ⁻¹' U → x ∈ (f ⁻¹' V)ᶜ} a
h₁ h₂ : ∀ (x : X) (hx : x ∈ f ⁻¹' U), x ∈ (f ⁻¹' V)ᶜ
⊢ (f ⁻¹' V)ᶜ ∈ 𝓝 x

Tactic:
filter_upwards [hf.continuousAt <| Uo.mem_nhds (hxU rfl)] with x hx
      using Set.disjoint_left.1 hd hx

Premises used: Continuous.continuousAt, IsOpen.mem_nhds, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
y : X
hy : y ∈ K \ f ⁻¹' V
refine_2 : ∀ (hys : f y ∉ s), False
⊢ f y ∈ s

Tactic:
by_contra hys
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
y : X
hy : y ∈ K \ f ⁻¹' V
hys : f y ∉ s
⊢ False

Tactic:
hy.2 (hV ⟨mem_image_of_mem _ hy.1, notMem_subset interior_subset hys⟩)

Premises used: interior_subset, And.right, And.left, Set.mem_image_of_mem, And.intro, Set.notMem_subset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst, inst_1] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
U V : Set Y
Uo : IsOpen[inst_1] U
Vo : IsOpen[inst_1] V
hxU : {f x} ⊆ U
hV : f '' K \ interior s ⊆ V
hd : Disjoint U V
y : X
hy : y ∈ K \ f ⁻¹' V
hys : f y ∉ s
⊢ False

Tactic:
exact hy.2 (hV ⟨mem_image_of_mem _ hy.1, notMem_subset interior_subset hys⟩)

Premises used: interior_subset, And.right, And.left, Set.mem_image_of_mem, And.intro, Set.notMem_subset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
x : X
L : Set X
hLc : IsCompact L
hxL : L ∈ 𝓝 x
⊢ (𝓝 x).HasBasis (fun (K : Set X) ↦ K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed[inst] K) fun (x : Set X) ↦ x

Tactic:
hasBasis_self.2 fun _U hU ↦
    let ⟨K, hKx, hKc, hKU⟩ := exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds
      continuous_id (interior_mem_nhds.2 hU) hLc hxL
    ⟨closure K, mem_of_superset hKx subset_closure, ⟨hKc.closure, isClosed_closure⟩,
      (hKc.closure_subset_of_isOpen isOpen_interior hKU).trans interior_subset⟩

Premises used: Iff.mpr, interior_subset, subset_closure, isOpen_interior, Membership.mem, Exists, nhds, IsCompact.closure, HasSubset.Subset.trans, exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds, HasSubset.Subset, IsClosed, And, continuous_id, closure, IsCompact.closure_subset_of_isOpen, And.intro, Exists.intro, Filter.hasBasis_self, interior_mem_nhds, _private.0.IsCompact.isCompact_isClosed_basis_nhds.match_1, isClosed_closure, IsCompact, Filter.mem_of_superset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
⊢ coclosedCompact X = cocompact X

Tactic:
le_antisymm ?_ cocompact_le_coclosedCompact

Premises used: le_antisymm, Filter.cocompact_le_coclosedCompact
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
refine : coclosedCompact X ≤ cocompact X
⊢ coclosedCompact X = cocompact X

Tactic:
refine le_antisymm ?_ cocompact_le_coclosedCompact

Premises used: le_antisymm, Filter.cocompact_le_coclosedCompact
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
rw : ∀ (i' : Set X), IsCompact i' → ∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ i'ᶜ
⊢ coclosedCompact X ≤ cocompact X

Tactic:
rw [hasBasis_coclosedCompact.le_basis_iff hasBasis_cocompact]

Premises used: Filter.HasBasis.le_basis_iff, Filter.hasBasis_coclosedCompact, Filter.hasBasis_cocompact
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
⊢ ∀ (i' : Set X), IsCompact i' → ∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ i'ᶜ

Tactic:
fun K hK ↦ ⟨closure K, ⟨isClosed_closure, hK.closure⟩, compl_subset_compl.2 subset_closure⟩

Premises used: Iff.mpr, subset_closure, IsCompact.closure, Set.compl_subset_compl, closure, And.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
⊢ ∀ (i' : Set X), IsCompact i' → ∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ i'ᶜ

Tactic:
exact fun K hK ↦ ⟨closure K, ⟨isClosed_closure, hK.closure⟩, compl_subset_compl.2 subset_closure⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
⊢ relativelyCompact X = inCompact X

Tactic:
Bornology.ext _ _ Filter.coclosedCompact_eq_cocompact

Premises used: Bornology.ext, Filter.coclosedCompact_eq_cocompact
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : WeaklyLocallyCompactSpace X
x : X
⊢ (𝓝 x).HasBasis (fun (K : Set X) ↦ K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed[inst] K) fun (x : Set X) ↦ x

Tactic:
let ⟨_L, hLc, hLx⟩ := exists_compact_mem_nhds x
  hLc.isCompact_isClosed_basis_nhds hLx

Premises used: IsCompact.isCompact_isClosed_basis_nhds, WeaklyLocallyCompactSpace.exists_compact_mem_nhds, Membership.mem, nhds, IsClosed, And, Filter.HasBasis, _private.0.instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space.match_1, IsCompact
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : WeaklyLocallyCompactSpace X
x : X
⊢ ∃ K ∈ 𝓝 x, IsCompact K ∧ IsClosed[inst] K

Tactic:
(isCompact_isClosed_basis_nhds x).ex_mem

Premises used: isCompact_isClosed_basis_nhds, Filter.HasBasis.ex_mem
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
x y : X
inst_2 : WeaklyLocallyCompactSpace X
⊢ LocallyCompactSpace X

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

Premises used: _private.0.WeaklyLocallyCompactSpace.locallyCompactSpace.match_1, isCompact_isClosed_basis_nhds, LocallyCompactSpace.of_hasBasis, IsCompact
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
rcases :
  ∀ (K' : Set X) (hK' : IsCompact K') (hKK' : K ⊆ interior K'),
    ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ IsCompact (closure[inst] V)
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ IsCompact (closure[inst] V)

Tactic:
rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩

Premises used: exists_compact_superset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hKK' : K ⊆ interior K'
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ IsCompact (closure[inst] V)

Tactic:
⟨interior K', isOpen_interior, hKK', hK'.closure_of_subset interior_subset⟩

Premises used: interior_subset, isOpen_interior, And.intro, interior, Exists.intro, IsCompact.closure_of_subset
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hKK' : K ⊆ interior K'
⊢ ∃ (V : Set X), IsOpen[inst] V ∧ K ⊆ V ∧ IsCompact (closure[inst] V)

Tactic:
exact ⟨interior K', isOpen_interior, hKK', hK'.closure_of_subset interior_subset⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : WeaklyLocallyCompactSpace X
x : X
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ IsCompact (closure[inst] U)

Tactic:
simpa only [singleton_subset_iff]
    using exists_isOpen_superset_and_isCompact_closure isCompact_singleton

Premises used: Set.singleton_subset_iff, isCompact_singleton, exists_isOpen_superset_and_isCompact_closure
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
simp_rw :
  Eq (α := Prop)
    (∀ (x : X) (x_1 : Set X),
      IsOpen[inst] x_1 → x ∈ x_1 → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ)
    (∀ (x : X) (x_1 : Set X),
      IsOpen[inst] x_1 → x ∈ x_1 → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ)
⊢ CompletelyRegularSpace X =
    ∀ (x : X) (x_1 : Set X),
      IsOpen[inst] x_1 → x ∈ x_1 → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ

Tactic:
simp_rw +singlePass [completelyRegularSpace_iff, compl_surjective.forall, isClosed_compl_iff,
      mem_compl_iff, not_not]

Premises used: Function.Surjective.forall, Classical.not_not, compl_surjective, completelyRegularSpace_iff, Set.mem_compl_iff, isClosed_compl_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
tactic :
  ∀ (x : X) (x_1 : Set X),
    IsOpen[inst] x_1 → x ∈ x_1 → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ
| CompletelyRegularSpace X

Tactic:
tactic =>
    simp_rw +singlePass [completelyRegularSpace_iff, compl_surjective.forall, isClosed_compl_iff,
      mem_compl_iff, not_not]

Premises used: Function.Surjective.forall, Classical.not_not, compl_surjective, completelyRegularSpace_iff, Set.mem_compl_iff, isClosed_compl_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
conv_lhs :
  CompletelyRegularSpace X ↔
    ∀ (x : X) (K : Set X),
      IsOpen[inst] K → x ∈ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
conv_lhs₁ :
  (∀ (x : X) (x_1 : Set X),
      IsOpen[inst] x_1 → x ∈ x_1 → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ) ↔
    ∀ (x : X) (K : Set X),
      IsOpen[inst] K → x ∈ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
⊢ CompletelyRegularSpace X ↔
    ∀ (x : X) (K : Set X),
      IsOpen[inst] K → x ∈ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ

Tactic:
conv_lhs => tactic =>
    simp_rw +singlePass [completelyRegularSpace_iff, compl_surjective.forall, isClosed_compl_iff,
      mem_compl_iff, not_not]

Premises used: Function.Surjective.forall, Classical.not_not, compl_surjective, completelyRegularSpace_iff, Set.mem_compl_iff, isClosed_compl_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
⊢ ∀ (x : X) (K : Set X), IsOpen[inst] K → x ∈ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ

Tactic:
completelyRegularSpace_iff_isOpen.mp inferInstance

Premises used: completelyRegularSpace_iff_isOpen, inferInstance, Iff.mp
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
rw : ∀ {s : Set X} {a : X}, IsClosed[inst] s → a ∉ s → Disjoint (𝓝ˢ s) (𝓝 a)
⊢ RegularSpace X

Tactic:
rw [regularSpace_iff]

Premises used: regularSpace_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
s : Set X
a : X
hs : IsClosed[inst] s
ha : a ∉ s
obtain : ∀ (f : X → (↑I : Type)) (cf : Continuous[inst, _] f) (hf : f a = 0) (hhf : EqOn f 1 s), Disjoint (𝓝ˢ s) (𝓝 a)
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
obtain ⟨f, cf, hf, hhf⟩ := CompletelyRegularSpace.completely_regular a s hs ha

Premises used: CompletelyRegularSpace.completely_regular
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
s : Set X
a : X
hs : IsClosed[inst] s
ha : a ∉ s
f : X → (↑I : Type)
cf : Continuous[inst, _] f
hf : f a = 0
hhf : EqOn f 1 s
apply : Disjoint (map f (𝓝ˢ s)) (map f (𝓝 a))
⊢ Disjoint (𝓝ˢ s) (𝓝 a)

Tactic:
apply disjoint_of_map (f := f)

Premises used: Filter.disjoint_of_map
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
s : Set X
a : X
hs : IsClosed[inst] s
ha : a ∉ s
f : X → (↑I : Type)
cf : Continuous[inst, _] f
hf : f a = 0
hhf : EqOn f 1 s
apply : Disjoint (𝓝 (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) 1 ⋯)) (𝓝 (f a))
⊢ Disjoint (map f (𝓝ˢ s)) (map f (𝓝 a))

Tactic:
apply Disjoint.mono (cf.tendsto_nhdsSet_nhds hhf) cf.continuousAt

Premises used: Continuous.tendsto_nhdsSet_nhds, Continuous.continuousAt, Disjoint.mono
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
s : Set X
a : X
hs : IsClosed[inst] s
ha : a ∉ s
f : X → (↑I : Type)
cf : Continuous[inst, _] f
hf : f a = 0
hhf : EqOn f 1 s
⊢ Disjoint (𝓝 (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) 1 ⋯)) (𝓝 (f a))

Tactic:
disjoint_nhds_nhds.mpr (hf.symm ▸ zero_ne_one).symm

Premises used: Iff.mpr, disjoint_nhds_nhds
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
s : Set X
a : X
hs : IsClosed[inst] s
ha : a ∉ s
f : X → (↑I : Type)
cf : Continuous[inst, _] f
hf : f a = 0
hhf : EqOn f 1 s
⊢ Disjoint (𝓝 (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) 1 ⋯)) (𝓝 (f a))

Tactic:
exact disjoint_nhds_nhds.mpr (hf.symm ▸ zero_ne_one).symm

Premises used: Iff.mpr, disjoint_nhds_nhds
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
rw :
  ∀ (x : X) (K : Set X),
    IsClosed[inst] K → x ∉ K → ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
⊢ CompletelyRegularSpace X

Tactic:
rw [completelyRegularSpace_iff]

Premises used: completelyRegularSpace_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
⊢ IsClosed[inst] (closure[inst] {x})

Tactic:
have cx : IsClosed (closure {x}) := isClosed_closure
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
rw : closure[inst] {x} ∩ K ⊆ ∅
⊢ Disjoint (closure[inst] {x}) K

Tactic:
rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
a : X
this : ∀ (hax : Membership.mem (γ := Set X) (closure[inst] {x}) a) (haK : a ∈ K), Membership.mem (γ := Set X) ∅ a
⊢ a ∈ closure[inst] {x} ∩ K → Membership.mem (γ := Set X) ∅ a

Tactic:
⟨hax, haK⟩
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
a : X
hax : Membership.mem (γ := Set X) (closure[inst] {x}) a
haK : a ∈ K
⊢ Membership.mem (γ := Set X) ∅ a

Tactic:
hx ((specializes_iff_mem_closure.mpr hax).symm.mem_closed hK haK)

Premises used: Iff.mpr, Specializes.symm, Set.Mem, specializes_iff_mem_closure, Specializes.mem_closed
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
a : X
hax : Membership.mem (γ := Set X) (closure[inst] {x}) a
haK : a ∈ K
⊢ Membership.mem (γ := Set X) ∅ a

Tactic:
exact hx ((specializes_iff_mem_closure.mpr hax).symm.mem_closed hK haK)

Premises used: Iff.mpr, Specializes.symm, specializes_iff_mem_closure, Specializes.mem_closed
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
⊢ Disjoint (closure[inst] {x}) K

Tactic:
have d : Disjoint (closure {x}) K := by
    rw [Set.disjoint_iff]
    intro a ⟨hax, haK⟩
    exact hx ((specializes_iff_mem_closure.mpr hax).symm.mem_closed hK haK)
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
d : Disjoint (closure[inst] {x}) K
let :
  ∀ (f : X → ℝ) (cf : Continuous[inst, _] f)
    (hfx :
      EqOn (α := X) (β := ℝ) (⇑{ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) 0 (closure[inst] {x}))
    (hfK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) 1 K)
    (hficc :
      ∀ (x : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
          (({ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)),
    ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K

Tactic:
let ⟨⟨f, cf⟩, hfx, hfK, hficc⟩ := exists_continuous_zero_one_of_isClosed cx hK d
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
d : Disjoint (closure[inst] {x}) K
f : X → ℝ
cf : Continuous[inst, _] f
hfx : EqOn (α := X) (β := ℝ) (⇑{ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) 0 (closure[inst] {x})
hfK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) 1 K
hficc :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
g : X → (↑I : Type) := fun (x : X) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (f x) ⋯
⊢ Continuous[inst, _] g

Tactic:
have cg : Continuous g := cf.subtype_mk hficc
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
inst_2 : R0Space X
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
cx : IsClosed[inst] (closure[inst] {x})
d : Disjoint (closure[inst] {x}) K
f : X → ℝ
cf : Continuous[inst, _] f
hfx : EqOn (α := X) (β := ℝ) (⇑{ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) 0 (closure[inst] {x})
hfK : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) 1 K
hficc :
  ∀ (x : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
      (({ toFun := f, continuous_toFun := cf : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)
g : X → (↑I : Type) := fun (x : X) ↦ Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (f x) ⋯
cg : Continuous[inst, _] g
⊢ g x = 0

Tactic:
have hgx : g x = 0 := Subtype.ext (hfx (subset_closure (mem_singleton x)))