awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst] U
a :
  ∀ (f : X → (↑I : Type)) (hf : Continuous[inst, _] f) (efx : f x = 0) (hfU : EqOn f 1 Uᶜ),
    ∃ (i : Set (StoneCech X)), stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U
⊢ ∃ (i : Set (StoneCech X)), stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U

Tactic:
obtain ⟨f, hf, efx, hfU⟩ :=
      CompletelyRegularSpace.completely_regular_isOpen x U hU hxU

Premises used: CompletelyRegularSpace.completely_regular_isOpen
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst] U
f : X → (↑I : Type)
hf : Continuous[inst, _] f
efx : f x = 0
hfU : EqOn f 1 Uᶜ
⊢ EqOn f 1 Uᶜ = (Uᶜ ⊆ f ⁻¹' {1})

Tactic:
simp [EqOn, subset_def]

Premises used: Set.subset_def, Set.EqOn
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst] U
f : X → (↑I : Type)
hf : Continuous[inst, _] f
efx : f x = 0
hfU : EqOn f 1 Uᶜ
⊢ Uᶜ ⊆ f ⁻¹' {1}

Tactic:
conv at hfU => equals Uᶜ ⊆ f ⁻¹' {1} => simp [EqOn, subset_def]

Premises used: Set.subset_def, Set.EqOn
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst] U
f : X → (↑I : Type)
hf : Continuous[inst, _] f
efx : f x = 0
hfU : Uᶜ ⊆ f ⁻¹' {1}
⊢ stoneCechUnit ⁻¹' stoneCechExtend hf ⁻¹' {1}ᶜ ⊆ U

Tactic:
rw [← compl_subset_comm, ← preimage_compl, ← stoneCechExtend_extends hf, preimage_comp] at hfU

Premises used: Set.compl_subset_comm, Set.preimage_comp, stoneCechExtend_extends, Set.preimage_compl
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst] U
f : X → (↑I : Type)
hf : Continuous[inst, _] f
efx : f x = 0
hfU : stoneCechUnit ⁻¹' stoneCechExtend hf ⁻¹' {1}ᶜ ⊆ U
⊢ ∃ (i : Set (StoneCech X)), stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U

Tactic:
⟨stoneCechExtend hf ⁻¹' {1}ᶜ, ?_,
      isOpen_compl_singleton.preimage (continuous_stoneCechExtend hf), hfU⟩

Premises used: Compl.compl, isOpen_compl_singleton, continuous_stoneCechExtend, Set.preimage, And.intro, Exists.intro, Singleton.singleton, OfNat.ofNat, IsOpen.preimage, stoneCechExtend
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst] U
f : X → (↑I : Type)
hf : Continuous[inst, _] f
efx : f x = 0
hfU : stoneCechUnit ⁻¹' stoneCechExtend hf ⁻¹' {1}ᶜ ⊆ U
a : stoneCechUnit x ∈ stoneCechExtend hf ⁻¹' {1}ᶜ
⊢ ∃ (i : Set (StoneCech X)), stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U

Tactic:
refine ⟨stoneCechExtend hf ⁻¹' {1}ᶜ, ?_,
      isOpen_compl_singleton.preimage (continuous_stoneCechExtend hf), hfU⟩
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst] U
f : X → (↑I : Type)
hf : Continuous[inst, _] f
efx : f x = 0
hfU : stoneCechUnit ⁻¹' stoneCechExtend hf ⁻¹' {1}ᶜ ⊆ U
a : ¬Eq (α := (↑I : Type)) 0 1
⊢ stoneCechUnit x ∈ stoneCechExtend hf ⁻¹' {1}ᶜ

Tactic:
rw [mem_preimage, stoneCechExtend_stoneCechUnit, efx, mem_compl_iff, mem_singleton_iff]

Premises used: Set.mem_singleton_iff, stoneCechExtend_stoneCechUnit, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst] U
f : X → (↑I : Type)
hf : Continuous[inst, _] f
efx : f x = 0
hfU : stoneCechUnit ⁻¹' stoneCechExtend hf ⁻¹' {1}ᶜ ⊆ U
⊢ ¬Eq (α := (↑I : Type)) 0 1

Tactic:
simp
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis.{u} (α := X) {s : Set X | IsClopen s}
x : X
K : Set X
hK : IsClosed[inst] K
hx : x ∉ K
obtain :
  ∀ (s : Set X) (hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} s) (hx : x ∈ s) (hsK : s ⊆ Kᶜ),
    ∃ (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:
obtain ⟨s, hs, hx, hsK⟩ := h.exists_subset_of_mem_open hx hK.isOpen_compl

Premises used: IsClosed.isOpen_compl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis.{u} (α := X) {s : Set X | IsClopen s}
x : X
K : Set X
hK : IsClosed[inst] K
hx_1 : x ∉ K
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} s
hx : x ∈ s
hsK : s ⊆ Kᶜ
⊢ Eq (α := (↑I : Type)) (sᶜ.indicator 1 x) 0

Tactic:
simpa
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis.{u} (α := X) {s : Set X | IsClopen s}
x : X
K : Set X
hK : IsClosed[inst] K
hx_1 : x ∉ K
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} s
hx : x ∈ s
hsK : s ⊆ Kᶜ
refine_1 : Continuous[inst, _] (sᶜ.indicator 1)
refine_2 : ∀ (x : X) (hx : x ∈ K), x ∈ sᶜ
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K

Tactic:
refine ⟨sᶜ.indicator 1, ?_, by simpa, fun x hx ↦ indicator_of_mem ?_ _⟩
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis.{u} (α := X) {s : Set X | IsClopen s}
x : X
K : Set X
hK : IsClosed[inst] K
hx_1 : x ∉ K
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} s
hx : x ∈ s
hsK : s ⊆ Kᶜ
⊢ Continuous[inst, _] (sᶜ.indicator 1)

Tactic:
hs.compl.continuous_indicator continuous_const

Premises used: continuous_const, IsClopen.compl, IsClopen.continuous_indicator
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis.{u} (α := X) {s : Set X | IsClopen s}
x : X
K : Set X
hK : IsClosed[inst] K
hx_1 : x ∉ K
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} s
hx : x ∈ s
hsK : s ⊆ Kᶜ
⊢ Continuous[inst, _] (sᶜ.indicator 1)

Tactic:
exact hs.compl.continuous_indicator continuous_const

Premises used: continuous_const, IsClopen.compl, IsClopen.continuous_indicator
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis.{u} (α := X) {s : Set X | IsClopen s}
x_1 : X
K : Set X
hK : IsClosed[inst] K
hx_1 : x_1 ∉ K
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} s
hx_2 : x_1 ∈ s
hsK : s ⊆ Kᶜ
x : X
hx : x ∈ K
⊢ x ∈ sᶜ

Tactic:
(mem_compl_iff s x).mpr fun hs ↦ hsK hs hx

Premises used: Iff.mpr, Set.mem_compl_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis.{u} (α := X) {s : Set X | IsClopen s}
x_1 : X
K : Set X
hK : IsClosed[inst] K
hx_1 : x_1 ∉ K
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} s
hx_2 : x_1 ∈ s
hsK : s ⊆ Kᶜ
x : X
hx : x ∈ K
⊢ x ∈ sᶜ

Tactic:
exact (mem_compl_iff s x).mpr fun hs ↦ hsK hs hx

Premises used: Iff.mpr, Set.mem_compl_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
⊢ IsTopologicalBasis.{u} (α := X) {s : Set X | IsClopen s}

Tactic:
isTopologicalBasis_of_isOpen_of_nhds (fun x s ↦ IsClopen.isOpen s) (fun x s hxs hs ↦ ?_)

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, IsClopen.isOpen
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
refine :
  ∀ (x : X) (s : Set X) (hxs : x ∈ s) (hs : IsOpen[inst] s),
    ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
⊢ IsTopologicalBasis.{u} (α := X) {s : Set X | IsClopen s}

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds (fun x s ↦ IsClopen.isOpen s) (fun x s hxs hs ↦ ?_)

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, IsClopen.isOpen
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
choose :
  ∀ (f : X → (↑I : Type)) (hf : Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 sᶜ),
    ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s

Tactic:
choose f hf using completely_regular_isOpen x s hs hxs

Premises used: CompletelyRegularSpace.completely_regular_isOpen
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hf : Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 sᶜ
⊢ Continuous[inst, _] f

Tactic:
obtain ⟨hfc, hf₀, hf₁⟩ := hf
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hf : Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 sᶜ
hfc : Continuous[inst, _] f
⊢ f x = 0

Tactic:
obtain ⟨hfc, hf₀, hf₁⟩ := hf
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hf : Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 sᶜ
hfc : Continuous[inst, _] f
hf₀ : f x = 0
⊢ EqOn f 1 sᶜ

Tactic:
obtain ⟨hfc, hf₀, hf₁⟩ := hf
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
⊢ lift.{u, 0} #(↑R : Type) < lift.{0, u} 𝔠

Tactic:
simpa [R] using mk_range_le_lift.trans_lt (lift_strictMono hX)

Premises used: Cardinal.lift_strictMono, LE.le.trans_lt, Cardinal.mk_range_le_lift
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
⊢ lift.{u, 0} #(↑R : Type) < lift.{0, u} 𝔠

Tactic:
have hR : lift.{u, 0} (Cardinal.mk R) < lift.{0, u} continuum := by
    simpa [R] using mk_range_le_lift.trans_lt (lift_strictMono hX)
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : lift.{u, 0} #(↑R : Type) < lift.{0, u} 𝔠
⊢ #(↑R : Type) < #(↑I : Type)

Tactic:
rw [lift_continuum, ← lift_continuum.{u, 0}, lift_lt, ← mk_Icc_real zero_lt_one, ← unitInterval]
    at hR

Premises used: Cardinal.mk_Icc_real, Cardinal.lift_lt, zero_lt_one, unitInterval, Cardinal.lift_continuum
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
⊢ ∃ (r : (↑I : Type)), r ∈ Rᶜ

Tactic:
compl_nonempty_of_mk_lt_mk hR

Premises used: Cardinal.compl_nonempty_of_mk_lt_mk, Set.Nonempty
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
obtain :
  ∀ (r : (↑I : Type)) (hr : r ∈ Rᶜ),
    ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s

Tactic:
obtain ⟨r, hr⟩ : ∃ r : I, r ∈ Rᶜ := compl_nonempty_of_mk_lt_mk hR

Premises used: Cardinal.compl_nonempty_of_mk_lt_mk
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
⊢ ∀ (x : X), f x ≠ r

Tactic:
simpa [R] using hr
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
⊢ ∀ (x : X), f x ≠ r

Tactic:
have hr' : ∀ (x : X), f x ≠ r := by simpa [R] using hr
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
h : ∀ (x : X), x ∈ f ⁻¹' Iio r ↔ x ∈ f ⁻¹' Iic r
⊢ f ⁻¹' Iio r = f ⁻¹' Iic r

Tactic:
ext
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
x_1 : X
⊢ x_1 ∈ f ⁻¹' Iio r ↔ x_1 ∈ f ⁻¹' Iic r

Tactic:
simp [le_iff_lt_or_eq, hr']

Premises used: le_iff_lt_or_eq
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
⊢ f ⁻¹' Iio r = f ⁻¹' Iic r

Tactic:
have hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r := by
    ext; simp [le_iff_lt_or_eq, hr']
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s

Tactic:
⟨f ⁻¹' Iio r, ⟨hrclopen ▸ isClosed_Iic.preimage hfc, isOpen_Iio.preimage hfc⟩, ?_, ?_⟩

Premises used: Eq.rec, isOpen_Iio, isClosed_Iic, Set.preimage, And.intro, Exists.intro, IsClosed.preimage, IsOpen.preimage, Eq.symm, Set.Iio
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
refine_1 : x ∈ f ⁻¹' Iio r
refine_2 : f ⁻¹' Iio r ⊆ s
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s

Tactic:
refine ⟨f ⁻¹' Iio r, ⟨hrclopen ▸ isClosed_Iic.preimage hfc, isOpen_Iio.preimage hfc⟩, ?_, ?_⟩
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ x ∈ f ⁻¹' Iio r

Tactic:
simp [hf₀, hrclopen]
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
⊢ f ⁻¹' Iio r ⊆ s

Tactic:
preimage_subset_iff.mpr (fun x ↦ ?_)

Premises used: Iff.mpr, Set.preimage_subset_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
refine_2 : ∀ (x : X), f x ∈ Iio r → x ∈ s
⊢ f ⁻¹' Iio r ⊆ s

Tactic:
refine preimage_subset_iff.mpr (fun x ↦ ?_)

Premises used: Iff.mpr, Set.preimage_subset_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x_1 : X
s : Set X
hxs : x_1 ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x_1 = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
x : X
refine_2 : x ∉ s → f x ∉ Iio r
⊢ f x ∈ Iio r → x ∈ s

Tactic:
contrapose
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
x_1 : X
s : Set X
hxs_1 : x_1 ∈ s
hs : IsOpen[inst] s
f : X → (↑I : Type)
hfc : Continuous[inst, _] f
hf₀ : f x_1 = 0
hf₁ : EqOn f 1 sᶜ
R : Set (↑I : Type) := range f
hR : #(↑R : Type) < #(↑I : Type)
r : (↑I : Type)
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
hrclopen : f ⁻¹' Iio r = f ⁻¹' Iic r
x : X
hxs : x ∉ s
⊢ f x ∉ Iio r

Tactic:
simpa [hf₁ hxs] using le_one'

Premises used: unitInterval.le_one'
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : T35Space Y
f : X → Y
hf : IsEmbedding f
⊢ T35Space X

Tactic:
@T35Space.mk _ _ hf.t0Space hf.isInducing.completelyRegularSpace

Premises used: T35Space.mk
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
x y : X
x_ne_y : x ≠ y
obtain :
  ∀ (f : X → (↑I : Type)) (f_cont : Continuous[inst, _] f) (f_zero : f x = 0) (f_one : EqOn f 1 {y}),
    ∃ (f : X → ℝ), Membership.mem (γ := Set (X → ℝ)) {f : X → ℝ | Continuous[inst, _] f} f ∧ f x ≠ f y
⊢ ∃ (f : X → ℝ), Membership.mem (γ := Set (X → ℝ)) {f : X → ℝ | Continuous[inst, _] f} f ∧ f x ≠ f y

Tactic:
obtain ⟨f, f_cont, f_zero, f_one⟩ :=
    CompletelyRegularSpace.completely_regular x {y} isClosed_singleton x_ne_y

Premises used: CompletelyRegularSpace.completely_regular, Singleton.singleton, isClosed_singleton
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → (↑I : Type)
f_cont : Continuous[inst, _] f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ Ne (α := ℝ) ((fun (x : X) ↦ (↑(f x) : ℝ)) x) ((fun (x : X) ↦ (↑(f x) : ℝ)) y)

Tactic:
simp_all
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → (↑I : Type)
f_cont : Continuous[inst, _] f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ ∃ (f : X → ℝ), Membership.mem (γ := Set (X → ℝ)) {f : X → ℝ | Continuous[inst, _] f} f ∧ f x ≠ f y

Tactic:
exact ⟨fun x ↦ f x, continuous_subtype_val.comp f_cont, by simp_all⟩
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
x y : X
x_ne_y : x ≠ y
obtain :
  ∀ (f : X → (↑I : Type)) (f_cont : Continuous[inst, _] f) (f_zero : f x = 0) (f_one : EqOn f 1 {y}),
    ∃ (f : X → (↑I : Type)),
      Membership.mem (γ := Set (X → (↑I : Type))) {f : X → (↑I : Type) | Continuous[inst, _] f} f ∧ f x ≠ f y
⊢ ∃ (f : X → (↑I : Type)),
    Membership.mem (γ := Set (X → (↑I : Type))) {f : X → (↑I : Type) | Continuous[inst, _] f} f ∧ f x ≠ f y

Tactic:
obtain ⟨f, f_cont, f_zero, f_one⟩ :=
    CompletelyRegularSpace.completely_regular x {y} isClosed_singleton x_ne_y

Premises used: CompletelyRegularSpace.completely_regular, Singleton.singleton, isClosed_singleton
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → (↑I : Type)
f_cont : Continuous[inst, _] f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ f x ≠ f y

Tactic:
simp_all
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → (↑I : Type)
f_cont : Continuous[inst, _] f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ ∃ (f : X → (↑I : Type)),
    Membership.mem (γ := Set (X → (↑I : Type))) {f : X → (↑I : Type) | Continuous[inst, _] f} f ∧ f x ≠ f y

Tactic:
exact ⟨f, f_cont, by simp_all⟩
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
a b : X
hab : Eq (α := StoneCech X) (stoneCechUnit a) (stoneCechUnit b)
contrapose : ∀ (hab : ¬a = b), ¬Eq (α := StoneCech X) (stoneCechUnit a) (stoneCechUnit b)
⊢ a = b

Tactic:
contrapose hab
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
a b : X
hab : ¬a = b
obtain :
  ∀ (f : X → (↑I : Type))
    (fc : Membership.mem (γ := Set (X → (↑I : Type))) {f : X → (↑I : Type) | Continuous[inst, _] f} f)
    (fab : f a ≠ f b), ¬Eq (α := StoneCech X) (stoneCechUnit a) (stoneCechUnit b)
⊢ ¬Eq (α := StoneCech X) (stoneCechUnit a) (stoneCechUnit b)

Tactic:
obtain ⟨f, fc, fab⟩ := separatesPoints_continuous_of_t35Space_Icc hab

Premises used: separatesPoints_continuous_of_t35Space_Icc
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
a b : X
hab : ¬a = b
f : X → (↑I : Type)
fc : Membership.mem (γ := Set (X → (↑I : Type))) {f : X → (↑I : Type) | Continuous[inst, _] f} f
fab : f a ≠ f b
⊢ ¬Eq (α := StoneCech X) (stoneCechUnit a) (stoneCechUnit b)

Tactic:
fun q ↦ fab (eq_if_stoneCechUnit_eq fc q)

Premises used: eq_if_stoneCechUnit_eq, Not
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T35Space X
a b : X
hab : ¬a = b
f : X → (↑I : Type)
fc : Membership.mem (γ := Set (X → (↑I : Type))) {f : X → (↑I : Type) | Continuous[inst, _] f} f
fab : f a ≠ f b
⊢ ¬Eq (α := StoneCech X) (stoneCechUnit a) (stoneCechUnit b)

Tactic:
exact fun q ↦ fab (eq_if_stoneCechUnit_eq fc q)

Premises used: eq_if_stoneCechUnit_eq