awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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 + 1) [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ (n + 1) / (↑(n + 1)! : ℝ)) • iteratedDerivWithin (n + 1 + 1) f [[x₀, x]] t
have 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
Tactic: specialize ih (by grind)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ 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
have 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
Tactic: simp only [taylorWithinEval_succ, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ 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
have 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
Tactic: rw [sub_add_eq_sub_sub, ih]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ (∫ (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
have 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
Tactic: simp only [Nat.factorial, Nat.succ_eq_add_one, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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
⊢ (∫ (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
have 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
Tactic: have := hf (n + 1) (by rfl)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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 : ℝ) 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
have 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)
Tactic: convert! this.symm using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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)
⊢ (∫ (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
have 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))
Tactic: convert! this.symm using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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 : ℝ) 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)
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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 : ℝ) 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
have 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₀
Tactic: apply fun (a b c d : F) (_ : b = c) (_ : a = -d) ↦ show a - b = -c - d by grind
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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₀
⊢ (∫ (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
have 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)
Tactic: apply fun (a b c d : F) (_ : b = c) (_ : a = -d) ↦ show a - b = -c - d by grind
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ 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)
have 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))
Tactic: rw [← intervalIntegral.integral_neg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ 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)
have 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)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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 ! : ℝ)) • 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)
have 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
Tactic: rw [deriv_fun_pow (by fun_prop), deriv_const_sub, deriv_id'', ← neg_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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 ! : ℝ)) • 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
have h : (x - t) ^ n / (↑n ! : ℝ) =
  -((↑(n + 1) : ℝ) * (x - t) ^ (n + 1 - 1) * -(fun (x : ℝ) ↦ (1 : ℝ)) t / (↑(n.succ * n !) : ℝ))
Tactic: congr