-- Mathlib/Analysis/Calculus/Taylor.lean
theorem taylorWithinEval_succ (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₀

Proof state:
case e_a
E : Type u_2
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₀

Tactic:
simp only [Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_C,
  PolynomialModule.eval_single, mul_inv_rev]

Result:
case e_a
E : Type u_2
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₀

Proof state:
case e_a
E : Type u_2
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₀

Tactic:
rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
  mul_inv_rev]

Result:
no goals

Proof state:
case e_a
E : Type u_2
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₀

Tactic:
dsimp only [taylorCoeffWithin]

Result:
case e_a
E : Type u_2
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₀

Proof state:
E : Type u_2
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₀

Tactic:
simp_rw [taylorWithinEval, taylorWithin_succ, LinearMap.map_add, PolynomialModule.comp_eval]

Result:
E : Type u_2
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₀

Proof state:
E : Type u_2
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₀

Tactic:
congr

Result:
case e_a
E : Type u_2
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₀