Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e'_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t) -
      ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f [[x₀, x]] x₀ =
    (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) x • (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x -
        (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) x₀ • (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x₀ -
      ∫ (t : ℝ) in x₀..x,
        deriv (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) t • (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) t

pp: case e'_3
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ ∫ (t : ℝ) in x₀..x, ((x - t) ^ (n + 1) / ((↑n + 1) * ↑n !)) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t =
    ∫ (t : ℝ) in x₀..x,
      (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) t • deriv (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) t

Tactic:
· simp only [sub_self, ne_eq, Nat.add_eq_zero_iff, one_ne_zero, and_false, not_false_eq_true,
        zero_pow, zero_div, zero_smul, zero_sub, deriv_div_const, Nat.factorial]
      apply fun (a b c d : F) (_ : b = c) (_ : a = -d) ↦ show a - b = -c - d by grind
      · grind
      · rw [← intervalIntegral.integral_neg]
        congr
        ext t
        rw [deriv_fun_pow (by fun_prop), deriv_const_sub, deriv_id'', ← neg_smul]
        congr
        field_simp
        grind

Goal state after:
case e'_3
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ ∫ (t : ℝ) in x₀..x, ((x - t) ^ (n + 1) / ((↑n + 1) * ↑n !)) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t =
    ∫ (t : ℝ) in x₀..x,
      (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) t • deriv (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) t