𝕜 : Type ?u.131034
E : Type u_1
F : Type ?u.131040
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ ↑(PolynomialModule.eval x) (taylorWithin f n s x₀) +
      ↑(PolynomialModule.eval (Polynomial.eval x (Polynomial.X - ↑Polynomial.C x₀)))
        (↑(PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀)) =
    ↑(PolynomialModule.eval x) (taylorWithin f n s x₀) +
      (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
𝕜 : Type ?u.131034
E : Type u_1
F : Type ?u.131040
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ taylorWithinEval f (n + 1) s x₀ x =
    taylorWithinEval f n s x₀ x + (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
simp_rw [taylorWithinEval, taylorWithin_succ, LinearMap.map_add, PolynomialModule.comp_eval]
case e_a
𝕜 : Type ?u.131034
E : Type u_1
F : Type ?u.131040
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ ↑(PolynomialModule.eval (Polynomial.eval x (Polynomial.X - ↑Polynomial.C x₀)))
      (↑(PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀)) =
    (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
𝕜 : Type ?u.131034
E : Type u_1
F : Type ?u.131040
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ ↑(PolynomialModule.eval x) (taylorWithin f n s x₀) +
      ↑(PolynomialModule.eval (Polynomial.eval x (Polynomial.X - ↑Polynomial.C x₀)))
        (↑(PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀)) =
    ↑(PolynomialModule.eval x) (taylorWithin f n s x₀) +
      (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
congr
case e_a
𝕜 : Type ?u.131034
E : Type u_1
F : Type ?u.131040
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ (x - x₀) ^ (n + 1) • taylorCoeffWithin f (n + 1) s x₀ =
    ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
case e_a
𝕜 : Type ?u.131034
E : Type u_1
F : Type ?u.131040
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ ↑(PolynomialModule.eval (Polynomial.eval x (Polynomial.X - ↑Polynomial.C x₀)))
      (↑(PolynomialModule.single ℝ (n + 1)) (taylorCoeffWithin f (n + 1) s x₀)) =
    (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
simp only [Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_C,
  PolynomialModule.eval_single, mul_inv_rev]
case e_a
𝕜 : Type ?u.131034
E : Type u_1
F : Type ?u.131040
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ (x - x₀) ^ (n + 1) • (↑(n + 1)!)⁻¹ • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
case e_a
𝕜 : Type ?u.131034
E : Type u_1
F : Type ?u.131040
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ (x - x₀) ^ (n + 1) • taylorCoeffWithin f (n + 1) s x₀ =
    ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
dsimp only [taylorCoeffWithin]
no goals
case e_a
𝕜 : Type ?u.131034
E : Type u_1
F : Type ?u.131040
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ (x - x₀) ^ (n + 1) • (↑(n + 1)!)⁻¹ • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
  mul_inv_rev]