awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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, ℝ))
H₁ : ‖g - f‖ < ε
⊢ g ∈ (↑A.toSubsemiring : Set C(X, ℝ))

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

Premises used: dist_eq_norm, Metric.mem_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, ℝ))
g : C(X, ℝ)
H : ‖g - f‖ < ε
m : g ∈ (↑A.toSubsemiring : Set C(X, ℝ))
⊢ ∃ (g : ↥A), ‖(↑g : C(X, ℝ)) - f‖ < ε

Tactic:
⟨⟨g, m⟩, H⟩

Premises used: Subtype.mk, Exists.intro
-- 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 - f‖ < ε
m : g ∈ (↑A.toSubsemiring : Set C(X, ℝ))
⊢ ∃ (g : ↥A), ‖(↑g : C(X, ℝ)) - f‖ < ε

Tactic:
exact ⟨⟨g, m⟩, 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
f : X → ℝ
c : Continuous[inst, _] f
ε : ℝ
pos : 0 < ε
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)‖ < ε
⊢ ∃ (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

Premises used: ContinuousMap.mk, ContinuousMap.exists_mem_subalgebra_near_continuousMap_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 : X → ℝ
c : Continuous[inst, _] f
ε : ℝ
pos : 0 < ε
g : ↥A
b : ‖(↑g : C(X, ℝ)) - { toFun := f, continuous_toFun := c : C(X, ℝ) }‖ < ε
h : ∀ (x : X), ‖HSub.hSub (α := ℝ) (((↑g : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (f x)‖ < ε
⊢ ∃ (g : ↥A), ∀ (x : X), ‖HSub.hSub (α := ℝ) (((↑g : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (f x)‖ < ε

Tactic:
use g
-- 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 : X → ℝ
c : Continuous[inst, _] f
ε : ℝ
pos : 0 < ε
g : ↥A
b : ‖(↑g : C(X, ℝ)) - { toFun := f, continuous_toFun := c : C(X, ℝ) }‖ < ε
h h₁ h₂ 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)‖ < ε
⊢ ∀ (x : X), ‖HSub.hSub (α := ℝ) (((↑g : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (f x)‖ < ε

Tactic:
rwa [norm_lt_iff _ pos] at b

Premises used: ContinuousMap.norm_lt_iff
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
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
⊢ ∃ (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)

Premises used: Iff.mpr, Subtype.coe_ne_coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
simp : ∃ a ∈ AK, Ne (α := ℝ) ((a : (a : (↑K : Type u_2)) → ℝ) x : ℝ) ((a : (a : (↑K : Type u_2)) → ℝ) 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

Tactic:
simp only [Set.mem_image, SetLike.mem_coe, exists_exists_and_eq_and]

Premises used: Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
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 :
        ℝ)
⊢ ∃ a ∈ AK, Ne (α := ℝ) ((a : (a : (↑K : Type u_2)) → ℝ) x : ℝ) ((a : (a : (↑K : Type u_2)) → ℝ) y : ℝ)

Tactic:
use restrict_on_K g

Premises used: DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ 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:
simpa only [compStarAlgHom'_apply, comp_apply, coe_mk, ne_eq, restrict_on_K, hg2]

Premises used: ContinuousMap.comp_apply, ne_eq, ContinuousMap.coe_mk, ContinuousMap.compStarAlgHom'_apply
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
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), ℝ))
⊢ 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:
refine ⟨Subalgebra.mem_map.mpr ?_,
      by simpa only [compStarAlgHom'_apply, comp_apply, coe_mk, ne_eq, restrict_on_K, hg2]⟩
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
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), ℝ))
⊢ ∃ 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:
use g, hg1
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ 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:
simp
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
⊢ 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
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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
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 : ℝ)‖ < ε
⊢ ∃ 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

Premises used: ContinuousMap.continuous, Continuous.continuousOn, ContinuousOn.restrict, Set.restrict, ContinuousMap.exists_mem_subalgebra_near_continuous_of_separatesPoints, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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 : ℝ)‖ <
      ε
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 : ℝ)‖ < ε
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε

Tactic:
obtain ⟨g, hgA, hgKAK⟩ := Subalgebra.mem_map.mp hgKAK

Premises used: Subalgebra.mem_map, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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_1 : gK ∈ AK
hgapprox :
  ∀ (x : (↑K : Type u_2)),
    ‖HSub.hSub (α := ℝ) (β := ℝ)
          (((↑(Subtype.mk (p := fun (x : C((↑K : Type u_2), ℝ)) ↦ x ∈ AK) gK hgKAK_1) : C((↑K : Type u_2), ℝ)) :
                (a : (↑K : Type u_2)) → ℝ)
              x :
            ℝ)
          (K.restrict (π := fun (a : X) ↦ ℝ) (⇑f : (a : X) → ℝ) x : ℝ)‖ <
      ε
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
right : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε

Tactic:
use g, hgA
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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_1 : gK ∈ AK
hgapprox :
  ∀ (x : (↑K : Type u_2)),
    ‖HSub.hSub (α := ℝ) (β := ℝ)
          (((↑(Subtype.mk (p := fun (x : C((↑K : Type u_2), ℝ)) ↦ x ∈ AK) gK hgKAK_1) : C((↑K : Type u_2), ℝ)) :
                (a : (↑K : Type u_2)) → ℝ)
              x :
            ℝ)
          (K.restrict (π := fun (a : X) ↦ ℝ) (⇑f : (a : X) → ℝ) x : ℝ)‖ <
      ε
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
x : X
hxK : x ∈ K
rw :
  Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ)
    (((((↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g :
            C((↑K : Type u_2), ℝ)) :
          (a : (↑K : Type u_2)) → ℝ)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) :
      ℝ)
⊢ Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ)
    ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)

Tactic:
rw [← hgKAK]
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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_1 : gK ∈ AK
hgapprox :
  ∀ (x : (↑K : Type u_2)),
    ‖HSub.hSub (α := ℝ) (β := ℝ)
          (((↑(Subtype.mk (p := fun (x : C((↑K : Type u_2), ℝ)) ↦ x ∈ AK) gK hgKAK_1) : C((↑K : Type u_2), ℝ)) :
                (a : (↑K : Type u_2)) → ℝ)
              x :
            ℝ)
          (K.restrict (π := fun (a : X) ↦ ℝ) (⇑f : (a : X) → ℝ) x : ℝ)‖ <
      ε
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
x : X
hxK : x ∈ K
⊢ Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ)
    (((((↑restrict_on_K : C(X, ℝ) →ₐ[ℝ] C((↑K : Type u_2), ℝ)) : (a : C(X, ℝ)) → C((↑K : Type u_2), ℝ)) g :
            C((↑K : Type u_2), ℝ)) :
          (a : (↑K : Type u_2)) → ℝ)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) :
      ℝ)

Tactic:
rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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_1 : gK ∈ AK
hgapprox :
  ∀ (x : (↑K : Type u_2)),
    ‖HSub.hSub (α := ℝ) (β := ℝ)
          (((↑(Subtype.mk (p := fun (x : C((↑K : Type u_2), ℝ)) ↦ x ∈ AK) gK hgKAK_1) : C((↑K : Type u_2), ℝ)) :
                (a : (↑K : Type u_2)) → ℝ)
              x :
            ℝ)
          (K.restrict (π := fun (a : X) ↦ ℝ) (⇑f : (a : X) → ℝ) x : ℝ)‖ <
      ε
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
x : X
hxK : x ∈ K
⊢ Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ)
    ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)

Tactic:
have eqg : g x = gK ⟨x, hxK⟩ := by
    rw [← hgKAK]; rfl
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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_1 : gK ∈ AK
hgapprox :
  ∀ (x : (↑K : Type u_2)),
    ‖HSub.hSub (α := ℝ) (β := ℝ)
          (((↑(Subtype.mk (p := fun (x : C((↑K : Type u_2), ℝ)) ↦ x ∈ AK) gK hgKAK_1) : C((↑K : Type u_2), ℝ)) :
                (a : (↑K : Type u_2)) → ℝ)
              x :
            ℝ)
          (K.restrict (π := fun (a : X) ↦ ℝ) (⇑f : (a : X) → ℝ) x : ℝ)‖ <
      ε
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
x : X
hxK : x ∈ K
eqg :
  Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ)
    ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)
right :
  ‖HSub.hSub (α := ℝ) (β := ℝ) ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)
        ((f : (a : X) → ℝ) x : ℝ)‖ <
    ε
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)‖ < ε

Tactic:
rw [eqg]
-- Module: Mathlib.Topology.ContinuousMap.StoneWeierstrass
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_1 : gK ∈ AK
hgapprox :
  ∀ (x : (↑K : Type u_2)),
    ‖HSub.hSub (α := ℝ) (β := ℝ)
          (((↑(Subtype.mk (p := fun (x : C((↑K : Type u_2), ℝ)) ↦ x ∈ AK) gK hgKAK_1) : C((↑K : Type u_2), ℝ)) :
                (a : (↑K : Type u_2)) → ℝ)
              x :
            ℝ)
          (K.restrict (π := fun (a : X) ↦ ℝ) (⇑f : (a : X) → ℝ) x : ℝ)‖ <
      ε
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
x : X
hxK : x ∈ K
eqg :
  Eq (α := ℝ) ((g : (a : X) → ℝ) x : ℝ)
    ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((gK : (a : (↑K : Type u_2)) → ℝ) (Subtype.mk (p := fun (x : X) ↦ x ∈ K) x hxK) : ℝ)
        ((f : (a : X) → ℝ) x : ℝ)‖ <
    ε

Tactic:
hgapprox ⟨x, hxK⟩

Premises used: Subtype.mk, Set.restrict