awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hgx : g x = 0
⊢ EqOn g 1 K

Tactic:
have hgK : EqOn g 1 K := fun k hk => Subtype.ext (hfK hk)
-- 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
hgx : g x = 0
hgK : EqOn g 1 K
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K

Tactic:
⟨g, cg, hgx, hgK⟩

Premises used: And.intro, Exists.intro
-- 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
hgx : g x = 0
hgK : EqOn g 1 K
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K

Tactic:
exact ⟨g, cg, hgx, hgK⟩
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set X
hK : IsClosed[inst] K
hxK : x ∉ K
⊢ ∃ (t : Set Y), IsClosed[inst_1] t ∧ f ⁻¹' t = K

Tactic:
rw [hf.isClosed_iff] at hK

Premises used: Topology.IsInducing.isClosed_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set X
hK : IsClosed[inst] K
hxK : x ∉ K
hK₁ : ∃ (t : Set Y), IsClosed[inst_1] t ∧ f ⁻¹' t = K
⊢ x ∉ K

Tactic:
rw [hf.isClosed_iff] at hK

Premises used: Topology.IsInducing.isClosed_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set X
hK : ∃ (t : Set Y), IsClosed[inst_1] t ∧ f ⁻¹' t = K
hxK : x ∉ K
obtain :
  ∀ (K : Set Y) (hK : IsClosed[inst_1] K) (hxK : x ∉ f ⁻¹' K),
    ∃ (f_1 : X → (↑I : Type)), Continuous[inst, _] f_1 ∧ f_1 x = 0 ∧ EqOn f_1 1 (f ⁻¹' K)
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K

Tactic:
obtain ⟨K, hK, rfl⟩ := hK

Premises used: rfl
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst_1] K
hxK : x ∉ f ⁻¹' K
⊢ f x ∉ K

Tactic:
rw [mem_preimage] at hxK

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst_1] K
hxK : f x ∉ K
obtain :
  ∀ (g : Y → (↑I : Type)) (hcf : Continuous[inst_1, _] g) (egfx : g (f x) = 0) (hgK : EqOn g 1 K),
    ∃ (f_1 : X → (↑I : Type)), Continuous[inst, _] f_1 ∧ f_1 x = 0 ∧ EqOn f_1 1 (f ⁻¹' K)
⊢ ∃ (f_1 : X → (↑I : Type)), Continuous[inst, _] f_1 ∧ f_1 x = 0 ∧ EqOn f_1 1 (f ⁻¹' K)

Tactic:
obtain ⟨g, hcf, egfx, hgK⟩ := CompletelyRegularSpace.completely_regular _ _ hK hxK

Premises used: CompletelyRegularSpace.completely_regular
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst_1] K
hxK : f x ∉ K
g : Y → (↑I : Type)
hcf : Continuous[inst_1, _] g
egfx : g (f x) = 0
hgK : EqOn g 1 K
⊢ ∃ (f_1 : X → (↑I : Type)), Continuous[inst, _] f_1 ∧ f_1 x = 0 ∧ EqOn f_1 1 (f ⁻¹' K)

Tactic:
⟨g ∘ f, hcf.comp hf.continuous, egfx, ?_⟩

Premises used: Continuous.comp, Function.comp, And.intro, Exists.intro, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst_1] K
hxK : f x ∉ K
g : Y → (↑I : Type)
hcf : Continuous[inst_1, _] g
egfx : g (f x) = 0
hgK : EqOn g 1 K
refine : EqOn (g ∘ f) 1 (f ⁻¹' K)
⊢ ∃ (f_1 : X → (↑I : Type)), Continuous[inst, _] f_1 ∧ f_1 x = 0 ∧ EqOn f_1 1 (f ⁻¹' K)

Tactic:
refine ⟨g ∘ f, hcf.comp hf.continuous, egfx, ?_⟩
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst_1] K
hxK : f x ∉ K
g : Y → (↑I : Type)
hcf : Continuous[inst_1, _] g
egfx : g (f x) = 0
hgK : EqOn g 1 K
arg : 1
| EqOn (g ∘ f) 1 (f ⁻¹' K)

Tactic:
arg 2
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst_1] K
hxK : f x ∉ K
g : Y → (↑I : Type)
hcf : Continuous[inst_1, _] g
egfx : g (f x) = 0
hgK : EqOn g 1 K
⊢ Eq (α := X → (↑I : Type)) 1 (1 ∘ f)

Tactic:
rfl
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst_1] K
hxK : f x ∉ K
g : Y → (↑I : Type)
hcf : Continuous[inst_1, _] g
egfx : g (f x) = 0
hgK : EqOn g 1 K
arg arg₁ : 1
| EqOn (g ∘ f) 1 (f ⁻¹' K)

Tactic:
arg 2; equals (1 : Y → ↥I) ∘ f => rfl

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst_1] K
hxK : f x ∉ K
g : Y → (↑I : Type)
hcf : Continuous[inst_1, _] g
egfx : g (f x) = 0
hgK : EqOn g 1 K
⊢ EqOn (g ∘ f) (1 ∘ f) (f ⁻¹' K)

Tactic:
hgK.comp_right <| mapsTo_preimage _ _

Premises used: Set.EqOn.comp_right, Set.mapsTo_preimage
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
inst_1 : TopologicalSpace Y
inst_2 : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set Y
hK : IsClosed[inst_1] K
hxK : f x ∉ K
g : Y → (↑I : Type)
hcf : Continuous[inst_1, _] g
egfx : g (f x) = 0
hgK : EqOn g 1 K
⊢ EqOn (g ∘ f) (1 ∘ f) (f ⁻¹' K)

Tactic:
exact hgK.comp_right <| mapsTo_preimage _ _

Premises used: Set.EqOn.comp_right, Set.mapsTo_preimage
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
inst_1 : CompletelyRegularSpace X
⊢ CompletelyRegularSpace.{u} (Subtype p)

Tactic:
Topology.IsInducing.subtypeVal.completelyRegularSpace

Premises used: Topology.IsInducing.completelyRegularSpace, Set.Mem, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u_1
Y : Type u_2
t : TopologicalSpace Y
ht : CompletelyRegularSpace Y
f : X → Y
⊢ CompletelyRegularSpace X

Tactic:
@IsInducing.completelyRegularSpace _ (t.induced f) _ t _ _ (IsInducing.induced f)

Premises used: Topology.IsInducing.completelyRegularSpace, Topology.IsInducing.induced
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
rw :
  ∀ (x : X) (K : Set X),
    IsOpen[⨅ (i : ι), t i] K → x ∈ K → ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
⊢ CompletelyRegularSpace X

Tactic:
rw [completelyRegularSpace_iff_isOpen]

Premises used: completelyRegularSpace_iff_isOpen
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
K : Set X
hK : IsOpen[⨅ (i : ι), t i] K
hxK : x ∈ K
⊢ ∃ (s : Finset ι) (V : ↥s → Set X), (∀ (i : ↥s), V i ∈ 𝓝 x) ∧ K = ⋂ (i : ↥s), V i

Tactic:
simp_rw [← hK.mem_nhds_iff, nhds_iInf, mem_iInf, exists_finite_iff_finset,
    Finset.coe_sort_coe] at hxK

Premises used: Finset.coe_sort_coe, Filter.mem_iInf, nhds_iInf, IsOpen.mem_nhds_iff, Set.exists_finite_iff_finset
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
K : Set X
hxK : ∃ (s : Finset ι) (V : ↥s → Set X), (∀ (i : ↥s), V i ∈ 𝓝 x) ∧ K = ⋂ (i : ↥s), V i
obtain :
  ∀ (I' : Finset ι) (V : ↥I' → Set X) (hV : ∀ (i : ↥I'), V i ∈ 𝓝 x),
    ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ

Tactic:
obtain ⟨I', V, hV, rfl⟩ := hxK

Premises used: rfl
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V : ↥I' → Set X
hV : ∀ (i : ↥I'), V i ∈ 𝓝 x
⊢ ∀ (i : ↥I'), ∃ t_1 ⊆ V i, IsOpen[t (↑i : ι)] t_1 ∧ x ∈ t_1

Tactic:
simp only [mem_nhds_iff] at hV

Premises used: mem_nhds_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V : ↥I' → Set X
hV : ∀ (i : ↥I'), ∃ t_1 ⊆ V i, IsOpen[t (↑i : ι)] t_1 ∧ x ∈ t_1
choose :
  ∀ (U : (i : ↥I') → Set X) (hUV : ∀ (i : ↥I'), U i ⊆ V i) (hU : ∀ (i : ↥I'), IsOpen[t (↑i : ι)] (U i))
    (hxU : ∀ (i : ↥I'), x ∈ U i),
    ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ

Tactic:
choose U hUV hU hxU using hV
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
hU : ∀ (i : ↥I'), IsOpen[t (↑i : ι)] (U i)
hxU : ∀ (i : ↥I'), x ∈ U i
⊢ ∀ (i : ↥I'), ∃ (f : X → (↑I : Type)), Continuous[t (↑i : ι), _] f ∧ f x = 0 ∧ EqOn f 1 (U i)ᶜ

Tactic:
replace hU := fun (i : ↥I') =>
    @CompletelyRegularSpace.completely_regular_isOpen _ (t i) (ht i) x (U i) (hU i) (hxU i)
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
hU : ∀ (i : ↥I'), ∃ (f : X → (↑I : Type)), Continuous[t (↑i : ι), _] f ∧ f x = 0 ∧ EqOn f 1 (U i)ᶜ
choose :
  ∀ (fs : (i : ↥I') → X → (↑I : Type)) (hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i))
    (hxfs : ∀ (i : ↥I'), fs i x = 0) (hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ),
    ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ

Tactic:
choose fs hfs hxfs hfsU using hU
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : (i : ↥I') → X → (↑I : Type)
hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
h :
  Continuous[⨅ (i : ι), t i, _] (I'.attach.sup fs) ∧
    I'.attach.sup fs x = 0 ∧ EqOn (I'.attach.sup fs) 1 (⋂ (i : ↥I'), V i)ᶜ
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ

Tactic:
use I'.attach.sup fs

Premises used: Finset.attach, Finset.sup
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : (i : ↥I') → X → (↑I : Type)
hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
h : Continuous[⨅ (i : ι), t i, _] (I'.attach.sup fs)
h₁ : I'.attach.sup fs x = 0
h₂ : EqOn (I'.attach.sup fs) 1 (⋂ (i : ↥I'), V i)ᶜ
⊢ Continuous[⨅ (i : ι), t i, _] (I'.attach.sup fs) ∧
    I'.attach.sup fs x = 0 ∧ EqOn (I'.attach.sup fs) 1 (⋂ (i : ↥I'), V i)ᶜ

Tactic:
constructorm* _ ∧ _
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : (i : ↥I') → X → (↑I : Type)
hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ Continuous[⨅ (i : ι), t i, _] (I'.attach.sup fs)

Tactic:
solve_by_elim [Continuous.finset_sup, continuous_iInf_dom]

Premises used: Continuous.finset_sup, continuous_iInf_dom
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : (i : ↥I') → X → (↑I : Type)
hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ I'.attach.sup fs x = 0

Tactic:
simpa [show (0 : ↥I) = ⊥ from rfl] using hxfs

Premises used: rfl
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : (i : ↥I') → X → (↑I : Type)
hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ ∀ (i : ↥I') ⦃x : X⦄, x ∈ (U i)ᶜ → fs i x = ⊤

Tactic:
simp only [EqOn, Pi.one_apply, show (1 : ↥I) = ⊤ from rfl] at hfsU ⊢

Premises used: Pi.one_apply, Set.EqOn, rfl
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : (i : ↥I') → X → (↑I : Type)
hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I') ⦃x : X⦄, x ∈ (U i)ᶜ → fs i x = ⊤
⊢ Eq (α := Prop) (∀ ⦃x : X⦄, Membership.mem (γ := Set X) (⋂ (i : ↥I'), V i)ᶜ x → I'.attach.sup fs x = ⊤)
    (∀ (x : X) (i : ↥I'), x ∈ (V i)ᶜ → ∃ (b : ↥I'), fs b x = ⊤)

Tactic:
simp [Finset.sup_eq_top_iff]

Premises used: Finset.sup_eq_top_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : (i : ↥I') → X → (↑I : Type)
hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I') ⦃x : X⦄, x ∈ (U i)ᶜ → fs i x = ⊤
h : ∀ (x : X) (i : ↥I'), x ∈ (V i)ᶜ → ∃ (b : ↥I'), fs b x = ⊤
⊢ ∀ ⦃x : X⦄, Membership.mem (γ := Set X) (⋂ (i : ↥I'), V i)ᶜ x → I'.attach.sup fs x = ⊤

Tactic:
conv => equals ∀ x i, x ∈ (V i)ᶜ → ∃ b, fs b x = ⊤ => simp [Finset.sup_eq_top_iff]

Premises used: Finset.sup_eq_top_iff
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x_1 : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : (i : ↥I') → X → (↑I : Type)
hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x_1 = 0
hfsU : ∀ (i : ↥I') ⦃x : X⦄, x ∈ (U i)ᶜ → fs i x = ⊤
x : X
i : ↥I'
hxi : x ∈ (V i)ᶜ
tauto_set tauto_set₁ :
  ∀ (hUV : ∀ (i : ↥I'), ∀ x ∈ U i, x ∈ V i) (hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i))
    (hxfs : ∀ (i : ↥I'), fs i x_1 = 0) (hfsU : ∀ (i : ↥I') ⦃x : X⦄, x ∉ U i → fs i x = ⊤) (hxi : x ∉ V i), x ∉ U i
tauto_set₂ tauto_set₃ :
  ∀ (hUV : ∀ (i : ↥I'), ∀ x ∈ U i, x ∈ V i) (hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i))
    (hxfs : ∀ (i : ↥I'), fs i x_1 = 0) (hfsU : ∀ (i : ↥I') ⦃x : X⦄, x ∉ U i → fs i x = ⊤) (hxi : x ∉ V i),
    x ∈ U i → False
⊢ x ∈ (U i)ᶜ

Tactic:
tauto_set
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x_1 : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : (i : ↥I') → X → (↑I : Type)
hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x_1 = 0
hfsU : ∀ (i : ↥I') ⦃x : X⦄, x ∈ (U i)ᶜ → fs i x = ⊤
x : X
i : ↥I'
hxi : x ∈ (V i)ᶜ
⊢ fs i x = ⊤

Tactic:
specialize hfsU i (by tauto_set)
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
x_1 : X
I' : Finset ι
V U : (i : ↥I') → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : (i : ↥I') → X → (↑I : Type)
hfs : ∀ (i : ↥I'), Continuous[t (↑i : ι), _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x_1 = 0
x : X
i : ↥I'
hxi : x ∈ (V i)ᶜ
hfsU h h₁ : fs i x = ⊤
⊢ ∃ (b : ↥I'), fs b x = ⊤

Tactic:
exists i
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u_1
t₁ t₂ : TopologicalSpace X
ht₁ : CompletelyRegularSpace X
ht₂ : CompletelyRegularSpace X
rw : CompletelyRegularSpace X
⊢ CompletelyRegularSpace X

Tactic:
rw [inf_eq_iInf]

Premises used: inf_eq_iInf
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u_1
t₁ t₂ : TopologicalSpace X
ht₁ : CompletelyRegularSpace X
ht₂ : CompletelyRegularSpace X
ht : ∀ (i : Bool), CompletelyRegularSpace X
⊢ CompletelyRegularSpace X

Tactic:
apply completelyRegularSpace_iInf

Premises used: completelyRegularSpace_iInf
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u_1
t₁ t₂ : TopologicalSpace X
ht₁ : CompletelyRegularSpace X
ht₂ : CompletelyRegularSpace X
⊢ ∀ (i : Bool), CompletelyRegularSpace X

Tactic:
simp [*]
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
t : (i : ι) → TopologicalSpace (X i)
ht : ∀ (i : ι), CompletelyRegularSpace.{u_2} (X i)
⊢ CompletelyRegularSpace ((i : ι) → X i)

Tactic:
completelyRegularSpace_iInf (fun i => completelyRegularSpace_induced (ht i) _)

Premises used: completelyRegularSpace_induced, completelyRegularSpace_iInf
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
htX : CompletelyRegularSpace X
htY : CompletelyRegularSpace Y
⊢ CompletelyRegularSpace (X × Y)

Tactic:
completelyRegularSpace_inf
    (completelyRegularSpace_induced htX _) ((completelyRegularSpace_induced htY _))

Premises used: completelyRegularSpace_induced, completelyRegularSpace_inf
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
rw : ∀ (x : X), 𝓝 x = comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x))
⊢ IsInducing.{u, u} (X := X) (Y := StoneCech X) stoneCechUnit

Tactic:
rw [isInducing_iff_nhds]

Premises used: Topology.isInducing_iff_nhds
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
a : 𝓝 x ≤ comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x))
a₁ : comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x)) ≤ 𝓝 x
⊢ 𝓝 x = comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
a : LE.le (α := Filter (StoneCech X)) (map stoneCechUnit (𝓝 x)) (𝓝 (stoneCechUnit x))
⊢ 𝓝 x ≤ comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x))

Tactic:
rw [← map_le_iff_le_comap]

Premises used: Filter.map_le_iff_le_comap
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
⊢ LE.le (α := Filter (StoneCech X)) (map stoneCechUnit (𝓝 x)) (𝓝 (stoneCechUnit x))

Tactic:
continuous_stoneCechUnit.continuousAt

Premises used: continuous_stoneCechUnit, ContinuousAt, Continuous.continuousAt, Filter.Tendsto
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
⊢ LE.le (α := Filter (StoneCech X)) (map stoneCechUnit (𝓝 x)) (𝓝 (stoneCechUnit x))

Tactic:
exact continuous_stoneCechUnit.continuousAt

Premises used: continuous_stoneCechUnit, Continuous.continuousAt
-- Module: Mathlib.Topology.Separation.CompletelyRegular
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
a :
  ∀ (s : Set X),
    x ∈ s → IsOpen[inst] s → ∃ (i : Set (StoneCech X)), stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ s
⊢ comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x)) ≤ 𝓝 x

Tactic:
simp_rw [le_nhds_iff, ((nhds_basis_opens _).comap _).mem_iff, and_assoc]

Premises used: Filter.HasBasis.mem_iff, le_nhds_iff, Filter.HasBasis.comap, and_assoc, nhds_basis_opens