awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have hgx : g x = 0
Tactic: have hgx : g x = 0 := Subtype.ext (hfx (subset_closure (mem_singleton x)))
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have hgK : EqOn g 1 K
Tactic: have hgK : EqOn g 1 K := fun k hk => Subtype.ext (hfK hk)
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have hK₁ : ∃ (t : Set Y), IsClosed[inst_1] t ∧ f ⁻¹' t = K
Tactic: rw [hf.isClosed_iff] at hK
Cleared hypotheses: hK, hxK
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have 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)
Tactic: obtain ⟨K, hK, rfl⟩ := hK
Cleared hypotheses: K, hK, hxK
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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_1 : X → (↑I : Type)), Continuous[inst, _] f_1 ∧ f_1 x = 0 ∧ EqOn f_1 1 (f ⁻¹' K)
have hxK₁ : f x ∉ K
Tactic: rw [mem_preimage] at hxK
Cleared hypotheses: hxK
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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
⊢ ∃ (f_1 : X → (↑I : Type)), Continuous[inst, _] f_1 ∧ f_1 x = 0 ∧ EqOn f_1 1 (f ⁻¹' K)
have 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)
Tactic: obtain ⟨g, hcf, egfx, hgK⟩ := CompletelyRegularSpace.completely_regular _ _ hK hxK
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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)
have refine : EqOn (g ∘ f) 1 (f ⁻¹' K)
Tactic: refine ⟨g ∘ f, hcf.comp hf.continuous, egfx, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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 ⁻¹' K)
have arg : 1
Tactic: arg 2
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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 ⁻¹' K)
have arg : 1
Tactic: arg 2; equals (1 : Y → ↥I) ∘ f => rfl
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ (i : ι), t i
⊢ CompletelyRegularSpace X
have 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ᶜ
Tactic: rw [completelyRegularSpace_iff_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
have hxK₁ : ∃ (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
Cleared hypotheses: hxK
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 Kᶜ
have 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)ᶜ
Tactic: obtain ⟨I', V, hV, rfl⟩ := hxK
Cleared hypotheses: K, hxK
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ
have hV₁ : ∀ (i : ↥I'), ∃ t_1 ⊆ V i, IsOpen[t (↑i : ι)] t_1 ∧ x ∈ t_1
Tactic: simp only [mem_nhds_iff] at hV
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ
have 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)ᶜ
Tactic: choose U hUV hU hxU using hV
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ
have hU₁ : ∀ (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)
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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)ᶜ
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ
have 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)ᶜ
Tactic: choose fs hfs hxfs hfsU using hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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)ᶜ
⊢ ∃ (f : X → (↑I : Type)), Continuous[⨅ (i : ι), t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ (i : ↥I'), V i)ᶜ
have 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)ᶜ
Tactic: use I'.attach.sup fs
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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) ∧
    I'.attach.sup fs x = 0 ∧ EqOn (I'.attach.sup fs) 1 (⋂ (i : ↥I'), V i)ᶜ
have h : Continuous[⨅ (i : ι), t i, _] (I'.attach.sup fs)
Tactic: constructorm* _ ∧ _
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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)
⊢ Continuous[⨅ (i : ι), t i, _] (I'.attach.sup fs) ∧
    I'.attach.sup fs x = 0 ∧ EqOn (I'.attach.sup fs) 1 (⋂ (i : ↥I'), V i)ᶜ
have h₁ : I'.attach.sup fs x = 0
Tactic: constructorm* _ ∧ _
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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
⊢ Continuous[⨅ (i : ι), t i, _] (I'.attach.sup fs) ∧
    I'.attach.sup fs x = 0 ∧ EqOn (I'.attach.sup fs) 1 (⋂ (i : ↥I'), V i)ᶜ
have h₂ : EqOn (I'.attach.sup fs) 1 (⋂ (i : ↥I'), V i)ᶜ
Tactic: constructorm* _ ∧ _
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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)ᶜ
⊢ EqOn (I'.attach.sup fs) 1 (⋂ (i : ↥I'), V i)ᶜ
have hfsU₁ : ∀ (i : ↥I') ⦃x : X⦄, x ∈ (U i)ᶜ → fs i x = ⊤
Tactic: simp only [EqOn, Pi.one_apply, show (1 : ↥I) = ⊤ from rfl] at hfsU ⊢
Cleared hypotheses: hfsU
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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 = ⊤
⊢ ∀ ⦃x : X⦄, Membership.mem (γ := Set X) (⋂ (i : ↥I'), V i)ᶜ x → I'.attach.sup fs x = ⊤
have h : ∀ (x : X) (i : ↥I'), x ∈ (V i)ᶜ → ∃ (b : ↥I'), fs b x = ⊤
Tactic: conv => equals ∀ x i, x ∈ (V i)ᶜ → ∃ b, fs b x = ⊤ => simp [Finset.sup_eq_top_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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)ᶜ
⊢ x ∈ (U i)ᶜ
have 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
Tactic: tauto_set
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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)ᶜ
⊢ ∃ (b : ↥I'), fs b x = ⊤
have hfsU₁ : fs i x = ⊤
Tactic: specialize hfsU i (by tauto_set)
Cleared hypotheses: hfsU
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u_1
t₁ t₂ : TopologicalSpace X
ht₁ : CompletelyRegularSpace X
ht₂ : CompletelyRegularSpace X
⊢ CompletelyRegularSpace X
have rw : CompletelyRegularSpace X
Tactic: rw [inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u_1
t₁ t₂ : TopologicalSpace X
ht₁ : CompletelyRegularSpace X
ht₂ : CompletelyRegularSpace X
⊢ CompletelyRegularSpace X
have ht : ∀ (i : Bool), CompletelyRegularSpace X
Tactic: apply completelyRegularSpace_iInf
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
⊢ IsInducing.{u, u} (X := X) (Y := StoneCech X) stoneCechUnit
have rw : ∀ (x : X), 𝓝 x = comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x))
Tactic: rw [isInducing_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
⊢ 𝓝 x = comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x))
have a : 𝓝 x ≤ comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
a : 𝓝 x ≤ comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x))
⊢ 𝓝 x = comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x))
have a₁ : comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x)) ≤ 𝓝 x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
⊢ 𝓝 x ≤ comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x))
have a : LE.le (α := Filter (StoneCech X)) (map stoneCechUnit (𝓝 x)) (𝓝 (stoneCechUnit x))
Tactic: rw [← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
⊢ comap (β := StoneCech X) stoneCechUnit (𝓝 (stoneCechUnit x)) ≤ 𝓝 x
have a : ∀ (s : Set X),
  x ∈ s → IsOpen[inst] s → ∃ (i : Set (StoneCech X)), stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ s
Tactic: simp_rw [le_nhds_iff, ((nhds_basis_opens _).comap _).mem_iff, and_assoc]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst] U
⊢ ∃ (i : Set (StoneCech X)), stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U
have 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
Tactic: obtain ⟨f, hf, efx, hfU⟩ :=
      CompletelyRegularSpace.completely_regular_isOpen x U hU hxU
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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ᶜ
⊢ ∃ (i : Set (StoneCech X)), stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U
have hfU₁ : Uᶜ ⊆ f ⁻¹' {1}
Tactic: conv at hfU => equals Uᶜ ⊆ f ⁻¹' {1} => simp [EqOn, subset_def]
Cleared hypotheses: hfU
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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}
⊢ ∃ (i : Set (StoneCech X)), stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U
have hfU₁ : stoneCechUnit ⁻¹' stoneCechExtend hf ⁻¹' {1}ᶜ ⊆ U
Tactic: rw [← compl_subset_comm, ← preimage_compl, ← stoneCechExtend_extends hf, preimage_comp] at hfU
Cleared hypotheses: hfU
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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
have a : stoneCechUnit x ∈ stoneCechExtend hf ⁻¹' {1}ᶜ
Tactic: refine ⟨stoneCechExtend hf ⁻¹' {1}ᶜ, ?_,
      isOpen_compl_singleton.preimage (continuous_stoneCechExtend hf), hfU⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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
⊢ stoneCechUnit x ∈ stoneCechExtend hf ⁻¹' {1}ᶜ
have a : ¬Eq (α := (↑I : Type)) 0 1
Tactic: rw [mem_preimage, stoneCechExtend_stoneCechUnit, efx, mem_compl_iff, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have 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
Tactic: obtain ⟨s, hs, hx, hsK⟩ := h.exists_subset_of_mem_open hx hK.isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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ᶜ
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have refine_1 : Continuous[inst, _] (sᶜ.indicator 1)
Tactic: refine ⟨sᶜ.indicator 1, ?_, by simpa, fun x hx ↦ indicator_of_mem ?_ _⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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)
⊢ ∃ (f : X → (↑I : Type)), Continuous[inst, _] f ∧ f x = 0 ∧ EqOn f 1 K
have refine_2 : ∀ (x : X) (hx : x ∈ K), x ∈ sᶜ
Tactic: refine ⟨sᶜ.indicator 1, ?_, by simpa, fun x hx ↦ indicator_of_mem ?_ _⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompletelyRegularSpace X
hX : #X < 𝔠
⊢ IsTopologicalBasis.{u} (α := X) {s : Set X | IsClopen s}
have 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
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds (fun x s ↦ IsClopen.isOpen s) (fun x s hxs hs ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (goal)
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
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have 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
Tactic: choose f hf using completely_regular_isOpen x s hs hxs
-- Lean 4 proof step from Mathlib.Topology.Separation.CompletelyRegular (hypothesis)
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ᶜ
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {s : Set X | IsClopen s} v ∧ x ∈ v ∧ v ⊆ s
have hfc : Continuous[inst, _] f
Tactic: obtain ⟨hfc, hf₀, hf₁⟩ := hf
Cleared hypotheses: hf