awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
have lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
Tactic: have lt_h : ∀ x z, f z - ε < (h x : X → ℝ) z := by
    intro x z
    obtain ⟨y, ym, zm⟩ := Set.exists_set_mem_of_union_eq_top _ _ (ys_w x) z
    dsimp [h]
    simp only [coe_sup', Finset.sup'_apply, Finset.lt_sup'_iff]
    exact ⟨y, ym, zm⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
have h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
Tactic: have h_eq : ∀ x, (h x : X → ℝ) x = f x := by intro x; simp [h, w₁]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
x : X
⊢ W x ∈ 𝓝 x
have refine_1 : IsOpen[inst] (W x)
Tactic: refine IsOpen.mem_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
x : X
refine_1 : IsOpen[inst] (W x)
⊢ W x ∈ 𝓝 x
have refine_2 : x ∈ W x
Tactic: refine IsOpen.mem_nhds ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
x : X
⊢ IsOpen[inst] (W x)
have refine_1 : Continuous[inst, _] (⇑(↑(h x) : C(X, ℝ)) : (a : X) → ℝ)
Tactic: apply isOpen_lt
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
x : X
refine_1 : Continuous[inst, _] (⇑(↑(h x) : C(X, ℝ)) : (a : X) → ℝ)
⊢ IsOpen[inst] (W x)
have refine_1₁ : Continuous[inst, _] fun (b : X) ↦ HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) b : ℝ) ε
Tactic: apply isOpen_lt
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
x : X
⊢ x ∈ W x
have refine_2 : ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ε
Tactic: dsimp only [W, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
x : X
⊢ ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ε
have refine_2 : (f : (a : X) → ℝ) x < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ε
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
have W_nhds : ∀ (x : X), W x ∈ 𝓝 x
Tactic: have W_nhds : ∀ x, W x ∈ 𝓝 x := by
    intro x
    refine IsOpen.mem_nhds ?_ ?_
    · apply isOpen_lt <;> fun_prop
    · dsimp only [W, Set.mem_setOf_eq]
      rw [h_eq]
      exact lt_add_of_pos_right _ pos
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ t, W x) ⊤)
xs_w : Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ xs, W x) ⊤ := ⋯
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
have xs_nonempty : xs.Nonempty
Tactic: have xs_nonempty : xs.Nonempty := Set.nonempty_of_union_eq_top_of_nonempty _ _ nX xs_w
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ t, W x) ⊤)
xs_w : Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ xs, W x) ⊤ := ⋯
xs_nonempty : xs.Nonempty
k : (↑L : Type u_1) :=
  Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) (xs.inf' xs_nonempty fun (x : X) ↦ (↑(h x) : C(X, ℝ))) ⋯
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L
have pos₁ : dist (↑k : C(X, ℝ)) f < ε
Tactic: refine ⟨k.1, ?_, k.2⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ t, W x) ⊤)
xs_w : Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ xs, W x) ⊤ := ⋯
xs_nonempty : xs.Nonempty
k : (↑L : Type u_1) :=
  Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) (xs.inf' xs_nonempty fun (x : X) ↦ (↑(h x) : C(X, ℝ))) ⋯
⊢ dist (↑k : C(X, ℝ)) f < ε
have pos₁ : ∀ (x : X), dist (α := ℝ) (((↑k : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) < ε
Tactic: rw [dist_lt_iff pos]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
L : Set C(X, ℝ)
nA : L.Nonempty
inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L
sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L
sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, (f : (a : X) → ℝ) x = v x ∧ (f : (a : X) → ℝ) y = v y
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
nX : Nonempty X
g : (x y : X) → C(X, ℝ)
hg : ∀ (x y : X), g x y ∈ L
w₁ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
w₂ : ∀ (x y : X), Eq (α := ℝ) ((g x y : (a : X) → ℝ) y : ℝ) ((f : (a : X) → ℝ) y : ℝ)
U : X → X → Set X := fun (x y : X) ↦ {z : X | HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < (g x y : (a : X) → ℝ) z}
U_nhds_y : ∀ (x y : X), U x y ∈ 𝓝 y
ys : X → Finset X := fun (x : X) ↦ ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x_1 ∈ t, U x x_1) ⊤)
ys_w : ∀ (x : X), Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ ys x, U x y) ⊤ := ⋯
ys_nonempty : ∀ (x : X), (ys x).Nonempty
h : X → (↑L : Type u_1) :=
  fun (x : X) ↦ Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) ((ys x).sup' ⋯ fun (y : X) ↦ g x y) ⋯
lt_h : ∀ (x z : X), HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z
h_eq : ∀ (x : X), Eq (α := ℝ) (((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
W : X → Set X :=
  fun (x : X) ↦ {z : X | ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε}
W_nhds : ∀ (x : X), W x ∈ 𝓝 x
xs : Finset X := ⋯.choose (p := fun (t : Finset X) ↦ Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ t, W x) ⊤)
xs_w : Eq.{u_1 + 1} (α := Set X) (⋃ x ∈ xs, W x) ⊤ := ⋯
xs_nonempty : xs.Nonempty
k : (↑L : Type u_1) :=
  Subtype.mk (p := fun (x : C(X, ℝ)) ↦ x ∈ L) (xs.inf' xs_nonempty fun (x : X) ↦ (↑(h x) : C(X, ℝ))) ⋯
z : X
⊢ dist (α := ℝ) (((↑k : C(X, ℝ)) : (a : X) → ℝ) z : ℝ) ((f : (a : X) → ℝ) z : ℝ) < ε
have pos₁ : ((↑k : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε ∧
  HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑k : C(X, ℝ)) : (a : X) → ℝ) z
Tactic: rw [show ∀ a b ε : ℝ, dist a b < ε ↔ a < b + ε ∧ b - ε < a by
        intros; simp only [← Metric.mem_ball, Real.ball_eq_Ioo, Set.mem_Ioo, and_comm]]