-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf :
  ∀ k ≤ n,
    let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
    let v : (t : ℝ) → F := 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 : x₀ ≠ x
inr :
  ∀
    (hf :
      ∀ k ≤ 0,
        let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
        let v : (t : ℝ) → F := 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),
    f x - taylorWithinEval f 0 [[x₀, x]] x₀ x =
      ∫ (t : ℝ) in x₀..x,
        (HPow.hPow (β := ℕ) (x - t) 0 / (↑0! : ℝ)) • iteratedDerivWithin (HAdd.hAdd (α := ℕ) 0 1) f [[x₀, x]] t
inr₁ :
  ∀ (n : ℕ)
    (ih :
      ∀
        (hf :
          ∀ k ≤ n,
            let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
            let v : (t : ℝ) → F := 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),
        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 : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
        let v : (t : ℝ) → F := 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),
    f x - taylorWithinEval f (n + 1) [[x₀, x]] x₀ x =
      ∫ (t : ℝ) in x₀..x, ((x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t

Tactic:
induction n with
  | zero =>
    simp only [taylor_within_zero_eval, pow_zero, Nat.factorial_zero, Nat.cast_one, ne_eq,
      one_ne_zero, not_false_eq_true, div_self, zero_add, iteratedDerivWithin_one, one_smul]
    simp only [nonpos_iff_eq_zero, sub_self, deriv_div_const, forall_eq, pow_zero,
      Nat.factorial_zero, Nat.cast_one, ne_eq, one_ne_zero, not_false_eq_true, div_self,
      iteratedDerivWithin_zero, one_smul, deriv_const', div_one, zero_smul,
      intervalIntegral.integral_zero, sub_zero] at hf
    rw [← hf]
    apply intervalIntegral.integral_congr_ae
    filter_upwards [MeasureTheory.volume.ae_ne x₀, MeasureTheory.volume.ae_ne x] with _ _ _ _
    grind [derivWithin_of_mem_nhds, Icc_mem_nhds, uIcc]
  | succ n ih =>
    have : UniqueDiffOn ℝ [[x₀, x]] := uniqueDiffOn_Icc (by grind)
    specialize ih (by grind)
    simp only [taylorWithinEval_succ, mul_inv_rev]
    rw [sub_add_eq_sub_sub, ih]
    simp only [Nat.factorial, Nat.succ_eq_add_one, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
    have := hf (n + 1) (by rfl)
    convert! this.symm using 1
    · 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
    · apply intervalIntegral.integral_congr_ae
      filter_upwards [MeasureTheory.volume.ae_ne x₀, MeasureTheory.volume.ae_ne x] with _ _ _ _
      rw [iteratedDerivWithin_succ]
      congr
      · rw [Nat.factorial]; grind
      · grind [derivWithin_of_mem_nhds, Icc_mem_nhds, uIcc]

Premises used: neg_smul, MeasureTheory.Measure.ae_ne, Nat.succ_eq_add_one, deriv_const', sub_self, sub_zero, iteratedDerivWithin_one, taylor_within_zero_eval, deriv_id'', zero_div, forall_eq, Ne.symm, iteratedDerivWithin_zero, taylorWithinEval_succ, zero_add, ne_eq, pow_zero, one_smul, Nat.cast_add, zero_smul, sub_add_eq_sub_sub, Nat.cast_mul, MeasureTheory.MeasureSpace.volume, Nat.factorial, intervalIntegral.integral_zero, iteratedDerivWithin_succ, Nat.factorial_zero, mul_inv_rev, and_false, deriv_fun_pow, intervalIntegral.integral_congr_ae, one_ne_zero, not_false_eq_true, div_one, Nat.cast_one, Nat.add_eq_zero_iff, Set.uIcc, zero_pow, intervalIntegral.integral_neg, div_self, deriv_const_sub, derivWithin_of_mem_nhds, deriv_div_const, zero_sub, nonpos_iff_eq_zero, Icc_mem_nhds