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
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
h : a < b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
Tactic: have hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b) :=
    hf.differentiableOn_iteratedDerivWithin (mod_cast n.lt_succ_self)
      (uniqueDiffOn_Icc 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
have rw : |(↑n ! : ℝ)⁻¹ * (x - y) ^ n| * ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
Tactic: rw [norm_smul, Real.norm_eq_abs]
-- 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ |(↑n ! : ℝ)⁻¹ * (x - y) ^ n| * ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
have h₁ : |(↑n ! : ℝ)⁻¹ * (x - y) ^ n| ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n
Tactic: gcongr
-- 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
h₁ : |(↑n ! : ℝ)⁻¹ * (x - y) ^ n| ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n
⊢ |(↑n ! : ℝ)⁻¹ * (x - y) ^ n| * ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
have h₂ : ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
Tactic: gcongr
-- 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ |(↑n ! : ℝ)⁻¹ * (x - y) ^ n| ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n
have h₁ : (↑n ! : ℝ)⁻¹ * |x - y| ^ n ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n
Tactic: rw [abs_mul, abs_pow, abs_inv, Nat.abs_cast]
-- 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
⊢ (↑n ! : ℝ)⁻¹ * |x - y| ^ n ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n
have h₁ : LE.le (α := ℝ) 0 (↑n ! : ℝ)⁻¹
Tactic: gcongr
-- 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
h₁ : LE.le (α := ℝ) 0 (↑n ! : ℝ)⁻¹
⊢ (↑n ! : ℝ)⁻¹ * |x - y| ^ n ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n
have h₂ : 0 ≤ |x - y|
Tactic: gcongr
-- 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
y : ℝ
hay : a ≤ y
hyx : y < x
h₁ : LE.le (α := ℝ) 0 (↑n ! : ℝ)⁻¹
h₂ : 0 ≤ |x - y|
⊢ (↑n ! : ℝ)⁻¹ * |x - y| ^ n ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n
have h₃ : 0 ≤ x - y
Tactic: gcongr
-- 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 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have h' : ∀ y ∈ Ico a x,
  ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
Tactic: have h' : ∀ y ∈ Ico a x,
      ‖((n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤
        (n ! : ℝ)⁻¹ * |x - a| ^ n * C := by
    rintro y ⟨hay, hyx⟩
    rw [norm_smul, Real.norm_eq_abs]
    gcongr
    · rw [abs_mul, abs_pow, abs_inv, Nat.abs_cast]
      gcongr
    -- Estimate the iterated derivative by `C`
    · exact hC y ⟨hay, hyx.le.trans hx.2⟩
-- 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 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
t : ℝ
ht : t ∈ Icc a x
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
    (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
have I : Icc a x ⊆ Icc a b
Tactic: have I : Icc a x ⊆ Icc a b := Icc_subset_Icc_right hx.2
-- 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 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have A : ∀ t ∈ Icc a x,
  HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
    (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
Tactic: have A : ∀ t ∈ Icc a x, HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
      (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t := by
    intro t ht
    have I : Icc a x ⊆ Icc a b := Icc_subset_Icc_right hx.2
    exact (hasDerivWithinAt_taylorWithinEval_at_Icc x h (I ht) hf.of_succ hf').mono I
-- 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 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have this : ‖taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)
Tactic: have := norm_image_sub_le_of_norm_deriv_le_segment' A h' x (right_mem_Icc.2 hx.1)
-- 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 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this :
  ‖taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have this₁ : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)
Tactic: simp only [taylorWithinEval_self] at this
Cleared hypotheses: this
-- 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have inr : (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
Tactic: refine this.trans_eq ?_
-- 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
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' :
  ∀ y ∈ Ico a x,
    ‖((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a)
⊢ (↑n ! : ℝ)⁻¹ * |x - a| ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have inr : (↑n ! : ℝ)⁻¹ * (x - a) ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / (↑n ! : ℝ)
Tactic: rw [abs_of_nonneg (sub_nonneg.mpr hx.1)]
-- 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 : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
⊢ ∃ (C : ℝ), ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)
have inl : ∀ (hab : a ≤ a) (hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)),
  ∃ (C : ℝ), ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1)
Tactic: rcases eq_or_lt_of_le hab with (rfl | h)
Cleared hypotheses: b, hab, hf
-- 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 : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
inl :
  ∀ (hab : a ≤ a) (hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)),
    ∃ (C : ℝ), ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1)
⊢ ∃ (C : ℝ), ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)
have inr : ∀ (h : a < b), ∃ (C : ℝ), ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)
Tactic: rcases eq_or_lt_of_le hab with (rfl | 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 : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)
⊢ ∃ (C : ℝ), ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1)
have inl : ∀ (x : ℝ) (hx : x ∈ Icc a a), ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ 0 * (x - a) ^ (n + 1)
Tactic: refine ⟨0, fun x hx => ?_⟩
-- 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 : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a a)
x : ℝ
hx : x ∈ Icc a a
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ 0 * (x - a) ^ (n + 1)
have this : x = a
Tactic: have : x = a := by simpa [← le_antisymm_iff] using hx
-- 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 : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun (y : ℝ) ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
⊢ ∃ (C : ℝ), ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)
have h₁ : ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) / (↑n ! : ℝ) * (x - a) ^ (n + 1)
Tactic: use SupSet.sSup (g '' Icc a b) / (n !)
-- 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 : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun (y : ℝ) ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) / (↑n ! : ℝ) * (x - a) ^ (n + 1)
have h₁ : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) * (x - a) ^ (n + 1) / (↑n ! : ℝ)
Tactic: rw [div_mul_eq_mul_div₀]
-- 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 : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun (y : ℝ) ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) * (x - a) ^ (n + 1) / (↑n ! : ℝ)
have h₁ : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ sSup (g '' Icc a b)
Tactic: refine taylor_mean_remainder_bound hab hf hx fun y => ?_
-- 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
⊢ 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 :
    ∀ 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
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
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
inl :
  ∀
    (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
⊢ 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 : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
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
have inr : f x - f x₀ = ∫ (t : ℝ) in x₀..x, derivWithin f [[x₀, x]] t
Tactic: 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]
-- 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 : x₀ ≠ x
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 - f x₀ = ∫ (t : ℝ) in x₀..x, derivWithin f [[x₀, x]] t
have hf₁ : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
Tactic: 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
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
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
⊢ f x - f x₀ = ∫ (t : ℝ) in x₀..x, derivWithin f [[x₀, x]] t
have inr : Eq.{u_3 + 1} (α := F) (∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t) (∫ (t : ℝ) in x₀..x, derivWithin f [[x₀, x]] t)
Tactic: rw [← hf]
-- 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 : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
⊢ Eq.{u_3 + 1} (α := F) (∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t)
    (∫ (t : ℝ) in x₀..x, derivWithin f [[x₀, x]] t)
have inr : ∀ᵐ (x_1 : ℝ), x_1 ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) x_1 = derivWithin f [[x₀, x]] 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 : x₀ ≠ x
hf : ∫ (t : ℝ) in x₀..x, deriv (fun (t : ℝ) ↦ f t) t = f x - f x₀
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) x_1 = derivWithin f [[x₀, x]] x_1
have h : ∀ (a : ℝ), a ≠ x₀ → a ≠ x → a ∈ Ι x₀ x → deriv (fun (t : ℝ) ↦ f t) a = derivWithin f [[x₀, x]] a
Tactic: filter_upwards [MeasureTheory.volume.ae_ne x₀, MeasureTheory.volume.ae_ne x] with _ _ _ _
-- 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 : 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
⊢ 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 this₁ : UniqueDiffOn ℝ [[x₀, x]]
Tactic: have : UniqueDiffOn ℝ [[x₀, x]] := uniqueDiffOn_Icc (by grind)