awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ! : ℝ) =
    -((↑(n + 1) : ℝ) * (x - t) ^ (n + 1 - 1) * -(fun (x : ℝ) ↦ (1 : ℝ)) t / (↑(n.succ * n !) : ℝ))
have h : (x - t) ^ n * (↑(n.succ * n !) : ℝ) = HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑(n + 1) : ℝ) * (x - t) ^ (n + 1 - 1)
Tactic: field_simp
-- 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 + 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))
have 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)
Tactic: apply intervalIntegral.integral_congr_ae
-- 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
⊢ ∀ᵐ (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)
have 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)
Tactic: filter_upwards [MeasureTheory.volume.ae_ne x₀, MeasureTheory.volume.ae_ne x] with _ _ _ _
-- 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
a : ℝ
h : a ≠ x₀
h_1 : a ≠ x
h_2 : 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)
have 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)
Tactic: rw [iteratedDerivWithin_succ]
-- 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
a : ℝ
h : a ≠ x₀
h_1 : a ≠ x
h_2 : a ∈ Ι x₀ x
⊢ ((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)
have h : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ) = (↑(n + 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
a : ℝ
h_1 : a ≠ x₀
h_2 : a ≠ x
h_3 : a ∈ Ι x₀ x
h : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n ! : ℝ) = (↑(n + 1)! : ℝ)
⊢ ((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)
have h₁ : derivWithin (iteratedDerivWithin (n + 1) f [[x₀, x]]) [[x₀, x]] a =
  deriv (fun (t : ℝ) ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) a
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₀ : ℝ
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
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / (↑n ! : ℝ)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
have 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
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]
Cleared hypotheses: n, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x 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
have 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
Tactic: rcases eq_or_ne x₀ x with rfl | this
Cleared hypotheses: x, hf₁, hf₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, (x - t) ^ n / (↑n ! : ℝ) * iteratedDerivWithin (n + 1) f [[x₀, x]] t
have 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
Tactic: rcases eq_or_ne x₀ x with rfl | this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
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
have 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
Tactic: apply taylor_integral_remainder_aux
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ 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
have inr : AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) x₀ x
Tactic: apply AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ 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
have inr₁ : AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x
Tactic: apply AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) x₀ x
have inr : ContDiffOn ℝ (F := ℝ) 1 (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
Tactic: apply ContDiffOn.absolutelyContinuousOnInterval
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x
have 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
Tactic: rcases hk.eq_or_lt with rfl | hk
Cleared hypotheses: n, hf₁, hf₂, hk
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x
have inr₁ : ∀ (hk : k < n), AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x
Tactic: rcases hk.eq_or_lt with rfl | hk
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x
have this₁ : UniqueDiffOn ℝ [[x₀, x]]
Tactic: have : UniqueDiffOn ℝ [[x₀, x]] := uniqueDiffOn_Icc (by grind)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
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]]
⊢ LE.le (α := WithTop ℕ∞) (↑k.succ : WithTop ℕ∞) (↑n : WithTop ℕ∞)
have norm_cast : k.succ ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
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]]
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x
have hf₃ : ContDiffOn ℝ (↑k.succ : WithTop ℕ∞) f [[x₀, x]]
Tactic: replace hf₁ := hf₁.of_le (m := k.succ) (by norm_cast)
Cleared hypotheses: hf₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[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
have inl : ∀ (hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[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: rcases eq_or_ne x₀ x with rfl | this
Cleared hypotheses: x, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
inl :
  ∀ (hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[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
have 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
Tactic: rcases eq_or_ne x₀ x with rfl | this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
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
have this₁ : UniqueDiffOn ℝ [[x₀, x]]
Tactic: have : UniqueDiffOn ℝ [[x₀, x]] := uniqueDiffOn_Icc (by grind)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
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
have inr : ∀ k ≤ n,
  have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
  have 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: apply taylor_integral_remainder_aux
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
  have 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
have inr : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
Tactic: apply intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt
    (u := fun t ↦ (x - t) ^ k / k !) (v := fun t ↦ iteratedDerivWithin k f (uIcc x₀ x) t)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
inr : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
⊢ have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
  have 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
have inr₁ : ContinuousOn.{0, u_3} (Y := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) [[x₀, x]]
Tactic: apply intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt
    (u := fun t ↦ (x - t) ^ k / k !) (v := fun t ↦ iteratedDerivWithin k f (uIcc x₀ x) t)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
inr : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
inr₁ : ContinuousOn.{0, u_3} (Y := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) [[x₀, x]]
⊢ have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
  have 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
have inr₂ : ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
  HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) (deriv (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) x_1) x_1
Tactic: apply intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt
    (u := fun t ↦ (x - t) ^ k / k !) (v := fun t ↦ iteratedDerivWithin k f (uIcc x₀ x) t)