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 : ℕ
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 : ℝ
h :
  ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t =
    -((↑(n + 1) : ℝ) * (x - t) ^ (n + 1 - 1) * -(fun (x : ℝ) ↦ (1 : ℝ)) t / (↑(n.succ * n !) : ℝ)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] 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)

Tactic:
rw [deriv_fun_pow (by fun_prop), deriv_const_sub, deriv_id'', ← neg_smul]

Premises used: neg_smul, deriv_id'', deriv_fun_pow, deriv_const_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
t : ℝ
h :
  (x - t) ^ n / (↑n ! : ℝ) =
    -((↑(n + 1) : ℝ) * (x - t) ^ (n + 1 - 1) * -(fun (x : ℝ) ↦ (1 : ℝ)) t / (↑(n.succ * n !) : ℝ))
⊢ ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t =
    -((↑(n + 1) : ℝ) * (x - t) ^ (n + 1 - 1) * -(fun (x : ℝ) ↦ (1 : ℝ)) t / (↑(n.succ * n !) : ℝ)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] t

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
t : ℝ
h : (x - t) ^ n * (↑(n.succ * n !) : ℝ) = HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑(n + 1) : ℝ) * (x - t) ^ (n + 1 - 1)
⊢ (x - t) ^ n / (↑n ! : ℝ) =
    -((↑(n + 1) : ℝ) * (x - t) ^ (n + 1 - 1) * -(fun (x : ℝ) ↦ (1 : ℝ)) t / (↑(n.succ * n !) : ℝ))

Tactic:
field_simp
-- 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 : ℝ
⊢ (x - t) ^ n * (↑(n.succ * n !) : ℝ) = HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑(n + 1) : ℝ) * (x - t) ^ (n + 1 - 1)

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 :
  ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Ι x₀ x →
      ((x - x_1) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) •
          iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] x_1 =
        HSMul.hSMul (α := ℝ) (β := F) ((fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) x_1)
          (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x_1)
⊢ 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))

Tactic:
apply intervalIntegral.integral_congr_ae

Premises used: intervalIntegral.integral_congr_ae
-- 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 : ℝ
h :
  a ≠ x₀ →
    a ≠ x →
      a ∈ Ι x₀ x →
        ((x - a) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) •
            iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] a =
          HSMul.hSMul (β := F) ((x - a) ^ (n + 1) / (↑(n + 1)! : ℝ))
            (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a)
⊢ a ≠ x₀ →
    a ≠ x →
      a ∈ Ι x₀ x →
        ((x - a) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) •
            iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] a =
          HSMul.hSMul (β := F) ((x - a) ^ (n + 1) / (↑(n + 1)! : ℝ))
            (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a)

Tactic:
_
-- 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 : ℝ
h_1 : a ≠ x₀
h :
  a ≠ x →
    a ∈ Ι x₀ x →
      ((x - a) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) •
          iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] a =
        HSMul.hSMul (β := F) ((x - a) ^ (n + 1) / (↑(n + 1)! : ℝ))
          (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a)
⊢ a ≠ x →
    a ∈ Ι x₀ x →
      ((x - a) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) •
          iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] a =
        HSMul.hSMul (β := F) ((x - a) ^ (n + 1) / (↑(n + 1)! : ℝ))
          (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a)

Tactic:
_
-- 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 : ℝ
h_1 : a ≠ x₀
h_2 : a ≠ x
h :
  a ∈ Ι x₀ x →
    ((x - a) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] a =
      HSMul.hSMul (β := F) ((x - a) ^ (n + 1) / (↑(n + 1)! : ℝ))
        (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a)
⊢ a ∈ Ι x₀ x →
    ((x - a) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] a =
      HSMul.hSMul (β := F) ((x - a) ^ (n + 1) / (↑(n + 1)! : ℝ))
        (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a)

Tactic:
_
-- 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 :
  ∀ (a : ℝ),
    a ≠ x₀ →
      a ≠ x →
        a ∈ Ι x₀ x →
          ((x - a) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) •
              iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] a =
            HSMul.hSMul (β := F) ((x - a) ^ (n + 1) / (↑(n + 1)! : ℝ))
              (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a)
⊢ ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Ι x₀ x →
      ((x - x_1) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) •
          iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] x_1 =
        HSMul.hSMul (α := ℝ) (β := F) ((fun (t : ℝ) ↦ (x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) x_1)
          (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x_1)

Tactic:
filter_upwards [MeasureTheory.volume.ae_ne x₀, MeasureTheory.volume.ae_ne x] with _ _ _ _

Premises used: MeasureTheory.Measure.ae_ne, MeasureTheory.MeasureSpace.volume
-- 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 : ℝ
h_1 : a ≠ x₀
h_2 : a ≠ x
h_3 : a ∈ Ι x₀ x
h :
  ((x - a) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) •
      derivWithin (iteratedDerivWithin (n + 1) f [[x₀, x]]) [[x₀, x]] a =
    HSMul.hSMul (β := F) ((x - a) ^ (n + 1) / (↑(n + 1)! : ℝ))
      (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a)
⊢ ((x - a) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] a =
    HSMul.hSMul (β := F) ((x - a) ^ (n + 1) / (↑(n + 1)! : ℝ))
      (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a)

Tactic:
rw [iteratedDerivWithin_succ]

Premises used: iteratedDerivWithin_succ
-- 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 : ℝ
h_1 : a ≠ x₀
h_2 : a ≠ x
h_3 : a ∈ Ι x₀ x
h : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ) = (↑(n + 1)! : ℝ)
h₁ :
  derivWithin (iteratedDerivWithin (n + 1) f [[x₀, x]]) [[x₀, x]] a =
    deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a
⊢ ((x - a) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ))) •
      derivWithin (iteratedDerivWithin (n + 1) f [[x₀, x]]) [[x₀, x]] a =
    HSMul.hSMul (β := F) ((x - a) ^ (n + 1) / (↑(n + 1)! : ℝ))
      (deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a)

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
a : ℝ
h : a ≠ x₀
h_1 : a ≠ x
h_2 : a ∈ Ι x₀ x
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ) = (↑(n.succ * n !) : ℝ)

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
a : ℝ
h : a ≠ x₀
h_1 : a ≠ x
h_2 : a ∈ Ι x₀ x
⊢ derivWithin (iteratedDerivWithin (n + 1) f [[x₀, x]]) [[x₀, x]] a =
    deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a

Tactic:
grind [derivWithin_of_mem_nhds, Icc_mem_nhds, uIcc]

Premises used: Set.uIcc, derivWithin_of_mem_nhds, Icc_mem_nhds
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
inl :
  ∀ (hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x₀]])
    (hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x₀]]) 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
inr :
  ∀ (this : 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
⊢ 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:
rcases eq_or_ne x₀ x with rfl | this

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x₀]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x₀]]) 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:
simp
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this : x₀ ≠ x
inr :
  ∀ k ≤ n,
    have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
    have v : (t : ℝ) → ℝ := 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

Tactic:
apply taylor_integral_remainder_aux

Premises used: taylor_integral_remainder_aux
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this : x₀ ≠ x
k : ℕ
hk : k ≤ n
inr : AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) x₀ x
inr₁ : AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x
⊢ have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
  have v : (t : ℝ) → ℝ := 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:
apply AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul

Premises used: AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this : x₀ ≠ x
k : ℕ
hk : k ≤ n
inr : ContDiffOn ℝ (F := ℝ) 1 (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) x₀ x

Tactic:
apply ContDiffOn.absolutelyContinuousOnInterval

Premises used: ContDiffOn.absolutelyContinuousOnInterval
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this : x₀ ≠ x
k : ℕ
hk : k ≤ n
⊢ ContDiffOn ℝ (F := ℝ) 1 (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this : x₀ ≠ x
k : ℕ
hk : k ≤ n
inr :
  ∀ (hf₁ : ContDiffOn ℝ (↑k : WithTop ℕ∞) f [[x₀, x]])
    (hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin k f [[x₀, x]]) x₀ x) (hk : k ≤ k),
    AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x
inr₁ : ∀ (hk : k < n), AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x

Tactic:
rcases hk.eq_or_lt with rfl | hk

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
this : x₀ ≠ x
k : ℕ
hf₁ : ContDiffOn ℝ (↑k : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin k f [[x₀, x]]) x₀ x
hk : k ≤ k
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x

Tactic:
hf₂
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
this : x₀ ≠ x
k : ℕ
hf₁ : ContDiffOn ℝ (↑k : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin k f [[x₀, x]]) x₀ x
hk : k ≤ k
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x

Tactic:
exact hf₂
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this : x₀ ≠ x
k : ℕ
hk_1 : k ≤ n
hk : k < n
⊢ min x₀ x < max x₀ x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this : x₀ ≠ x
k : ℕ
hk_1 : k ≤ n
hk : k < n
⊢ UniqueDiffOn ℝ [[x₀, x]]

Tactic:
have : UniqueDiffOn ℝ [[x₀, x]] := uniqueDiffOn_Icc (by grind)
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this_1 : x₀ ≠ x
k : ℕ
hk_1 : k ≤ n
hk : k < n
this : UniqueDiffOn ℝ [[x₀, x]]
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : k.succ ≤ n
⊢ LE.le (α := WithTop ℕ∞) (↑k.succ : WithTop ℕ∞) (↑n : WithTop ℕ∞)

Tactic:
norm_cast