awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
⊢ Filter.Tendsto.{0, u_2} (β := E) (fun (x : ℝ) ↦ ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (𝓝[s] x₀)
    (𝓝 0)
have h_isLittleO : Asymptotics.IsLittleO (E := ℝ) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ ‖f x - taylorWithinEval f n s x₀ x‖) fun (x : ℝ) ↦
  ‖(x - x₀) ^ n‖
Tactic: have h_isLittleO := (taylor_isLittleO hs hx₀s hf).norm_norm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
h_isLittleO :
  Asymptotics.IsLittleO (E := ℝ) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ ‖f x - taylorWithinEval f n s x₀ x‖) fun (x : ℝ) ↦
    ‖(x - x₀) ^ n‖
⊢ Filter.Tendsto.{0, u_2} (β := E) (fun (x : ℝ) ↦ ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (𝓝[s] x₀)
    (𝓝 0)
have rw : ∀
  (h_isLittleO :
    Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x - taylorWithinEval f n s x₀ x‖ / ‖(x - x₀) ^ n‖) (𝓝[s] x₀) (𝓝 0)),
  Filter.Tendsto.{0, u_2} (β := E) (fun (x : ℝ) ↦ ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (𝓝[s] x₀)
    (𝓝 0)
Tactic: rw [Asymptotics.isLittleO_iff_tendsto] at h_isLittleO
Cleared hypotheses: h_isLittleO
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
h_isLittleO :
  Asymptotics.IsLittleO (E := ℝ) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ ‖f x - taylorWithinEval f n s x₀ x‖) fun (x : ℝ) ↦
    ‖(x - x₀) ^ n‖
rw :
  ∀
    (h_isLittleO :
      Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x - taylorWithinEval f n s x₀ x‖ / ‖(x - x₀) ^ n‖) (𝓝[s] x₀) (𝓝 0)),
    Filter.Tendsto.{0, u_2} (β := E) (fun (x : ℝ) ↦ ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (𝓝[s] x₀)
      (𝓝 0)
⊢ Filter.Tendsto.{0, u_2} (β := E) (fun (x : ℝ) ↦ ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (𝓝[s] x₀)
    (𝓝 0)
have rw₁ : ∀ (x : ℝ), ‖(x - x₀) ^ n‖ = 0 → ‖f x - taylorWithinEval f n s x₀ x‖ = 0
Tactic: rw [Asymptotics.isLittleO_iff_tendsto] at h_isLittleO
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
h_isLittleO :
  Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖f x - taylorWithinEval f n s x₀ x‖ / ‖(x - x₀) ^ n‖) (𝓝[s] x₀) (𝓝 0)
⊢ Filter.Tendsto.{0, u_2} (β := E) (fun (x : ℝ) ↦ ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (𝓝[s] x₀)
    (𝓝 0)
have rw : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)‖) (𝓝[s] x₀) (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
h_isLittleO :
  Asymptotics.IsLittleO (E := ℝ) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ ‖f x - taylorWithinEval f n s x₀ x‖) fun (x : ℝ) ↦
    ‖(x - x₀) ^ n‖
⊢ ∀ (x : ℝ), ‖(x - x₀) ^ n‖ = 0 → ‖f x - taylorWithinEval f n s x₀ x‖ = 0
have simp : ∀ (x : ℝ), x - x₀ = 0 → ¬n = 0 → f x - taylorWithinEval f n s x₀ x = 0
Tactic: simp only [norm_pow, Real.norm_eq_abs, pow_eq_zero_iff', abs_eq_zero, ne_eq, norm_eq_zero,
      and_imp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
h_isLittleO :
  Asymptotics.IsLittleO (E := ℝ) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ ‖f x - taylorWithinEval f n s x₀ x‖) fun (x : ℝ) ↦
    ‖(x - x₀) ^ n‖
x : ℝ
hx : x - x₀ = 0
⊢ ¬n = 0 → f x - taylorWithinEval f n s x₀ x = 0
have hx₁ : x = x₀
Tactic: rw [sub_eq_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ (f x - taylorWithinEval f n s x₀ x) / (x - x₀) ^ n) (𝓝[s] x₀) (𝓝 0)
have h : ∀ (x : ℝ), (f x - taylorWithinEval f n s x₀ x) / (x - x₀) ^ n = ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)
Tactic: convert! _root_.taylor_tendsto hs hx₀s hf using 2 with x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn g [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ((x - x') ^ n / (↑n ! : ℝ) * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f [[x₀, x]] x'
have hx₁ : min x₀ x < max x₀ x
Tactic: have hx₁ : min x₀ x < max x₀ x := by grind
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn g [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₁ : min x₀ x < max x₀ x
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ((x - x') ^ n / (↑n ! : ℝ) * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f [[x₀, x]] x'
have rcases : ∀ (y : ℝ) (hy : y ∈ Ioo (min x₀ x) (max x₀ x))
  (h :
    (g (max x₀ x) - g (min x₀ x)) * ((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f [[x₀, x]] y =
      (taylorWithinEval f n [[x₀, x]] (max x₀ x) x - taylorWithinEval f n [[x₀, x]] (min x₀ x) x) * g' y),
  ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ((x - x') ^ n / (↑n ! : ℝ) * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f [[x₀, x]] x'
Tactic: rcases exists_ratio_hasDerivAt_eq_ratio_slope (fun t => taylorWithinEval f n (uIcc x₀ x) t x)
      (fun t => ((n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (uIcc x₀ x) t) hx₁
      (continuousOn_taylorWithinEval (uniqueDiffOn_Icc hx₁) hf)
      (fun _ hy => taylorWithinEval_hasDerivAt_Ioo x hx₁ hy hf hf')
    g g' gcont gdiff with ⟨y, hy, h⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn g [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₁ : min x₀ x < max x₀ x
y : ℝ
hy : y ∈ Ioo (min x₀ x) (max x₀ x)
h :
  (g (max x₀ x) - g (min x₀ x)) * ((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f [[x₀, x]] y =
    (taylorWithinEval f n [[x₀, x]] (max x₀ x) x - taylorWithinEval f n [[x₀, x]] (min x₀ x) x) * g' y
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ((x - x') ^ n / (↑n ! : ℝ) * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f [[x₀, x]] x'
have right : f x - taylorWithinEval f n [[x₀, x]] x₀ x =
  ((x - y) ^ n / (↑n ! : ℝ) * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
Tactic: use y, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
Tactic: have gcont : ContinuousOn (fun t : ℝ => (x - t) ^ (n + 1)) (uIcc x₀ x) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
Tactic: have xy_ne : ∀ y : ℝ, y ∈ uIoo x₀ x → (x - y) ^ n ≠ 0 := by grind [uIoo, pow_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have hg' : ∀ y ∈ uIoo x₀ x, -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n ≠ 0
Tactic: have hg' : ∀ y : ℝ, y ∈ uIoo x₀ x → -(↑n + 1) * (x - y) ^ n ≠ 0 := fun y hy =>
    mul_ne_zero (neg_ne_zero.mpr (Nat.cast_add_one_ne_zero n)) (xy_ne y hy)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n ≠ 0
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have rcases : ∀ (y : ℝ) (hy : y ∈ uIoo x₀ x)
  (h :
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ((x - y) ^ n / (↑n ! : ℝ) * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) /
          (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
        iteratedDerivWithin (n + 1) f [[x₀, x]] y),
  ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
Tactic: rcases taylor_mean_remainder hx hf hf' gcont (fun y _ => monomial_has_deriv_aux y x _) hg' with
    ⟨y, hy, h⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / (↑n ! : ℝ) * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) /
        (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have right : f x - taylorWithinEval f n [[x₀, x]] x₀ x =
  iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
Tactic: use y, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / (↑n ! : ℝ) * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) /
        (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have h₁ : f x - taylorWithinEval f n [[x₀, x]] x₀ x =
  (-((x - y) ^ n / (↑n ! : ℝ) * (x - x₀) ^ (n + 1)) / (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
    iteratedDerivWithin (n + 1) f [[x₀, x]] y
Tactic: simp only [sub_self, zero_pow, Ne, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    (-((x - y) ^ n / (↑n ! : ℝ) * (x - x₀) ^ (n + 1)) / (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have right : ((x - y) ^ n / (↑n ! : ℝ) * (x - x₀) ^ (n + 1) / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (x - y) ^ n)) •
    iteratedDerivWithin (n + 1) f [[x₀, x]] y =
  iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
Tactic: rw [h, neg_div, ← div_neg, neg_mul, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have hu : UniqueDiffOn ℝ [[x₀, x]]
Tactic: have hu : UniqueDiffOn ℝ (uIcc x₀ x) := uniqueDiffOn_Icc (by grind)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
⊢ DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
have refine : (↑n : WithTop ℕ∞) < HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1
Tactic: refine hf.differentiableOn_iteratedDerivWithin ?_ hu
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
⊢ (↑n : WithTop ℕ∞) < HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1
have norm_cast : n < n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
Tactic: have hd : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIcc x₀ x) := by
    refine hf.differentiableOn_iteratedDerivWithin ?_ hu
    norm_cast
    simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have obtain : ∀ (x' : ℝ) (h1 : x' ∈ uIoo x₀ x)
  (h2 :
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)),
  ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
Tactic: obtain ⟨x', h1, h2⟩ := taylor_mean_remainder_lagrange hx hf.of_succ (hd.mono Ioo_subset_Icc_self)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have right : f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
Tactic: use x', h1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x = iteratedDeriv (n + 1) f x' * (x - x₀) ^ (n + 1) / (↑(n + 1)! : ℝ)
have rw : ContDiffAt ℝ (↑(n + 1) : WithTop ℕ∞) f x'
Tactic: rw [h2, iteratedDeriv_eq_iteratedFDeriv, iteratedDerivWithin_eq_iteratedFDerivWithin,
    iteratedFDerivWithin_eq_iteratedFDeriv hu _ ⟨le_of_lt h1.1, le_of_lt h1.2⟩]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x') ^ n / (↑n ! : ℝ) * (x - x₀)
have gcont : ContinuousOn id [[x₀, x]]
Tactic: have gcont : ContinuousOn id (uIcc x₀ x) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x') ^ n / (↑n ! : ℝ) * (x - x₀)
have gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun (x : ℝ) ↦ (1 : ℝ)) x_1) x_1
Tactic: have gdiff : ∀ x_1 : ℝ, x_1 ∈ uIoo x₀ x → HasDerivAt id ((fun _ : ℝ => (1 : ℝ)) x_1) x_1 :=
    fun _ _ => hasDerivAt_id _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun (x : ℝ) ↦ (1 : ℝ)) x_1) x_1
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x') ^ n / (↑n ! : ℝ) * (x - x₀)
have rcases : ∀ (y : ℝ) (hy : y ∈ uIoo x₀ x)
  (h :
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      ((x - y) ^ n / (↑n ! : ℝ) * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y),
  ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x') ^ n / (↑n ! : ℝ) * (x - x₀)
Tactic: rcases taylor_mean_remainder hx hf hf' gcont gdiff fun _ _ => by simp with ⟨y, hy, h⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun (x : ℝ) ↦ (1 : ℝ)) x_1) x_1
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / (↑n ! : ℝ) * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ ∃ x' ∈ uIoo x₀ x,
    f x - taylorWithinEval f n [[x₀, x]] x₀ x =
      iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x') ^ n / (↑n ! : ℝ) * (x - x₀)
have right : f x - taylorWithinEval f n [[x₀, x]] x₀ x =
  iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - y) ^ n / (↑n ! : ℝ) * (x - x₀)
Tactic: use y, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) (uIoo x₀ x)
gcont : ContinuousOn id [[x₀, x]]
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt id ((fun (x : ℝ) ↦ (1 : ℝ)) x_1) x_1
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ((x - y) ^ n / (↑n ! : ℝ) * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - y) ^ n / (↑n ! : ℝ) * (x - x₀)
have right : ((x - y) ^ n / (↑n ! : ℝ) * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f [[x₀, x]] y =
  iteratedDerivWithin (n + 1) f [[x₀, x]] y * (x - y) ^ n / (↑n ! : ℝ) * (x - x₀)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have inl : ∀ (hab : a ≤ a) (hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)) (hx : x ∈ Icc a a)
  (hC : ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C),
  ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
Tactic: rcases eq_or_lt_of_le hab with (rfl | h)
Cleared hypotheses: b, hab, hf, hx, hC
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
inl :
  ∀ (hab : a ≤ a) (hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)) (hx : x ∈ Icc a a)
    (hC : ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C),
    ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have inr : ∀ (h : a < b), ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
Tactic: rcases eq_or_lt_of_le hab with (rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a C x : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)
hx : x ∈ Icc a a
hC : ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have hx₁ : x = a
Tactic: rw [Icc_self, mem_singleton_iff] at hx
Cleared hypotheses: hx, hC