awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ((↑k : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε ∧
    HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑k : C(X, ℝ)) : (a : X) → ℝ) z
have pos₁ : ((↑k : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε
Tactic: fconstructor
-- 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
pos₁ : ((↑k : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (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
have pos₂ : HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑k : C(X, ℝ)) : (a : X) → ℝ) z
Tactic: fconstructor
-- 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
⊢ ((↑k : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε
have pos₁ : ∃ b ∈ xs, ((↑(h b) : C(X, ℝ)) : (a : X) → ℝ) z < HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε
Tactic: simp only [k, Finset.inf'_lt_iff, ContinuousMap.inf'_apply]
-- 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
⊢ HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑k : C(X, ℝ)) : (a : X) → ℝ) z
have pos₁ : ∀ i ∈ xs, HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) z : ℝ) ε < ((↑(h i) : C(X, ℝ)) : (a : X) → ℝ) z
Tactic: simp only [k, Finset.lt_inf'_iff, ContinuousMap.inf'_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
⊢ A.topologicalClosure = ⊤
have h : (↑A.topologicalClosure : Set C(X, ℝ)) = (↑⊤ : Set C(X, ℝ))
Tactic: apply SetLike.ext'
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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
⊢ (↑A.topologicalClosure : Set C(X, ℝ)) = (↑⊤ : Set C(X, ℝ))
have n : (↑L : Set C(X, ℝ)).Nonempty
Tactic: have n : Set.Nonempty (L : Set C(X, ℝ)) := ⟨(1 : C(X, ℝ)), A.le_topologicalClosure A.one_mem⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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, ℝ)) = (↑⊤ : Set C(X, ℝ))
have h : (↑A.topologicalClosure : Set C(X, ℝ)) = closure (↑L : 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))
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
⊢ f ∈ A.topologicalClosure
have rw : Membership.mem (γ := Subalgebra ℝ C(X, ℝ)) ⊤ f
Tactic: rw [subalgebra_topologicalClosure_eq_top_of_separatesPoints A w]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ (g : ↥A), ‖(↑g : C(X, ℝ)) - f‖ < ε
have w₁ : ∃ᶠ (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)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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, ℝ))
⊢ ∃ (g : ↥A), ‖(↑g : C(X, ℝ)) - f‖ < ε
have w₁ : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ (↑A.toSubsemiring : Set C(X, ℝ))
Tactic: rw [Metric.nhds_basis_ball.frequently_iff] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
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 : ↥A), ‖(↑g : C(X, ℝ)) - f‖ < ε
have obtain : ∀ (g : C(X, ℝ)) (H : g ∈ Metric.ball f ε) (m : g ∈ (↑A.toSubsemiring : Set C(X, ℝ))),
  ∃ (g : ↥A), ‖(↑g : C(X, ℝ)) - f‖ < ε
Tactic: obtain ⟨g, H, m⟩ := w ε pos
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
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 : ↥A), ‖(↑g : C(X, ℝ)) - f‖ < ε
have H₁ : ‖g - f‖ < ε
Tactic: rw [Metric.mem_ball, dist_eq_norm] at H
Cleared hypotheses: H, m
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : X → ℝ
c : Continuous[inst, _] f
ε : ℝ
pos : 0 < ε
⊢ ∃ (g : ↥A), ∀ (x : X), ‖HSub.hSub (α := ℝ) (((↑g : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (f x)‖ < ε
have obtain : ∀ (g : ↥A) (b : ‖(↑g : C(X, ℝ)) - { toFun := f, continuous_toFun := c : C(X, ℝ) }‖ < ε),
  ∃ (g : ↥A), ∀ (x : X), ‖HSub.hSub (α := ℝ) (((↑g : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (f x)‖ < ε
Tactic: obtain ⟨g, b⟩ := exists_mem_subalgebra_near_continuousMap_of_separatesPoints A w ⟨f, c⟩ ε pos
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : X → ℝ
c : Continuous[inst, _] f
ε : ℝ
pos : 0 < ε
g : ↥A
b : ‖(↑g : C(X, ℝ)) - { toFun := f, continuous_toFun := c : C(X, ℝ) }‖ < ε
⊢ ∃ (g : ↥A), ∀ (x : X), ‖HSub.hSub (α := ℝ) (((↑g : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (f x)‖ < ε
have h : ∀ (x : X), ‖HSub.hSub (α := ℝ) (((↑g : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (f x)‖ < ε
Tactic: use g
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : X → ℝ
c : Continuous[inst, _] f
ε : ℝ
pos : 0 < ε
g : ↥A
b : ‖(↑g : C(X, ℝ)) - { toFun := f, continuous_toFun := c : C(X, ℝ) }‖ < ε
⊢ ∀ (x : X), ‖HSub.hSub (α := ℝ) (((↑g : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (f x)‖ < ε
have h : ∀
  (b :
    ∀ (x : X),
      norm (E := ℝ) (((↑g : C(X, ℝ)) - { toFun := f, continuous_toFun := c : C(X, ℝ) } : (a : X) → ℝ) x : ℝ) < ε)
  (x : X), ‖HSub.hSub (α := ℝ) (((↑g : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (f x)‖ < ε
Tactic: rwa [norm_lt_iff _ pos] at b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C((↑K : Type u_2), ℝ) :=
  compStarAlgHom' ℝ ℝ { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ }
AK : Subalgebra ℝ C((↑K : Type u_2), ℝ) := Subalgebra.map (↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) A
x y : (↑K : Type u_2)
hxy : x ≠ y
⊢ ∃ (f : (↑K : Type u_2) → ℝ),
    Membership.mem (γ := Set ((↑K : Type u_2) → ℝ))
        ((fun (f : C((↑K : Type u_2), ℝ)) ↦ (⇑f : (a : (↑K : Type u_2)) → ℝ)) '' (↑AK : Set C((↑K : Type u_2), ℝ))) f ∧
      f x ≠ f y
have obtain : ∀ (w : X → ℝ) (hg_sep : w (↑x : X) ≠ w (↑y : X)) (g : C(X, ℝ)) (hg1 : g ∈ (↑A : Set C(X, ℝ)))
  (hg2 : (fun (f : C(X, ℝ)) ↦ ((⇑f : (a : X) → ℝ) : (a : X) → ℝ)) g = w),
  ∃ (f : (↑K : Type u_2) → ℝ),
    Membership.mem (γ := Set ((↑K : Type u_2) → ℝ))
        ((fun (f : C((↑K : Type u_2), ℝ)) ↦ (⇑f : (a : (↑K : Type u_2)) → ℝ)) '' (↑AK : Set C((↑K : Type u_2), ℝ))) f ∧
      f x ≠ f y
Tactic: obtain ⟨_, ⟨g, hg1, hg2⟩, hg_sep⟩ := hA (Subtype.coe_ne_coe.mpr hxy)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C((↑K : Type u_2), ℝ) :=
  compStarAlgHom' ℝ ℝ { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ }
AK : Subalgebra ℝ C((↑K : Type u_2), ℝ) := Subalgebra.map (↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) A
x y : (↑K : Type u_2)
hxy : x ≠ y
w : X → ℝ
hg_sep : w (↑x : X) ≠ w (↑y : X)
g : C(X, ℝ)
hg1 : g ∈ (↑A : Set C(X, ℝ))
hg2 : (fun (f : C(X, ℝ)) ↦ ((⇑f : (a : X) → ℝ) : (a : X) → ℝ)) g = w
⊢ ∃ (f : (↑K : Type u_2) → ℝ),
    Membership.mem (γ := Set ((↑K : Type u_2) → ℝ))
        ((fun (f : C((↑K : Type u_2), ℝ)) ↦ (⇑f : (a : (↑K : Type u_2)) → ℝ)) '' (↑AK : Set C((↑K : Type u_2), ℝ))) f ∧
      f x ≠ f y
have simp : ∃ a ∈ AK, Ne (α := ℝ) ((a : (a : (↑K : Type u_2)) → ℝ) x : ℝ) ((a : (a : (↑K : Type u_2)) → ℝ) y : ℝ)
Tactic: simp only [Set.mem_image, SetLike.mem_coe, exists_exists_and_eq_and]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C((↑K : Type u_2), ℝ) :=
  compStarAlgHom' ℝ ℝ { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ }
AK : Subalgebra ℝ C((↑K : Type u_2), ℝ) := Subalgebra.map (↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) A
x y : (↑K : Type u_2)
hxy : x ≠ y
w : X → ℝ
hg_sep : w (↑x : X) ≠ w (↑y : X)
g : C(X, ℝ)
hg1 : g ∈ (↑A : Set C(X, ℝ))
hg2 : (fun (f : C(X, ℝ)) ↦ ((⇑f : (a : X) → ℝ) : (a : X) → ℝ)) g = w
⊢ ∃ a ∈ AK, Ne (α := ℝ) ((a : (a : (↑K : Type u_2)) → ℝ) x : ℝ) ((a : (a : (↑K : Type u_2)) → ℝ) y : ℝ)
have h : Membership.mem (α := C((↑K : Type u_2), ℝ)) AK
    ((restrict_on_K : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g : C((↑K : Type u_2), ℝ)) ∧
  Ne (α := ℝ)
    ((((restrict_on_K : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g : C((↑K : Type u_2), ℝ)) : (a : (↑K : Type u_2)) → ℝ)
        x :
      ℝ)
    ((((restrict_on_K : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g : C((↑K : Type u_2), ℝ)) : (a : (↑K : Type u_2)) → ℝ)
        y :
      ℝ)
Tactic: use restrict_on_K g
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C((↑K : Type u_2), ℝ) :=
  compStarAlgHom' ℝ ℝ { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ }
AK : Subalgebra ℝ C((↑K : Type u_2), ℝ) := Subalgebra.map (↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) A
x y : (↑K : Type u_2)
hxy : x ≠ y
w : X → ℝ
hg_sep : w (↑x : X) ≠ w (↑y : X)
g : C(X, ℝ)
hg1 : g ∈ (↑A : Set C(X, ℝ))
hg2 : (fun (f : C(X, ℝ)) ↦ ((⇑f : (a : X) → ℝ) : (a : X) → ℝ)) g = w
⊢ Membership.mem (α := C((↑K : Type u_2), ℝ)) AK
      ((restrict_on_K : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g : C((↑K : Type u_2), ℝ)) ∧
    Ne (α := ℝ)
      ((((restrict_on_K : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g : C((↑K : Type u_2), ℝ)) : (a : (↑K : Type u_2)) → ℝ)
          x :
        ℝ)
      ((((restrict_on_K : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g : C((↑K : Type u_2), ℝ)) : (a : (↑K : Type u_2)) → ℝ)
          y :
        ℝ)
have h : ∃ x ∈ A,
  Eq (α := C((↑K : Type u_2), ℝ))
    (((↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) x :
      C((↑K : Type u_2), ℝ))
    ((restrict_on_K : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g : C((↑K : Type u_2), ℝ))
Tactic: refine ⟨Subalgebra.mem_map.mpr ?_,
      by simpa only [compStarAlgHom'_apply, comp_apply, coe_mk, ne_eq, restrict_on_K, hg2]⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C((↑K : Type u_2), ℝ) :=
  compStarAlgHom' ℝ ℝ { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ }
AK : Subalgebra ℝ C((↑K : Type u_2), ℝ) := Subalgebra.map (↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) A
x y : (↑K : Type u_2)
hxy : x ≠ y
w : X → ℝ
hg_sep : w (↑x : X) ≠ w (↑y : X)
g : C(X, ℝ)
hg1 : g ∈ (↑A : Set C(X, ℝ))
hg2 : (fun (f : C(X, ℝ)) ↦ ((⇑f : (a : X) → ℝ) : (a : X) → ℝ)) g = w
⊢ ∃ x ∈ A,
    Eq (α := C((↑K : Type u_2), ℝ))
      (((↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) x :
        C((↑K : Type u_2), ℝ))
      ((restrict_on_K : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g : C((↑K : Type u_2), ℝ))
have right : Eq (α := C((↑K : Type u_2), ℝ))
  (((↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g :
    C((↑K : Type u_2), ℝ))
  ((restrict_on_K : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g : C((↑K : Type u_2), ℝ))
Tactic: use g, hg1
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C((↑K : Type u_2), ℝ) :=
  compStarAlgHom' ℝ ℝ { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ }
AK : Subalgebra ℝ C((↑K : Type u_2), ℝ) := Subalgebra.map (↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) A
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε
have hsep : AK.SeparatesPoints
Tactic: have hsep : AK.SeparatesPoints := by
    intro x y hxy
    obtain ⟨_, ⟨g, hg1, hg2⟩, hg_sep⟩ := hA (Subtype.coe_ne_coe.mpr hxy)
    simp only [Set.mem_image, SetLike.mem_coe, exists_exists_and_eq_and]
    use restrict_on_K g
    refine ⟨Subalgebra.mem_map.mpr ?_,
      by simpa only [compStarAlgHom'_apply, comp_apply, coe_mk, ne_eq, restrict_on_K, hg2]⟩
    use g, hg1
    simp
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C((↑K : Type u_2), ℝ) :=
  compStarAlgHom' ℝ ℝ { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ }
AK : Subalgebra ℝ C((↑K : Type u_2), ℝ) := Subalgebra.map (↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) A
hsep : AK.SeparatesPoints
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε
have obtain : ∀ (gK : C((↑K : Type u_2), ℝ)) (hgKAK : gK ∈ AK)
  (hgapprox :
    ∀ (x : (↑K : Type u_2)),
      ‖HSub.hSub (α := ℝ) (β := ℝ)
            (((↑(Subtype.mk (p := fun (x : C((↑K : Type u_2), ℝ)) ↦ x ∈ AK) gK hgKAK) : C((↑K : Type u_2), ℝ)) :
                  (a : (↑K : Type u_2)) → ℝ)
                x :
              ℝ)
            (K.restrict (π := fun (a : X) ↦ ℝ) (⇑f : (a : X) → ℝ) x : ℝ)‖ <
        ε),
  ∃ g ∈ A, ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε
Tactic: obtain ⟨⟨gK, hgKAK⟩, hgapprox⟩ :=
    @ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints _ _
    (isCompact_iff_compactSpace.mp hK) AK hsep (K.restrict f)
    (ContinuousOn.restrict (Continuous.continuousOn f.continuous)) ε pos
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.StoneWeierstrass (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
A : Subalgebra ℝ C(X, ℝ)
hA : A.SeparatesPoints
f : C(X, ℝ)
K : Set X
hK : IsCompact K
ε : ℝ
pos : 0 < ε
restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C((↑K : Type u_2), ℝ) :=
  compStarAlgHom' ℝ ℝ { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ }
AK : Subalgebra ℝ C((↑K : Type u_2), ℝ) := Subalgebra.map (↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) A
hsep : AK.SeparatesPoints
gK : C((↑K : Type u_2), ℝ)
hgKAK : gK ∈ AK
hgapprox :
  ∀ (x : (↑K : Type u_2)),
    ‖HSub.hSub (α := ℝ) (β := ℝ)
          (((↑(Subtype.mk (p := fun (x : C((↑K : Type u_2), ℝ)) ↦ x ∈ AK) gK hgKAK) : C((↑K : Type u_2), ℝ)) :
                (a : (↑K : Type u_2)) → ℝ)
              x :
            ℝ)
          (K.restrict (π := fun (a : X) ↦ ℝ) (⇑f : (a : X) → ℝ) x : ℝ)‖ <
      ε
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε
have obtain : ∀ (g : C(X, ℝ)) (hgA : g ∈ A)
  (hgKAK : ((↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g = gK),
  ∃ g ∈ A, ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε
Tactic: obtain ⟨g, hgA, hgKAK⟩ := Subalgebra.mem_map.mp hgKAK