𝕜 : Type ?u.66235
E : Type u_1
F : Type ?u.66241
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
⊢ ∑ k in Finset.range (n + 1 + 1),
      ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
        (↑(PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀)) =
    ∑ k in Finset.range (n + 1),
        ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
          (↑(PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀)) +
      ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
        (↑(PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀))
𝕜 : Type ?u.66235
E : Type u_1
F : Type ?u.66241
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
⊢ taylorWithin f (n + 1) s x₀ =
    taylorWithin f n s x₀ +
      ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
        (↑(PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀))
dsimp only [taylorWithin]
no goals
𝕜 : Type ?u.66235
E : Type u_1
F : Type ?u.66241
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
⊢ ∑ k in Finset.range (n + 1 + 1),
      ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
        (↑(PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀)) =
    ∑ k in Finset.range (n + 1),
        ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
          (↑(PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀)) +
      ↑(PolynomialModule.comp (Polynomial.X - ↑Polynomial.C x₀))
        (↑(PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀))
rw [Finset.sum_range_succ]