awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 : 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₁]
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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

Tactic:
IsOpen.mem_nhds ?_ ?_

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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)
refine_2 : x ∈ W x
⊢ W x ∈ 𝓝 x

Tactic:
refine IsOpen.mem_nhds ?_ ?_

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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) → ℝ)
refine_1₁ : Continuous[inst, _] fun (b : X) ↦ HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) b : ℝ) ε
⊢ IsOpen[inst] (W x)

Tactic:
apply isOpen_lt

Premises used: isOpen_lt
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ Continuous[inst, _] (⇑(↑(h x) : C(X, ℝ)) : (a : X) → ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ Continuous[inst, _] fun (b : X) ↦ HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) b : ℝ) ε

Tactic:
fun_prop
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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_2 : ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ε
⊢ x ∈ W x

Tactic:
dsimp only [W, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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_2 : (f : (a : X) → ℝ) x < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ε
⊢ ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) x < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ε

Tactic:
rw [h_eq]
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ (f : (a : X) → ℝ) x < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ε

Tactic:
lt_add_of_pos_right _ pos

Premises used: lt_add_of_pos_right
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ (f : (a : X) → ℝ) x < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ε

Tactic:
exact lt_add_of_pos_right _ pos

Premises used: lt_add_of_pos_right
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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

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
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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

Tactic:
have xs_nonempty : xs.Nonempty := Set.nonempty_of_union_eq_top_of_nonempty _ _ nX xs_w
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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

Tactic:
⟨k.1, ?_, k.2⟩

Premises used: And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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, ℝ))) ⋯
pos₁ : dist (↑k : C(X, ℝ)) f < ε
⊢ ∃ (x : C(X, ℝ)), dist x f < ε ∧ x ∈ L

Tactic:
refine ⟨k.1, ?_, k.2⟩