-- Mathlib/Topology/ContinuousMap/Weierstrass.lean
theorem exists_polynomial_near_of_continuousOn (a b : ℝ) (f : ℝ → ℝ)
    (c : ContinuousOn f (Set.Icc a b)) (ε : ℝ) (pos : 0 < ε) :
    ∃ p : ℝ[X], ∀ x ∈ Set.Icc a b, |p.eval x - f x| < ε

Proof state:
a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε

Tactic:
let f' : C(Set.Icc a b, ℝ) := ⟨fun x => f x, continuousOn_iff_continuous_restrict.mp c⟩

Result:
a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }
⊢ ∃ p, ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε

Proof state:
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ‖p.toContinuousMapOn (Set.Icc a b✝) - f'‖ < ε
⊢ ∃ p, ∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε

Tactic:
use p

Result:
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ‖p.toContinuousMapOn (Set.Icc a b✝) - f'‖ < ε
⊢ ∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε

Proof state:
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖(p.toContinuousMapOn (Set.Icc a b✝) - f') x‖ < ε
x : ℝ
m : x ∈ Set.Icc a b✝
⊢ |Polynomial.eval x p - f x| < ε

Tactic:
exact b ⟨x, m⟩

Result:
no goals

Proof state:
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ‖p.toContinuousMapOn (Set.Icc a b✝) - f'‖ < ε
⊢ ∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε

Tactic:
rw [norm_lt_iff _ pos] at b

Result:
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖(p.toContinuousMapOn (Set.Icc a b✝) - f') x‖ < ε
⊢ ∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε

Proof state:
a b : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }
⊢ ∃ p, ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε

Tactic:
obtain ⟨p, b⟩ := exists_polynomial_near_continuousMap a b f' ε pos

Result:
case intro
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ‖p.toContinuousMapOn (Set.Icc a b✝) - f'‖ < ε
⊢ ∃ p, ∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε

Proof state:
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖(p.toContinuousMapOn (Set.Icc a b✝) - f') x‖ < ε
⊢ ∀ x ∈ Set.Icc a b✝, |Polynomial.eval x p - f x| < ε

Tactic:
intro x m

Result:
case h
a b✝ : ℝ
f : ℝ → ℝ
c : ContinuousOn f (Set.Icc a b✝)
ε : ℝ
pos : 0 < ε
f' : C(↑(Set.Icc a b✝), ℝ) := { toFun := fun x => f ↑x, continuous_toFun := ⋯ }
p : ℝ[X]
b : ∀ (x : ↑(Set.Icc a b✝)), ‖(p.toContinuousMapOn (Set.Icc a b✝) - f') x‖ < ε
x : ℝ
m : x ∈ Set.Icc a b✝
⊢ |Polynomial.eval x p - f x| < ε