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
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₁ : ∀ (x : X), dist (α := ℝ) (((↑k : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ) < ε
⊢ dist (↑k : C(X, ℝ)) f < ε

Tactic:
rw [dist_lt_iff pos]

Premises used: ContinuousMap.dist_lt_iff
-- 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, ℝ))) ⋯
z : X
a b ε_1 : ℝ
⊢ dist a b < ε_1 ↔ a < b + ε_1 ∧ b - ε_1 < a

Tactic:
simp only [← Metric.mem_ball, Real.ball_eq_Ioo, Set.mem_Ioo, and_comm]

Premises used: Set.mem_Ioo, Real.ball_eq_Ioo, and_comm, Metric.mem_ball
-- 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, ℝ))) ⋯
z : X
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
⊢ dist (α := ℝ) (((↑k : C(X, ℝ)) : (a : X) → ℝ) z : ℝ) ((f : (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]]
-- 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, ℝ))) ⋯
z : X
pos₁ : ((↑k : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε
pos₂ : HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑k : C(X, ℝ)) : (a : X) → ℝ) z
⊢ ((↑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:
fconstructor
-- 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, ℝ))) ⋯
z : X
pos₁ : ∃ b ∈ xs, ((↑(h b) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε
⊢ ((↑k : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε

Tactic:
simp only [k, Finset.inf'_lt_iff, ContinuousMap.inf'_apply]

Premises used: Finset.inf'_lt_iff, ContinuousMap.inf'_apply
-- 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, ℝ))) ⋯
z : X
⊢ ∃ b ∈ xs, ((↑(h b) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε

Tactic:
Set.exists_set_mem_of_union_eq_top _ _ xs_w z

Premises used: Set.Mem, Set.exists_set_mem_of_union_eq_top
-- 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, ℝ))) ⋯
z : X
⊢ ∃ b ∈ xs, ((↑(h b) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε

Tactic:
exact Set.exists_set_mem_of_union_eq_top _ _ xs_w z

Premises used: Set.exists_set_mem_of_union_eq_top
-- 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, ℝ))) ⋯
z : X
pos₁ : ∀ i ∈ xs, HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h i) : C(X, ℝ)) : (a : X) → ℝ) z
⊢ HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑k : C(X, ℝ)) : (a : X) → ℝ) z

Tactic:
simp only [k, Finset.lt_inf'_iff, ContinuousMap.inf'_apply]

Premises used: ContinuousMap.inf'_apply, Finset.lt_inf'_iff
-- 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, ℝ))) ⋯
z x : X
⊢ HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h x) : C(X, ℝ)) : (a : X) → ℝ) z

Tactic:
apply lt_h
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
h : (↑A.topologicalClosure : Set C(X, ℝ)) = (↑⊤ : Set C(X, ℝ))
⊢ A.topologicalClosure = ⊤

Tactic:
apply SetLike.ext'

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure
⊢ (↑L : Set C(X, ℝ)).Nonempty

Tactic:
have n : Set.Nonempty (L : Set C(X, ℝ)) := ⟨(1 : C(X, ℝ)), A.le_topologicalClosure A.one_mem⟩
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure
n : (↑L : Set C(X, ℝ)).Nonempty
⊢ closure (↑L : Set C(X, ℝ)) = ⊤

Tactic:
sublattice_closure_eq_top (L : Set C(X, ℝ)) n
      (fun f fm g gm => inf_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩)
      (fun f fm g gm => sup_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩)
      (Subalgebra.SeparatesPoints.strongly
        (Subalgebra.separatesPoints_monotone A.le_topologicalClosure w))

Premises used: Subalgebra.SeparatesPoints.strongly, Subalgebra.separatesPoints_monotone, ContinuousMap.sup_mem_closed_subalgebra, ContinuousMap.inf_mem_closed_subalgebra, ContinuousMap.sublattice_closure_eq_top, Subtype.mk, SetLike.coe, Subalgebra.le_topologicalClosure, Subalgebra.isClosed_topologicalClosure
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure
n : (↑L : Set C(X, ℝ)).Nonempty
h : (↑A.topologicalClosure : Set C(X, ℝ)) = closure (↑L : Set C(X, ℝ))
⊢ (↑A.topologicalClosure : Set C(X, ℝ)) = (↑⊤ : Set C(X, ℝ))

Tactic:
convert!
    sublattice_closure_eq_top (L : Set C(X, ℝ)) n
      (fun f fm g gm => inf_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩)
      (fun f fm g gm => sup_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩)
      (Subalgebra.SeparatesPoints.strongly
        (Subalgebra.separatesPoints_monotone A.le_topologicalClosure w))

Premises used: Subalgebra.SeparatesPoints.strongly, Subalgebra.separatesPoints_monotone, ContinuousMap.sup_mem_closed_subalgebra, ContinuousMap.inf_mem_closed_subalgebra, ContinuousMap.sublattice_closure_eq_top, Subtype.mk, SetLike.coe, Subalgebra.le_topologicalClosure, Subalgebra.isClosed_topologicalClosure
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure
n : (↑L : Set C(X, ℝ)).Nonempty
⊢ (↑A.topologicalClosure : Set C(X, ℝ)) = closure (↑L : Set C(X, ℝ))

Tactic:
simp [L]
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
rw : Membership.mem (γ := Subalgebra ℝ C(X, ℝ)) ⊤ f
⊢ f ∈ A.topologicalClosure

Tactic:
rw [subalgebra_topologicalClosure_eq_top_of_separatesPoints A w]

Premises used: ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ Membership.mem (γ := Subalgebra ℝ C(X, ℝ)) ⊤ f

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ᶠ (x : C(X, ℝ)) in 𝓝 f, x ∈ (↑A.toSubsemiring : Set C(X, ℝ))

Tactic:
have w :=
    mem_closure_iff_frequently.mp (continuousMap_mem_subalgebra_closure_of_separatesPoints A w f)
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w_1 : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(X, ℝ)) in 𝓝 f, x ∈ (↑A.toSubsemiring : Set C(X, ℝ))
⊢ ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ (↑A.toSubsemiring : Set C(X, ℝ))

Tactic:
rw [Metric.nhds_basis_ball.frequently_iff] at w

Premises used: Filter.HasBasis.frequently_iff, Metric.nhds_basis_ball
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w_1 : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ (↑A.toSubsemiring : Set C(X, ℝ))
obtain :
  ∀ (g : C(X, ℝ)) (H : g ∈ Metric.ball f ε) (m : g ∈ (↑A.toSubsemiring : Set C(X, ℝ))),
    ∃ (g : ↥A), ‖(↑g : C(X, ℝ)) - f‖ < ε
⊢ ∃ (g : ↥A), ‖(↑g : C(X, ℝ)) - f‖ < ε

Tactic:
obtain ⟨g, H, m⟩ := w ε pos
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w_1 : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ (↑A.toSubsemiring : Set C(X, ℝ))
g : C(X, ℝ)
H : g ∈ Metric.ball f ε
m : g ∈ (↑A.toSubsemiring : Set C(X, ℝ))
⊢ ‖g - f‖ < ε

Tactic:
rw [Metric.mem_ball, dist_eq_norm] at H

Premises used: dist_eq_norm, Metric.mem_ball