case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
g : ℝ[X]
a✝ : X
⊢ ↑(comp (Polynomial.toContinuousMapOn g (Set.Icc (-‖f‖) ‖f‖)) (attachBound ↑f)) a✝ = ↑↑(↑(Polynomial.aeval f) g) a✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
g : ℝ[X]
⊢ comp (Polynomial.toContinuousMapOn g (Set.Icc (-‖f‖) ‖f‖)) (attachBound ↑f) = ↑(↑(Polynomial.aeval f) g)
ext
no goals
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
g : ℝ[X]
a✝ : X
⊢ ↑(comp (Polynomial.toContinuousMapOn g (Set.Icc (-‖f‖) ‖f‖)) (attachBound ↑f)) a✝ = ↑↑(↑(Polynomial.aeval f) g) a✝
simp only [ContinuousMap.coe_comp, Function.comp_apply, ContinuousMap.attachBound_apply_coe,
  Polynomial.toContinuousMapOn_apply, Polynomial.aeval_subalgebra_coe,
  Polynomial.aeval_continuousMap_apply, Polynomial.toContinuousMap_apply]