𝕜 : Type ?u.139420
E : Type u_1
F : Type ?u.139426
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ ↑(PolynomialModule.eval x) (taylorWithin f 0 s x₀) = f x₀
𝕜 : Type ?u.139420
E : Type u_1
F : Type ?u.139426
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ taylorWithinEval f 0 s x₀ x = f x₀
dsimp only [taylorWithinEval]
𝕜 : Type ?u.139420
E : Type u_1
F : Type ?u.139426
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ ↑(PolynomialModule.eval x)
      (∑ k in Finset.range (0 + 1),
        ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
          (↑(PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀))) =
    f x₀
𝕜 : Type ?u.139420
E : Type u_1
F : Type ?u.139426
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ ↑(PolynomialModule.eval x) (taylorWithin f 0 s x₀) = f x₀
dsimp only [taylorWithin]
𝕜 : Type ?u.139420
E : Type u_1
F : Type ?u.139426
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ ↑(PolynomialModule.eval x)
      (∑ k in Finset.range (0 + 1),
        ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
          (↑(PolynomialModule.single ℝ k) ((↑k !)⁻¹ • iteratedDerivWithin k f s x₀))) =
    f x₀
𝕜 : Type ?u.139420
E : Type u_1
F : Type ?u.139426
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ ↑(PolynomialModule.eval x)
      (∑ k in Finset.range (0 + 1),
        ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
          (↑(PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀))) =
    f x₀
dsimp only [taylorCoeffWithin]
no goals
𝕜 : Type ?u.139420
E : Type u_1
F : Type ?u.139426
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ ↑(PolynomialModule.eval x)
      (∑ k in Finset.range (0 + 1),
        ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
          (↑(PolynomialModule.single ℝ k) ((↑k !)⁻¹ • iteratedDerivWithin k f s x₀))) =
    f x₀
simp