awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Taylor
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
hf : ContDiffOn ℝ (↑0 : WithTop ℕ∞) f s
hf' : DifferentiableWithinAt ℝ f s y
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ f t) (derivWithin f s y) s' y

Tactic:
exact hf'.hasDerivWithinAt.mono h

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.Taylor
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
succ :
  HasDerivWithinAt
    (fun (t : ℝ) ↦
      taylorWithinEval f k s t x +
        ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    (((↑(k + 0).succ ! : ℝ)⁻¹ * (x - y) ^ (k + 0).succ) • iteratedDerivWithin ((k + 0).succ + 0).succ f s y) 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:
simp_rw [Nat.add_succ, taylorWithinEval_succ]

Premises used: taylorWithinEval_succ, Nat.add_succ
-- Module: Mathlib.Analysis.Calculus.Taylor
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
succ :
  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
⊢ HasDerivWithinAt
    (fun (t : ℝ) ↦
      taylorWithinEval f k s t x +
        ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    (((↑(k + 0).succ ! : ℝ)⁻¹ * (x - y) ^ (k + 0).succ) • iteratedDerivWithin ((k + 0).succ + 0).succ f s y) s' y

Tactic:
simp only [add_zero, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]

Premises used: Nat.factorial_succ, Nat.cast_add, Nat.cast_mul, add_zero, Nat.cast_one
-- Module: Mathlib.Analysis.Calculus.Taylor
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
⊢ LT.lt (α := WithTop ℕ) (↑k : WithTop ℕ) (↑k.succ : WithTop ℕ)

Tactic:
have coe_lt_succ : (k : WithTop ℕ) < k.succ := Nat.cast_lt.2 k.lt_succ_self
-- Module: Mathlib.Analysis.Calculus.Taylor
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 ℕ)
⊢ DifferentiableOn ℝ (iteratedDerivWithin k f s) s'

Tactic:
have hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s' :=
      (hf.differentiableOn_iteratedDerivWithin (mod_cast coe_lt_succ) hs_unique).mono h
-- Module: Mathlib.Analysis.Calculus.Taylor
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)
    (((↑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')

Premises used: ContDiffOn.of_succ, DifferentiableWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Taylor
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
    (HAdd.hAdd (α := ℝ → E) (fun (t : ℝ) ↦ taylorWithinEval f k s t x) fun (z : ℝ) ↦
      ((HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * (↑k ! : ℝ))⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z)
    (((↑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))
    s' y

Tactic:
hk.add
        (hasDerivWithinAt_taylor_coeff_within hs'_unique (nhdsWithin_mono _ h self_mem_nhdsWithin)
          hf')

Premises used: hasDerivWithinAt_taylor_coeff_within, HasDerivWithinAt.add, self_mem_nhdsWithin, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.Taylor
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
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)
⊢ 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

Tactic:
convert!
      hk.add
        (hasDerivWithinAt_taylor_coeff_within hs'_unique (nhdsWithin_mono _ h self_mem_nhdsWithin)
          hf') using 1

Premises used: hasDerivWithinAt_taylor_coeff_within, HasDerivWithinAt.add, self_mem_nhdsWithin, nhdsWithin_mono
-- Module: Mathlib.Analysis.Calculus.Taylor
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
⊢ ((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:
(add_sub_cancel _ _).symm

Premises used: add_sub_cancel, Eq.symm
-- Module: Mathlib.Analysis.Calculus.Taylor
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
⊢ ((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:
exact (add_sub_cancel _ _).symm

Premises used: add_sub_cancel, Eq.symm
-- Module: Mathlib.Analysis.Calculus.Taylor
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
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
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ taylorWithinEval f n s t x)
    (((↑n ! : ℝ)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 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

Premises used: inv_one, Nat.factorial_succ, iteratedDerivWithin_one, taylor_within_zero_eval, DifferentiableWithinAt.hasDerivWithinAt, iteratedDerivWithin_zero, taylorWithinEval_succ, zero_add, pow_zero, one_smul, Nat.cast_add, Nat.cast_mul, add_sub_cancel, Nat.add_succ, HasDerivWithinAt.mono, Nat.factorial_zero, mul_one, add_zero, Eq.symm, Nat.cast_one
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b t x : ℝ
n : ℕ
hx : a < b
ht : t ∈ Ioo a b
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
⊢ HasDerivAt (fun (y : ℝ) ↦ taylorWithinEval f n (Icc a b) y x)
    (((↑n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) t

Tactic:
have h_nhds : Ioo a b ∈ 𝓝 t := isOpen_Ioo.mem_nhds ht
  have h_nhds' : Ioo a b ∈ 𝓝[Icc a b] t := nhdsWithin_le_nhds h_nhds
  (hasDerivWithinAt_taylorWithinEval (uniqueDiffOn_Icc hx) h_nhds' ht
    Ioo_subset_Icc_self hf <| (hf' t ht).mono_of_mem_nhdsWithin h_nhds').hasDerivAt h_nhds

Premises used: uniqueDiffOn_Icc, hasDerivWithinAt_taylorWithinEval, Set.Ioo_subset_Icc_self, isOpen_Ioo, nhdsWithin_le_nhds, IsOpen.mem_nhds, HasDerivWithinAt.hasDerivAt, DifferentiableWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b t x : ℝ
n : ℕ
hx : a < b
ht : t ∈ Icc a b
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
⊢ 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 b) t

Tactic:
hasDerivWithinAt_taylorWithinEval (uniqueDiffOn_Icc hx)
    self_mem_nhdsWithin ht rfl.subset hf (hf' t ht)

Premises used: uniqueDiffOn_Icc, hasDerivWithinAt_taylorWithinEval, Eq.subset, self_mem_nhdsWithin, rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
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
⊢ HasDerivAt (fun (x : ℝ) ↦ taylorWithinEval f (n + 1) s x₀ x) (taylorWithinEval (derivWithin f s) n s x₀ x) x

Tactic:
simp_rw [taylor_within_apply]

Premises used: taylor_within_apply
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ x : ℝ
s : Set ℝ
f : ℝ → E
n : ℕ
⊢ ∀ (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 _
-- Module: Mathlib.Analysis.Calculus.Taylor
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
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₀)
⊢ 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:
apply HasDerivAt.fun_sum (fun i _ => this i) |>.congr_deriv

Premises used: HasDerivAt.fun_sum, HasDerivAt.congr_deriv
-- Module: Mathlib.Analysis.Calculus.Taylor
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
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₀)
⊢ 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:
rw [Finset.sum_range_succ', Nat.cast_zero, zero_mul, zero_mul, mul_zero, zero_smul, add_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, zero_smul, Nat.cast_zero, add_zero, Finset.sum_range_succ'
-- Module: Mathlib.Analysis.Calculus.Taylor
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
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₀
⊢ 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:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
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 : ℕ
_ :
  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₀
⊢ 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₀

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.Taylor
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)
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₀
⊢ ((↑(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₀

Tactic:
rw [← iteratedDerivWithin_succ']

Premises used: iteratedDerivWithin_succ'
-- Module: Mathlib.Analysis.Calculus.Taylor
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)
e_a : (↑(i + 1)! : ℝ)⁻¹ * ((↑(i + 1) : ℝ) * (x - x₀) ^ (i + 1 - 1) * 1) = (↑i ! : ℝ)⁻¹ * (x - x₀) ^ i
⊢ ((↑(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:
congr 1
-- Module: Mathlib.Analysis.Calculus.Taylor
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) = (↑i ! : ℝ)⁻¹ * (x - x₀) ^ i

Tactic:
simp [field, Nat.factorial_succ]

Premises used: Nat.factorial_succ
-- Module: Mathlib.Analysis.Calculus.Taylor
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
zero : Filter.Tendsto.{0, u_2} (β := E) (fun (x : ℝ) ↦ f x - f x₀) (𝓝[s] x₀) (𝓝 0)
⊢ 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:
simp only [taylor_within_zero_eval, pow_zero, Asymptotics.isLittleO_one_iff]

Premises used: taylor_within_zero_eval, pow_zero, Asymptotics.isLittleO_one_iff
-- Module: Mathlib.Analysis.Calculus.Taylor
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
zero : Filter.Tendsto f (𝓝[s] x₀) (𝓝 (f x₀))
⊢ Filter.Tendsto.{0, u_2} (β := E) (fun (x : ℝ) ↦ f x - f x₀) (𝓝[s] x₀) (𝓝 0)

Tactic:
rw [tendsto_sub_nhds_zero_iff]

Premises used: tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Analysis.Calculus.Taylor
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 f (𝓝[s] x₀) (𝓝 (f x₀))

Tactic:
hf.continuousOn.continuousWithinAt hx₀s

Premises used: ContinuousWithinAt, ContDiffOn.continuousOn, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.Taylor
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 f (𝓝[s] x₀) (𝓝 (f x₀))

Tactic:
exact hf.continuousOn.continuousWithinAt hx₀s

Premises used: ContDiffOn.continuousOn, ContinuousOn.continuousWithinAt