-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints
    {X : Type*} [TopologicalSpace X] {A : Subalgebra ℝ C(X, ℝ)} (hA : A.SeparatesPoints)
    (f : C(X, ℝ)) {K : Set X} (hK : IsCompact K) {ε : ℝ} (pos : 0 < ε) :
    ∃ g ∈ A, ∀ x ∈ K, ‖(g : X → ℝ) x - f x‖ < ε

Proof state:
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
x y : ↑K
hxy : x ≠ y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑AK, f x ≠ f y

Tactic:
obtain ⟨_, ⟨g, hg1, hg2⟩, hg_sep⟩ := hA (Subtype.coe_ne_coe.mpr hxy)

Result:
case intro.intro.intro.intro
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
x y : ↑K
hxy : x ≠ y
w✝ : X → ℝ
hg_sep : w✝ ↑x ≠ w✝ ↑y
g : C(X, ℝ)
hg1 : g ∈ ↑A
hg2 : (fun f => ⇑f) g = w✝
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑AK, f x ≠ f y

Proof state:
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
x y : ↑K
hxy : x ≠ y
w✝ : X → ℝ
hg_sep : w✝ ↑x ≠ w✝ ↑y
g : C(X, ℝ)
hg1 : g ∈ ↑A
hg2 : (fun f => ⇑f) g = w✝
⊢ (restrict_on_K g) x ≠ (restrict_on_K g) y

Tactic:
simpa only [compStarAlgHom'_apply, comp_apply, coe_mk, ne_eq, restrict_on_K, hg2]

Result:
no goals

Proof state:
case h
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
x y : ↑K
hxy : x ≠ y
w✝ : X → ℝ
hg_sep : w✝ ↑x ≠ w✝ ↑y
g : C(X, ℝ)
hg1 : g ∈ ↑A
hg2 : (fun f => ⇑f) g = w✝
⊢ ∃ x ∈ A, ↑restrict_on_K x = restrict_on_K g

Tactic:
use g, hg1

Result:
case right
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
x y : ↑K
hxy : x ≠ y
w✝ : X → ℝ
hg_sep : w✝ ↑x ≠ w✝ ↑y
g : C(X, ℝ)
hg1 : g ∈ ↑A
hg2 : (fun f => ⇑f) g = w✝
⊢ ↑restrict_on_K g = restrict_on_K g

Proof state:
case right
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
x y : ↑K
hxy : x ≠ y
w✝ : X → ℝ
hg_sep : w✝ ↑x ≠ w✝ ↑y
g : C(X, ℝ)
hg1 : g ∈ ↑A
hg2 : (fun f => ⇑f) g = w✝
⊢ ↑restrict_on_K g = restrict_on_K g

Tactic:
simp [AlgHom.coe_coe]

Result:
no goals

Proof state:
case intro.mk.intro.intro
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
gK : C(↑K, ℝ)
hgKAK✝ : gK ∈ AK
hgapprox : ∀ (x : ↑K), ‖↑⟨gK, hgKAK✝⟩ x - K.restrict (⇑f) x‖ < ε
g : C(X, ℝ)
hgA : g ∈ A
hgKAK : ↑restrict_on_K g = gK
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε

Tactic:
use g, hgA

Result:
case right
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
gK : C(↑K, ℝ)
hgKAK✝ : gK ∈ AK
hgapprox : ∀ (x : ↑K), ‖↑⟨gK, hgKAK✝⟩ x - K.restrict (⇑f) x‖ < ε
g : C(X, ℝ)
hgA : g ∈ A
hgKAK : ↑restrict_on_K g = gK
⊢ ∀ x ∈ K, ‖g x - f x‖ < ε

Proof state:
case h
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
x y : ↑K
hxy : x ≠ y
w✝ : X → ℝ
hg_sep : w✝ ↑x ≠ w✝ ↑y
g : C(X, ℝ)
hg1 : g ∈ ↑A
hg2 : (fun f => ⇑f) g = w✝
⊢ restrict_on_K g ∈ AK ∧ (restrict_on_K g) x ≠ (restrict_on_K g) y

Tactic:
refine ⟨Subalgebra.mem_map.mpr ?_,
  by simpa only [compStarAlgHom'_apply, comp_apply, coe_mk, ne_eq, restrict_on_K, hg2]⟩

Result:
case h
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
x y : ↑K
hxy : x ≠ y
w✝ : X → ℝ
hg_sep : w✝ ↑x ≠ w✝ ↑y
g : C(X, ℝ)
hg1 : g ∈ ↑A
hg2 : (fun f => ⇑f) g = w✝
⊢ ∃ x ∈ A, ↑restrict_on_K x = restrict_on_K g

Proof state:
case right
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
gK : C(↑K, ℝ)
hgKAK✝ : gK ∈ AK
hgapprox : ∀ (x : ↑K), ‖↑⟨gK, hgKAK✝⟩ x - K.restrict (⇑f) x‖ < ε
g : C(X, ℝ)
hgA : g ∈ A
hgKAK : ↑restrict_on_K g = gK
⊢ ∀ x ∈ K, ‖g x - f x‖ < ε

Tactic:
intro x hxK

Result:
case right
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
AK : Subalgebra ℝ C(↑K, ℝ) := Subalgebra.map (↑restrict_on_K) A
hsep : AK.SeparatesPoints
gK : C(↑K, ℝ)
hgKAK✝ : gK ∈ AK
hgapprox : ∀ (x : ↑K), ‖↑⟨gK, hgKAK✝⟩ x - K.restrict (⇑f) x‖ < ε
g : C(X, ℝ)
hgA : g ∈ A
hgKAK : ↑restrict_on_K g = gK
x : X
hxK : x ∈ K
⊢ ‖g x - f x‖ < ε

Proof state:
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 < ε
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε

Tactic:
let restrict_on_K : C(X, ℝ) →⋆ₐ[ℝ] C(K, ℝ) :=
  ContinuousMap.compStarAlgHom' ℝ ℝ ⟨(Subtype.val), continuous_subtype_val⟩

Result:
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, ℝ) := compStarAlgHom' ℝ ℝ { toFun := Subtype.val, continuous_toFun := ⋯ }
⊢ ∃ g ∈ A, ∀ x ∈ K, ‖g x - f x‖ < ε