awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
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
this : UniqueDiffOn ℝ [[x₀, x]]
⊢ ∀ 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

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
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
this : UniqueDiffOn ℝ [[x₀, x]]
⊢ 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:
specialize ih (by grind)
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this : UniqueDiffOn ℝ [[x₀, x]]
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
inr :
  f x -
      (taylorWithinEval f n [[x₀, x]] x₀ x +
        ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) •
          iteratedDerivWithin (n + 1) f [[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 + 1) [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t

Tactic:
simp only [taylorWithinEval_succ, mul_inv_rev]

Premises used: taylorWithinEval_succ, mul_inv_rev
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this : UniqueDiffOn ℝ [[x₀, x]]
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
inr :
  (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t) -
      ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) •
        iteratedDerivWithin (n + 1) f [[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 +
        ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) •
          iteratedDerivWithin (n + 1) f [[x₀, x]] x₀) =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t

Tactic:
rw [sub_add_eq_sub_sub, ih]

Premises used: sub_add_eq_sub_sub
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this : UniqueDiffOn ℝ [[x₀, x]]
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
inr :
  (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t) -
      ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] x₀ =
    ∫ (t : ℝ) in x₀..x,
      ((x - t) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t
⊢ (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t) -
      ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] x₀ =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t

Tactic:
simp only [Nat.factorial, Nat.succ_eq_add_one, Nat.cast_mul, Nat.cast_add, Nat.cast_one]

Premises used: Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_mul, Nat.factorial, Nat.cast_one
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this : UniqueDiffOn ℝ [[x₀, x]]
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
⊢ n + 1 ≤ n + 1

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this : UniqueDiffOn ℝ [[x₀, x]]
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
⊢ let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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

Tactic:
have := hf (n + 1) (by rfl)
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this_2 : UniqueDiffOn ℝ [[x₀, x]]
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
this :
  let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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
⊢ HSMul.hSMul (α := ℝ) (β := F) ((fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) x)
          ((fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x) -
        HSMul.hSMul (α := ℝ) (β := F) ((fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) x₀)
          ((fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x₀) -
      ∫ (t : ℝ) in x₀..x,
        HSMul.hSMul (α := ℝ) (β := F) (deriv (fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) t)
          ((fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) t) =
    ∫ (t : ℝ) in x₀..x,
      HSMul.hSMul (α := ℝ) (β := F) ((fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) t)
        (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) t)

Tactic:
this.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this_2 : UniqueDiffOn ℝ [[x₀, x]]
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
this :
  let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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
h :
  (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t) -
      ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] x₀ =
    HSMul.hSMul (α := ℝ) (β := F) ((fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) x)
          ((fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x) -
        HSMul.hSMul (α := ℝ) (β := F) ((fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) x₀)
          ((fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x₀) -
      ∫ (t : ℝ) in x₀..x,
        HSMul.hSMul (α := ℝ) (β := F) (deriv (fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) t)
          ((fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) t)
h₁ :
  Eq.{u_3 + 1} (α := F)
    (∫ (t : ℝ) in x₀..x,
      ((x - t) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) •
        iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t)
    (∫ (t : ℝ) in x₀..x,
      HSMul.hSMul (α := ℝ) (β := F) ((fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) t)
        (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) t))
⊢ (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t) -
      ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] x₀ =
    ∫ (t : ℝ) in x₀..x,
      ((x - t) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t

Tactic:
convert! this.symm using 1

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this_2 : UniqueDiffOn ℝ [[x₀, x]]
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
this :
  let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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
h :
  (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t) -
      ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] x₀ =
    -(((x - x₀) ^ (n + 1) / (↑(n.succ * n !) : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] x₀) -
      ∫ (t : ℝ) in x₀..x,
        HDiv.hDiv (α := ℝ) (deriv (fun (x_1 : ℝ) ↦ (x - x_1) ^ (n + 1)) t) (↑(n.succ * n !) : ℝ) •
          iteratedDerivWithin (n + 1) f [[x₀, x]] t
⊢ (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t) -
      ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] x₀ =
    HSMul.hSMul (α := ℝ) (β := F) ((fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) x)
          ((fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x) -
        HSMul.hSMul (α := ℝ) (β := F) ((fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) x₀)
          ((fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x₀) -
      ∫ (t : ℝ) in x₀..x,
        HSMul.hSMul (α := ℝ) (β := F) (deriv (fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) t)
          ((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]

Premises used: sub_self, zero_div, ne_eq, zero_smul, Nat.factorial, and_false, one_ne_zero, not_false_eq_true, Nat.add_eq_zero_iff, zero_pow, deriv_div_const, zero_sub
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this_2 : UniqueDiffOn ℝ [[x₀, x]]
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
this :
  let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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
a b c d : F
h : b = c
h_1 : a = -d
⊢ a - b = -c - d

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this_2 : UniqueDiffOn ℝ [[x₀, x]]
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
this :
  let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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
h :
  ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f [[x₀, x]] x₀ =
    ((x - x₀) ^ (n + 1) / (↑(n.succ * n !) : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] x₀
h₁ :
  Eq.{u_3 + 1} (α := F) (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t)
    (-∫ (t : ℝ) in x₀..x,
        HDiv.hDiv (α := ℝ) (deriv (fun (x_1 : ℝ) ↦ (x - x_1) ^ (n + 1)) t) (↑(n.succ * n !) : ℝ) •
          iteratedDerivWithin (n + 1) f [[x₀, x]] t)
⊢ (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t) -
      ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] x₀ =
    -(((x - x₀) ^ (n + 1) / (↑(n.succ * n !) : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] x₀) -
      ∫ (t : ℝ) in x₀..x,
        HDiv.hDiv (α := ℝ) (deriv (fun (x_1 : ℝ) ↦ (x - x_1) ^ (n + 1)) t) (↑(n.succ * n !) : ℝ) •
          iteratedDerivWithin (n + 1) f [[x₀, x]] t

Tactic:
apply fun (a b c d : F) (_ : b = c) (_ : a = -d) ↦ show a - b = -c - d by grind
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this_2 : UniqueDiffOn ℝ [[x₀, x]]
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
this :
  let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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
⊢ ((↑n ! : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f [[x₀, x]] x₀ =
    ((x - x₀) ^ (n + 1) / (↑(n.succ * n !) : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] x₀

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this_2 : UniqueDiffOn ℝ [[x₀, x]]
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
this :
  let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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
h :
  Eq.{u_3 + 1} (α := F) (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t)
    (∫ (x_1 : ℝ) in x₀..x,
      -(HDiv.hDiv (α := ℝ) (deriv (fun (x_2 : ℝ) ↦ (x - x_2) ^ (n + 1)) x_1) (↑(n.succ * n !) : ℝ) •
          iteratedDerivWithin (n + 1) f [[x₀, x]] x_1))
⊢ Eq.{u_3 + 1} (α := F) (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t)
    (-∫ (t : ℝ) in x₀..x,
        HDiv.hDiv (α := ℝ) (deriv (fun (x_1 : ℝ) ↦ (x - x_1) ^ (n + 1)) t) (↑(n.succ * n !) : ℝ) •
          iteratedDerivWithin (n + 1) f [[x₀, x]] t)

Tactic:
rw [← intervalIntegral.integral_neg]

Premises used: intervalIntegral.integral_neg
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this_2 : UniqueDiffOn ℝ [[x₀, x]]
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
this :
  let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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
h :
  Eq.{u_3 + 1} (α := ℝ → F) (fun (t : ℝ) ↦ ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t)
    fun (x_1 : ℝ) ↦
    -(HDiv.hDiv (α := ℝ) (deriv (fun (x_2 : ℝ) ↦ (x - x_2) ^ (n + 1)) x_1) (↑(n.succ * n !) : ℝ) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] x_1)
⊢ Eq.{u_3 + 1} (α := F) (∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t)
    (∫ (x_1 : ℝ) in x₀..x,
      -(HDiv.hDiv (α := ℝ) (deriv (fun (x_2 : ℝ) ↦ (x - x_2) ^ (n + 1)) x_1) (↑(n.succ * n !) : ℝ) •
          iteratedDerivWithin (n + 1) f [[x₀, x]] x_1))

Tactic:
congr
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this_2 : UniqueDiffOn ℝ [[x₀, x]]
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
this :
  let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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
h :
  ∀ (t : ℝ),
    ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t =
      -(HDiv.hDiv (α := ℝ) (deriv (fun (x_1 : ℝ) ↦ (x - x_1) ^ (n + 1)) t) (↑(n.succ * n !) : ℝ) •
          iteratedDerivWithin (n + 1) f [[x₀, x]] t)
⊢ Eq.{u_3 + 1} (α := ℝ → F) (fun (t : ℝ) ↦ ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t)
    fun (x_1 : ℝ) ↦
    -(HDiv.hDiv (α := ℝ) (deriv (fun (x_2 : ℝ) ↦ (x - x_2) ^ (n + 1)) x_1) (↑(n.succ * n !) : ℝ) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] x_1)

Tactic:
ext t
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this_1 : x₀ ≠ x
n : ℕ
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
this_2 : UniqueDiffOn ℝ [[x₀, x]]
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
this :
  let u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ);
  let v : (t : ℝ) → F := 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 : ℝ
⊢ DifferentiableAt ℝ (HSub.hSub x) t

Tactic:
fun_prop