awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
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)
⊢ 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'

Premises used: Set.eq_singleton_or_nontrivial, rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x₀ : ℝ
n : ℕ
f : ℝ → E
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:
simp
-- 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
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
⊢ UniqueDiffOn ℝ s

Tactic:
replace hs' := uniqueDiffOn_convex hs (hs.nontrivial_iff_nonempty_interior.1 hs')
-- 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
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
⊢ ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1) f s

Tactic:
simp only [Nat.cast_add, Nat.cast_one] at hf

Premises used: Nat.cast_add, Nat.cast_one
-- 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
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 : ℝ) ↦
      HSub.hSub (α := E) ((fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x) x)
        ((fun (x : ℝ) ↦ f x - taylorWithinEval f (n + 1) s x₀ x) x₀))
    fun (x : ℝ) ↦ (x - x₀) ^ (n + 1)

Tactic:
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)

Premises used: le_rfl, ContDiffOn.derivWithin, Convex.isLittleO_pow_succ_real
-- 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
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₀)
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
⊢ 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:
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

Premises used: le_rfl, ContDiffOn.derivWithin, Convex.isLittleO_pow_succ_real
-- 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
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
⊢ 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:
simp
-- 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
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

Tactic:
HasDerivWithinAt.sub ?_ (hasDerivAt_taylorWithinEval_succ f n).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, HasDerivWithinAt.sub, hasDerivAt_taylorWithinEval_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
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
succ : HasDerivWithinAt f (derivWithin f s x) s x
⊢ 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:
refine HasDerivWithinAt.sub ?_ (hasDerivAt_taylorWithinEval_succ f n).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, HasDerivWithinAt.sub, hasDerivAt_taylorWithinEval_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
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
⊢ HAdd.hAdd (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) 1 ≠ 0

Tactic:
simp
-- 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
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 f (derivWithin f s x) s x

Tactic:
exact (hf.differentiableOn (by simp) _ hx).hasDerivWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, ContDiffOn.differentiableOn
-- Module: Mathlib.Analysis.Calculus.Taylor
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
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)
⊢ 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

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

Premises used: HasDerivAt.hasDerivWithinAt, HasDerivWithinAt.sub, taylor_within_zero_eval, hasDerivAt_taylorWithinEval_succ, pow_zero, Nat.cast_add, ContDiffOn.continuousOn, Asymptotics.isLittleO_one_iff, Set.eq_singleton_or_nontrivial, Nat.cast_one, rfl, tendsto_sub_nhds_zero_iff, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
x₀ : ℝ
n : ℕ
hf : ContDiff ℝ (↑n : WithTop ℕ∞) f
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := E) (F := ℝ) (𝓝 x₀) (fun (x : ℝ) ↦ f x - taylorWithinEval f n univ x₀ x)
    fun (x : ℝ) ↦ (x - x₀) ^ n

Tactic:
simpa using taylor_isLittleO convex_univ (mem_univ x₀) hf.contDiffOn

Premises used: ContDiff.contDiffOn, convex_univ, taylor_isLittleO, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.Taylor
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 (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
-- Module: Mathlib.Analysis.Calculus.Taylor
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)
rw₁ : ∀ (x : ℝ), ‖(x - x₀) ^ n‖ = 0 → ‖f x - taylorWithinEval f n s x₀ 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

Premises used: Asymptotics.isLittleO_iff_tendsto
-- Module: Mathlib.Analysis.Calculus.Taylor
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)
rw : Filter.Tendsto (β := ℝ) (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)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.Calculus.Taylor
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 (β := ℝ) (fun (x : ℝ) ↦ ‖((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)‖) (𝓝[s] x₀) (𝓝 0)

Tactic:
simpa [norm_smul, div_eq_inv_mul] using h_isLittleO

Premises used: norm_smul, div_eq_inv_mul
-- Module: Mathlib.Analysis.Calculus.Taylor
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‖
simp : ∀ (x : ℝ), x - x₀ = 0 → ¬n = 0 → f x - taylorWithinEval f n s x₀ x = 0
⊢ ∀ (x : ℝ), ‖(x - x₀) ^ 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]

Premises used: norm_eq_zero, norm_pow, and_imp, pow_eq_zero_iff', ne_eq, abs_eq_zero, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Calculus.Taylor
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
⊢ x = x₀

Tactic:
rw [sub_eq_zero] at hx

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Calculus.Taylor
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₀
⊢ ¬n = 0 → f x - taylorWithinEval f n s x₀ x = 0

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (𝓝[s] x₀) (𝓝 0)

Tactic:
_root_.taylor_tendsto hs hx₀s hf

Premises used: taylor_tendsto
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
h :
  ∀ (x : ℝ), (f x - taylorWithinEval f n s x₀ x) / (x - x₀) ^ n = ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ (f x - taylorWithinEval f n s x₀ x) / (x - x₀) ^ n) (𝓝[s] x₀) (𝓝 0)

Tactic:
convert! _root_.taylor_tendsto hs hx₀s hf using 2 with x

Premises used: taylor_tendsto
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n : WithTop ℕ∞) f s
x : ℝ
⊢ (f x - taylorWithinEval f n s x₀ x) / (x - x₀) ^ n = ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)

Tactic:
simp [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Analysis.Calculus.Taylor
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
⊢ min x₀ x < max x₀ x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.Taylor
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
⊢ min x₀ x < max x₀ x

Tactic:
have hx₁ : min x₀ x < max x₀ x := by grind
-- Module: Mathlib.Analysis.Calculus.Taylor
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
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'
⊢ ∃ 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⟩

Premises used: taylorWithinEval, uniqueDiffOn_Icc, taylorWithinEval_hasDerivAt_Ioo, HMul.hMul, HSub.hSub, iteratedDerivWithin, Nat.cast, Inv.inv, HPow.hPow, HAdd.hAdd, Nat.factorial, exists_ratio_hasDerivAt_eq_ratio_slope, HSMul.hSMul, continuousOn_taylorWithinEval, OfNat.ofNat, Set.uIcc
-- Module: Mathlib.Analysis.Calculus.Taylor
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
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
⊢ ∃ 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:
use y, hy
-- Module: Mathlib.Analysis.Calculus.Taylor
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
⊢ 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:
grind [uIoo, smul_eq_mul, taylorWithinEval_self]

Premises used: Set.uIoo, taylorWithinEval_self, smul_eq_mul
-- Module: Mathlib.Analysis.Calculus.Taylor
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)
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ (n + 1)) [[x₀, x]]

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.Taylor
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)
⊢ 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
-- Module: Mathlib.Analysis.Calculus.Taylor
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]]
⊢ ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0

Tactic:
grind [uIoo, pow_ne_zero]

Premises used: pow_ne_zero, Set.uIoo
-- Module: Mathlib.Analysis.Calculus.Taylor
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]]
⊢ ∀ 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]
-- Module: Mathlib.Analysis.Calculus.Taylor
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
⊢ ∀ 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)