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 y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
k : ℕ
hk :
  ∀ (hf : ContDiffOn ℝ (↑k : WithTop ℕ∞) f s) (hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y),
    HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f k s t x)
      (((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
hf : ContDiffOn ℝ (↑(k + 1) : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
coe_lt_succ : LT.lt (α := WithTop ℕ) (↑k : WithTop ℕ) (↑k.succ : WithTop ℕ)
hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s'
⊢ HasDerivWithinAt
    (fun (t : ℝ) ↦
      taylorWithinEval f k s t x +
        ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    (((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y
have hk₁ : HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f k s t x)
  (((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
Tactic: specialize hk hf.of_succ ((hdiff y hy).mono_of_mem_nhdsWithin hs')
Cleared hypotheses: hk
-- 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 y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
k : ℕ
hf : ContDiffOn ℝ (↑(k + 1) : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
coe_lt_succ : LT.lt (α := WithTop ℕ) (↑k : WithTop ℕ) (↑k.succ : WithTop ℕ)
hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s'
hk :
  HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f k s t x)
    (((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
⊢ HasDerivWithinAt
    (fun (t : ℝ) ↦
      taylorWithinEval f k s t x +
        ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    (((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y) s' y
have h₁ : ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ k.succ) • iteratedDerivWithin k.succ.succ f s y =
  ((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y +
    (((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
      ((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
Tactic: convert!
      hk.add
        (hasDerivWithinAt_taylor_coeff_within hs'_unique (nhdsWithin_mono _ h self_mem_nhdsWithin)
          hf') using 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
x y : ℝ
n : ℕ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin n f s) s y
hs'_unique : UniqueDiffWithinAt ℝ s' y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f n s t x)
    (((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f s y) s' y
have zero : ∀ (hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s) (hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin 0 f s) s y),
  HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f 0 s t x)
    (((↑0! : ℝ)⁻¹ * HPow.hPow (β := ℕ) (x - y) 0) • iteratedDerivWithin (HAdd.hAdd (α := ℕ) 0 1) f s y) s' y
Tactic: induction n with
  | zero =>
    simp only [taylor_within_zero_eval, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero,
      mul_one, zero_add, one_smul]
    simp only [iteratedDerivWithin_zero] at hf'
    rw [iteratedDerivWithin_one]
    exact hf'.hasDerivWithinAt.mono h
  | succ k hk =>
    simp_rw [Nat.add_succ, taylorWithinEval_succ]
    simp only [add_zero, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
    have coe_lt_succ : (k : WithTop ℕ) < k.succ := Nat.cast_lt.2 k.lt_succ_self
    have hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s' :=
      (hf.differentiableOn_iteratedDerivWithin (mod_cast coe_lt_succ) hs_unique).mono h
    specialize hk hf.of_succ ((hdiff y hy).mono_of_mem_nhdsWithin hs')
    convert!
      hk.add
        (hasDerivWithinAt_taylor_coeff_within hs'_unique (nhdsWithin_mono _ h self_mem_nhdsWithin)
          hf') using 1
    exact (add_sub_cancel _ _).symm
Cleared hypotheses: n, hf, 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
x y : ℝ
n : ℕ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin n f s) s y
hs'_unique : UniqueDiffWithinAt ℝ s' y
zero :
  ∀ (hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s) (hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin 0 f s) s y),
    HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f 0 s t x)
      (((↑0! : ℝ)⁻¹ * HPow.hPow (β := ℕ) (x - y) 0) • iteratedDerivWithin (HAdd.hAdd (α := ℕ) 0 1) f s y) s' y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f n s t x)
    (((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f s y) s' y
have succ : ∀ (k : ℕ)
  (hk :
    ∀ (hf : ContDiffOn ℝ (↑k : WithTop ℕ∞) f s) (hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y),
      HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f k s t x)
        (((↑k ! : ℝ)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y)
  (hf : ContDiffOn ℝ (↑(k + 1) : WithTop ℕ∞) f s)
  (hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y),
  HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f (k + 1) s t x)
    (((↑(k + 1)! : ℝ)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 1 + 1) f s y) s' y
Tactic: induction n with
  | zero =>
    simp only [taylor_within_zero_eval, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero,
      mul_one, zero_add, one_smul]
    simp only [iteratedDerivWithin_zero] at hf'
    rw [iteratedDerivWithin_one]
    exact hf'.hasDerivWithinAt.mono h
  | succ k hk =>
    simp_rw [Nat.add_succ, taylorWithinEval_succ]
    simp only [add_zero, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
    have coe_lt_succ : (k : WithTop ℕ) < k.succ := Nat.cast_lt.2 k.lt_succ_self
    have hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s' :=
      (hf.differentiableOn_iteratedDerivWithin (mod_cast coe_lt_succ) hs_unique).mono h
    specialize hk hf.of_succ ((hdiff y hy).mono_of_mem_nhdsWithin hs')
    convert!
      hk.add
        (hasDerivWithinAt_taylor_coeff_within hs'_unique (nhdsWithin_mono _ h self_mem_nhdsWithin)
          hf') using 1
    exact (add_sub_cancel _ _).symm
Cleared hypotheses: n, hf, hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
⊢ HasDerivAt (fun (x : ℝ) ↦ taylorWithinEval f (n + 1) s x₀ x) (taylorWithinEval (derivWithin f s) n s x₀ x) x
have simp_rw : HasDerivAt.{0, u_2} (F := E)
  (fun (x : ℝ) ↦ ∑ k ∈ Finset.range (n + 1 + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀)
  (∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k (derivWithin f s) s x₀) x
Tactic: simp_rw [taylor_within_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
⊢ HasDerivAt.{0, u_2} (F := E)
    (fun (x : ℝ) ↦ ∑ k ∈ Finset.range (n + 1 + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀)
    (∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k (derivWithin f s) s x₀) x
have this : ∀ (i : ℕ) {c : ℝ} {c' : E},
  HasDerivAt (fun (x : ℝ) ↦ (c * (x - x₀) ^ i) • c') ((c * ((↑i : ℝ) * (x - x₀) ^ (i - 1) * 1)) • c') x
Tactic: have : ∀ (i : ℕ) {c : ℝ} {c' : E},
      HasDerivAt (fun x ↦ (c * (x - x₀) ^ i) • c') ((c * (i * (x - x₀) ^ (i - 1) * 1)) • c') x :=
    fun _ _ ↦ hasDerivAt_id _ |>.sub_const _ |>.pow _ |>.const_mul _ |>.smul_const _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E},
    HasDerivAt (fun (x : ℝ) ↦ (c * (x - x₀) ^ i) • c') ((c * ((↑i : ℝ) * (x - x₀) ^ (i - 1) * 1)) • c') x
⊢ HasDerivAt.{0, u_2} (F := E)
    (fun (x : ℝ) ↦ ∑ k ∈ Finset.range (n + 1 + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀)
    (∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k (derivWithin f s) s x₀) x
have apply : Eq.{u_2 + 1} (α := E)
  (∑ i ∈ Finset.range (n + 1 + 1), ((↑i ! : ℝ)⁻¹ * ((↑i : ℝ) * (x - x₀) ^ (i - 1) * 1)) • iteratedDerivWithin i f s x₀)
  (∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k (derivWithin f s) s x₀)
Tactic: apply HasDerivAt.fun_sum (fun i _ => this i) |>.congr_deriv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E},
    HasDerivAt (fun (x : ℝ) ↦ (c * (x - x₀) ^ i) • c') ((c * ((↑i : ℝ) * (x - x₀) ^ (i - 1) * 1)) • c') x
⊢ Eq.{u_2 + 1} (α := E)
    (∑ i ∈ Finset.range (n + 1 + 1),
      ((↑i ! : ℝ)⁻¹ * ((↑i : ℝ) * (x - x₀) ^ (i - 1) * 1)) • iteratedDerivWithin i f s x₀)
    (∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k (derivWithin f s) s x₀)
have rw : Eq.{u_2 + 1} (α := E)
  (∑ k ∈ Finset.range (n + 1),
    ((↑(k + 1)! : ℝ)⁻¹ * ((↑(k + 1) : ℝ) * (x - x₀) ^ (k + 1 - 1) * 1)) • iteratedDerivWithin (k + 1) f s x₀)
  (∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k (derivWithin f s) s x₀)
Tactic: rw [Finset.sum_range_succ', Nat.cast_zero, zero_mul, zero_mul, mul_zero, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E},
    HasDerivAt (fun (x : ℝ) ↦ (c * (x - x₀) ^ i) • c') ((c * ((↑i : ℝ) * (x - x₀) ^ (i - 1) * 1)) • c') x
⊢ Eq.{u_2 + 1} (α := E)
    (∑ k ∈ Finset.range (n + 1),
      ((↑(k + 1)! : ℝ)⁻¹ * ((↑(k + 1) : ℝ) * (x - x₀) ^ (k + 1 - 1) * 1)) • iteratedDerivWithin (k + 1) f s x₀)
    (∑ k ∈ Finset.range (n + 1), ((↑k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k (derivWithin f s) s x₀)
have apply : ∀ x_1 ∈ Finset.range (n + 1),
  ((↑(x_1 + 1)! : ℝ)⁻¹ * ((↑(x_1 + 1) : ℝ) * (x - x₀) ^ (x_1 + 1 - 1) * 1)) • iteratedDerivWithin (x_1 + 1) f s x₀ =
    ((↑x_1 ! : ℝ)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 (derivWithin f s) s x₀
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E},
    HasDerivAt (fun (x : ℝ) ↦ (c * (x - x₀) ^ i) • c') ((c * ((↑i : ℝ) * (x - x₀) ^ (i - 1) * 1)) • c') x
i : ℕ
h : i ∈ Finset.range (n + 1)
⊢ ((↑(i + 1)! : ℝ)⁻¹ * ((↑(i + 1) : ℝ) * (x - x₀) ^ (i + 1 - 1) * 1)) • iteratedDerivWithin (i + 1) f s x₀ =
    ((↑i ! : ℝ)⁻¹ * (x - x₀) ^ i) • iteratedDerivWithin i (derivWithin f s) s x₀
have rw : ((↑(i + 1)! : ℝ)⁻¹ * ((↑(i + 1) : ℝ) * (x - x₀) ^ (i + 1 - 1) * 1)) • iteratedDerivWithin (i + 1) f s x₀ =
  ((↑i ! : ℝ)⁻¹ * (x - x₀) ^ i) • iteratedDerivWithin (i + 1) f s x₀
Tactic: rw [← iteratedDerivWithin_succ']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
this :
  ∀ (i : ℕ) {c : ℝ} {c' : E},
    HasDerivAt (fun (x : ℝ) ↦ (c * (x - x₀) ^ i) • c') ((c * ((↑i : ℝ) * (x - x₀) ^ (i - 1) * 1)) • c') x
i : ℕ
h : i ∈ Finset.range (n + 1)
⊢ ((↑(i + 1)! : ℝ)⁻¹ * ((↑(i + 1) : ℝ) * (x - x₀) ^ (i + 1 - 1) * 1)) • iteratedDerivWithin (i + 1) f s x₀ =
    ((↑i ! : ℝ)⁻¹ * (x - x₀) ^ i) • iteratedDerivWithin (i + 1) f s x₀
have e_a : (↑(i + 1)! : ℝ)⁻¹ * ((↑(i + 1) : ℝ) * (x - x₀) ^ (i + 1 - 1) * 1) = (↑i ! : ℝ)⁻¹ * (x - x₀) ^ i
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
f : ℝ → E
hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f 0 s x₀ x)
    fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (x - x₀) 0
have zero : Filter.Tendsto.{0, u_2} (β := E) (fun (x : ℝ) ↦ f x - f x₀) (𝓝[s] x₀) (𝓝 0)
Tactic: simp only [taylor_within_zero_eval, pow_zero, Asymptotics.isLittleO_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
f : ℝ → E
hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s
⊢ Filter.Tendsto.{0, u_2} (β := E) (fun (x : ℝ) ↦ f x - f x₀) (𝓝[s] x₀) (𝓝 0)
have zero : Filter.Tendsto f (𝓝[s] x₀) (𝓝 (f x₀))
Tactic: rw [tendsto_sub_nhds_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h :
  ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s),
    Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n s x₀ x)
      fun (x : ℝ) ↦ (x - x₀) ^ n
f : ℝ → E
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f s
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
have succ : ∀ (hs : Convex ℝ (E := ℝ) {x₀}) (hx₀s : Membership.mem (γ := Set ℝ) {x₀} x₀)
  (h :
    ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f {x₀}),
      Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[{x₀}] x₀)
        (fun (x : ℝ) ↦ f x - taylorWithinEval f n {x₀} x₀ x) fun (x : ℝ) ↦ (x - x₀) ^ n)
  (hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f {x₀}),
  Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[{x₀}] x₀)
    (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) {x₀} x₀ x) fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
Tactic: rcases s.eq_singleton_or_nontrivial hx₀s with rfl | hs'
Cleared hypotheses: s, hs, hx₀s, h, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h :
  ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s),
    Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n s x₀ x)
      fun (x : ℝ) ↦ (x - x₀) ^ n
f : ℝ → E
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f s
succ :
  ∀ (hs : Convex ℝ (E := ℝ) {x₀}) (hx₀s : Membership.mem (γ := Set ℝ) {x₀} x₀)
    (h :
      ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f {x₀}),
        Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[{x₀}] x₀)
          (fun (x : ℝ) ↦ f x - taylorWithinEval f n {x₀} x₀ x) fun (x : ℝ) ↦ (x - x₀) ^ n)
    (hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f {x₀}),
    Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[{x₀}] x₀)
      (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) {x₀} x₀ x) fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
have succ₁ : ∀ (hs' : s.Nontrivial),
  Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
Tactic: rcases s.eq_singleton_or_nontrivial hx₀s with rfl | hs'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h :
  ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s),
    Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n s x₀ x)
      fun (x : ℝ) ↦ (x - x₀) ^ n
f : ℝ → E
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f s
hs' : s.Nontrivial
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
have hs'₁ : UniqueDiffOn ℝ s
Tactic: replace hs' := uniqueDiffOn_convex hs (hs.nontrivial_iff_nonempty_interior.1 hs')
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h :
  ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s),
    Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n s x₀ x)
      fun (x : ℝ) ↦ (x - x₀) ^ n
f : ℝ → E
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f s
hs' : UniqueDiffOn ℝ s
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
have hf₁ : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f s
Tactic: simp only [Nat.cast_add, Nat.cast_one] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h :
  ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s),
    Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n s x₀ x)
      fun (x : ℝ) ↦ (x - x₀) ^ n
f : ℝ → E
hs' : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f s
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
have h₁ : Eq.{u_2 + 1} (α := ℝ → E) (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x) fun (x : ℝ) ↦
  f x - taylorWithinEval f (n + 1) s x₀ x - (f x₀ - taylorWithinEval f (n + 1) s x₀ x₀)
Tactic: convert!
      Convex.isLittleO_pow_succ_real hs hx₀s ?_ (h (hf.derivWithin hs' le_rfl)) (f := fun x ↦
        f x - taylorWithinEval f (n + 1) s x₀ x) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h :
  ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s),
    Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n s x₀ x)
      fun (x : ℝ) ↦ (x - x₀) ^ n
f : ℝ → E
hs' : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f s
h₁ :
  Eq.{u_2 + 1} (α := ℝ → E) (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x) fun (x : ℝ) ↦
    f x - taylorWithinEval f (n + 1) s x₀ x - (f x₀ - taylorWithinEval f (n + 1) s x₀ x₀)
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
have succ : ∀ x ∈ s,
  HasDerivWithinAt (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    (derivWithin f s x - taylorWithinEval (derivWithin f s) n s x₀ x) s x
Tactic: convert!
      Convex.isLittleO_pow_succ_real hs hx₀s ?_ (h (hf.derivWithin hs' le_rfl)) (f := fun x ↦
        f x - taylorWithinEval f (n + 1) s x₀ x) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Taylor (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h :
  ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s),
    Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n s x₀ x)
      fun (x : ℝ) ↦ (x - x₀) ^ n
f : ℝ → E
hs' : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f s
x : ℝ
hx : x ∈ s
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    (derivWithin f s x - taylorWithinEval (derivWithin f s) n s x₀ x) s x
have succ : HasDerivWithinAt f (derivWithin f s x) s x
Tactic: refine HasDerivWithinAt.sub ?_ (hasDerivAt_taylorWithinEval_succ f n).hasDerivWithinAt
-- 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
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n s x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ n
have zero : ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s),
  Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f 0 s x₀ x)
    fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (x - x₀) 0
Tactic: induction n generalizing f with
  | zero =>
    simp only [taylor_within_zero_eval, pow_zero, Asymptotics.isLittleO_one_iff]
    rw [tendsto_sub_nhds_zero_iff]
    exact hf.continuousOn.continuousWithinAt hx₀s
  | succ n h =>
    rcases s.eq_singleton_or_nontrivial hx₀s with rfl | hs'
    · simp
    replace hs' := uniqueDiffOn_convex hs (hs.nontrivial_iff_nonempty_interior.1 hs')
    simp only [Nat.cast_add, Nat.cast_one] at hf
    convert!
      Convex.isLittleO_pow_succ_real hs hx₀s ?_ (h (hf.derivWithin hs' le_rfl)) (f := fun x ↦
        f x - taylorWithinEval f (n + 1) s x₀ x) using 1
    · simp
    · intro x hx
      refine HasDerivWithinAt.sub ?_ (hasDerivAt_taylorWithinEval_succ f n).hasDerivWithinAt
      exact (hf.differentiableOn (by simp) _ hx).hasDerivWithinAt
Cleared hypotheses: f, n, 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
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
zero :
  ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s),
    Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f 0 s x₀ x)
      fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (x - x₀) 0
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n s x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ n
have succ : ∀ (n : ℕ)
  (h :
    ∀ {f : ℝ → E} (hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s),
      Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n s x₀ x)
        fun (x : ℝ) ↦ (x - x₀) ^ n)
  {f : ℝ → E} (hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f s),
  Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝[s] x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)
Tactic: induction n generalizing f with
  | zero =>
    simp only [taylor_within_zero_eval, pow_zero, Asymptotics.isLittleO_one_iff]
    rw [tendsto_sub_nhds_zero_iff]
    exact hf.continuousOn.continuousWithinAt hx₀s
  | succ n h =>
    rcases s.eq_singleton_or_nontrivial hx₀s with rfl | hs'
    · simp
    replace hs' := uniqueDiffOn_convex hs (hs.nontrivial_iff_nonempty_interior.1 hs')
    simp only [Nat.cast_add, Nat.cast_one] at hf
    convert!
      Convex.isLittleO_pow_succ_real hs hx₀s ?_ (h (hf.derivWithin hs' le_rfl)) (f := fun x ↦
        f x - taylorWithinEval f (n + 1) s x₀ x) using 1
    · simp
    · intro x hx
      refine HasDerivWithinAt.sub ?_ (hasDerivAt_taylorWithinEval_succ f n).hasDerivWithinAt
      exact (hf.differentiableOn (by simp) _ hx).hasDerivWithinAt
Cleared hypotheses: f, n, hf