awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n : WithTop ℕ∞) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this_1 : x₀ ≠ x
k : ℕ
hk_1 : k ≤ n
hk : k < n
this : UniqueDiffOn ℝ [[x₀, x]]
⊢ ContDiffOn ℝ (↑k.succ : WithTop ℕ∞) f [[x₀, x]]

Tactic:
replace hf₁ := hf₁.of_le (m := k.succ) (by norm_cast)
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this_1 : x₀ ≠ x
k : ℕ
hk_1 : k ≤ n
hk : k < n
this : UniqueDiffOn ℝ [[x₀, x]]
hf₁ : ContDiffOn ℝ (↑k.succ : WithTop ℕ∞) f [[x₀, x]]
⊢ AbsolutelyContinuousOnInterval (X := ℝ) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x₀ x

Tactic:
grind [ContDiffOn.absolutelyContinuousOnInterval,
      contDiffOn_nat_succ_iff_contDiffOn_one_iteratedDerivWithin]

Premises used: contDiffOn_nat_succ_iff_contDiffOn_one_iteratedDerivWithin, ContDiffOn.absolutelyContinuousOnInterval
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
inl :
  ∀ (hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[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
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
⊢ 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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[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:
simp
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this : x₀ ≠ x
⊢ min x₀ x < max x₀ x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this : x₀ ≠ x
⊢ UniqueDiffOn ℝ [[x₀, x]]

Tactic:
have : UniqueDiffOn ℝ [[x₀, x]] := uniqueDiffOn_Icc (by grind)
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
inr :
  ∀ k ≤ n,
    have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
    have 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:
apply taylor_integral_remainder_aux

Premises used: taylor_integral_remainder_aux
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
inr : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
inr₁ : ContinuousOn.{0, u_3} (Y := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) [[x₀, x]]
inr₂ :
  ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) (deriv (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) x_1)
      x_1
inr₃ :
  ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt.{0, u_3} (F := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t)
      (deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1) x_1
inr₄ : IntervalIntegrable (ε := ℝ) (deriv fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) MeasureTheory.volume x₀ x
inr₅ :
  IntervalIntegrable.{u_3} (ε := F) (deriv fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) MeasureTheory.volume x₀ x
⊢ have u : (t : ℝ) → ℝ := fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ);
  have 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

Tactic:
apply intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt
    (u := fun t ↦ (x - t) ^ k / k !) (v := fun t ↦ iteratedDerivWithin k f (uIcc x₀ x) t)

Premises used: intervalIntegral.integral_smul_deriv_eq_deriv_smul_of_hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
funProp : ∀ x_1 ∈ [[x₀, x]], Ne (α := ℝ) (↑k ! : ℝ) 0
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
norm_cast : k ≤ n + 1
⊢ LE.le (α := WithTop ℕ∞) (↑k : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ k ≤ n + 1

Tactic:
omega
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ContinuousOn.{0, u_3} (Y := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) [[x₀, x]]

Tactic:
exact hf.continuousOn_iteratedDerivWithin (by norm_cast; omega) this

Premises used: ContDiffOn.continuousOn_iteratedDerivWithin
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
inr : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) t
⊢ HasDerivAt (F := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) (deriv (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) t) t

Tactic:
apply DifferentiableAt.hasDerivAt

Premises used: DifferentiableAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) t

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ uIoo x₀ x ∈ 𝓝 t

Tactic:
grind [Ioo_mem_nhds, uIoo]

Premises used: Ioo_mem_nhds, Set.uIoo
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
inr : DifferentiableOn.{0, 0, u_3} ℝ (F := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) (uIoo x₀ x)
⊢ HasDerivAt.{0, u_3} (F := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t)
    (deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) t) t

Tactic:
refine DifferentiableOn.hasDerivAt (s := uIoo x₀ x) ?_ (by grind [Ioo_mem_nhds, uIoo])

Premises used: DifferentiableOn.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
norm_cast : k < n + 1
⊢ LT.lt (α := WithTop ℕ∞) (↑k : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ k < n + 1

Tactic:
omega
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ uIoo x₀ x ⊆ [[x₀, x]]

Tactic:
grind [uIoo, uIcc]

Premises used: Set.uIoo, Set.uIcc
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ DifferentiableOn.{0, 0, u_3} ℝ (F := F) (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) (uIoo x₀ x)

Tactic:
exact hf.differentiableOn_iteratedDerivWithin (by norm_cast; omega) this
      |>.mono (by grind [uIoo, uIcc])

Premises used: ContDiffOn.differentiableOn_iteratedDerivWithin, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
inr : ContinuousOn (Y := ℝ) (deriv fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]
⊢ IntervalIntegrable (ε := ℝ) (deriv fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) MeasureTheory.volume x₀ x

Tactic:
apply ContinuousOn.intervalIntegrable

Premises used: ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ContinuousOn (Y := ℝ) (deriv fun (t : ℝ) ↦ (x - t) ^ k / (↑k ! : ℝ)) [[x₀, x]]

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
inr : IntervalIntegrable (iteratedDerivWithin (k + 1) f [[x₀, x]]) MeasureTheory.volume x₀ x
inr₁ :
  iteratedDerivWithin (k + 1) f
      [[x₀,
        x]] =ᶠ[MeasureTheory.ae (F := MeasureTheory.Measure ℝ)
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι x₀ x))]
    deriv fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t
⊢ IntervalIntegrable.{u_3} (ε := F) (deriv fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) MeasureTheory.volume x₀ x

Tactic:
apply IntervalIntegrable.congr_ae (f := iteratedDerivWithin (k + 1) f [[x₀, x]])

Premises used: IntervalIntegrable.congr_ae
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
norm_cast : k + 1 ≤ n + 1
⊢ LE.le (α := WithTop ℕ∞) (↑(k + 1) : WithTop ℕ∞) (↑(n + 1) : WithTop ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ k + 1 ≤ n + 1

Tactic:
omega
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ IntervalIntegrable (iteratedDerivWithin (k + 1) f [[x₀, x]]) MeasureTheory.volume x₀ x

Tactic:
exact hf.continuousOn_iteratedDerivWithin (by norm_cast; omega) this |>.intervalIntegrable

Premises used: ContDiffOn.continuousOn_iteratedDerivWithin, ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ MeasurableSet (Ι x₀ x)

Tactic:
measurability
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
inr :
  ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Ι x₀ x →
      iteratedDerivWithin (k + 1) f [[x₀, x]] x_1 = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1
⊢ iteratedDerivWithin (k + 1) f
      [[x₀,
        x]] =ᶠ[MeasureTheory.ae (F := MeasureTheory.Measure ℝ)
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ι x₀ x))]
    deriv fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t

Tactic:
rw [Filter.EventuallyEq, MeasureTheory.ae_restrict_iff' (by measurability)]

Premises used: Filter.EventuallyEq, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
a : ℝ
h :
  a ≠ x₀ →
    a ≠ x →
      a ∈ Ι x₀ x →
        iteratedDerivWithin (k + 1) f [[x₀, x]] a = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a
⊢ a ≠ x₀ →
    a ≠ x →
      a ∈ Ι x₀ x →
        iteratedDerivWithin (k + 1) f [[x₀, x]] a = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
a : ℝ
h_1 : a ≠ x₀
h :
  a ≠ x →
    a ∈ Ι x₀ x → iteratedDerivWithin (k + 1) f [[x₀, x]] a = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a
⊢ a ≠ x →
    a ∈ Ι x₀ x → iteratedDerivWithin (k + 1) f [[x₀, x]] a = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
a : ℝ
h_1 : a ≠ x₀
h_2 : a ≠ x
h : a ∈ Ι x₀ x → iteratedDerivWithin (k + 1) f [[x₀, x]] a = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a
⊢ a ∈ Ι x₀ x → iteratedDerivWithin (k + 1) f [[x₀, x]] a = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
h :
  ∀ (a : ℝ),
    a ≠ x₀ →
      a ≠ x →
        a ∈ Ι x₀ x →
          iteratedDerivWithin (k + 1) f [[x₀, x]] a = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a
⊢ ∀ᵐ (x_1 : ℝ),
    x_1 ∈ Ι x₀ x →
      iteratedDerivWithin (k + 1) f [[x₀, x]] x_1 = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1

Tactic:
filter_upwards [MeasureTheory.volume.ae_ne x₀, MeasureTheory.volume.ae_ne x] with _ _ _ _

Premises used: MeasureTheory.Measure.ae_ne, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
a : ℝ
h_1 : a ≠ x₀
h_2 : a ≠ x
h_3 : a ∈ Ι x₀ x
h :
  derivWithin (iteratedDerivWithin k f [[x₀, x]]) [[x₀, x]] a =
    deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a
⊢ iteratedDerivWithin (k + 1) f [[x₀, x]] a = deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a

Tactic:
rw [iteratedDerivWithin_succ]

Premises used: iteratedDerivWithin_succ
-- Module: Mathlib.Analysis.Calculus.Taylor
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1) : WithTop ℕ∞) f [[x₀, x]]
this_1 : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
a : ℝ
h : a ≠ x₀
h_1 : a ≠ x
h_2 : a ∈ Ι x₀ x
⊢ derivWithin (iteratedDerivWithin k f [[x₀, x]]) [[x₀, x]] a =
    deriv (fun (t : ℝ) ↦ iteratedDerivWithin k f [[x₀, x]] t) a

Tactic:
grind [derivWithin_of_mem_nhds, Icc_mem_nhds, uIcc]

Premises used: Set.uIcc, derivWithin_of_mem_nhds, Icc_mem_nhds
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
rw :
  ∀ (hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)),
    TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (𝓝 x)
⊢ UniformCauchySeqOnFilter f l (𝓝 x)

Tactic:
rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero] at hf' ⊢

Premises used: SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this :
  TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
⊢ TendstoUniformlyOnFilter
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    (HAdd.hAdd (α := E → G) (-0) (-0)) (l ×ˢ l) (𝓝 x)

Tactic:
have := this.1.neg.add this.2.neg
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 :
  TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
this :
  TendstoUniformlyOnFilter
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    (HAdd.hAdd (α := E → G) (-0) (-0)) (l ×ˢ l) (𝓝 x)
⊢ TendstoUniformlyOnFilter
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    0 (l ×ˢ l) (𝓝 x)

Tactic:
rw [neg_zero, add_zero] at this

Premises used: add_zero, neg_zero
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x_1 : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x_1, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x_1) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x_1)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 :
  TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G)
      (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x_1 - f n.2 x_1)) 0 (l ×ˢ l) (𝓝 x_1) ∧
    TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x : E) ↦ f n.1 x_1 - f n.2 x_1) 0 (l ×ˢ l)
      (𝓝 x_1)
this :
  TendstoUniformlyOnFilter
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x_1 - f n.2 x_1))
      (-fun (n : ι × ι) (x : E) ↦ f n.1 x_1 - f n.2 x_1))
    0 (l ×ˢ l) (𝓝 x_1)
x : Prod.{u_1, u_2} (ι × ι) E
simp :
  f x.1.1 x_1 - f x.1.2 x_1 - (f x.1.1 x.2 - f x.1.2 x.2) + (f x.1.2 x_1 - f x.1.1 x_1) = -f x.1.1 x.2 + f x.1.2 x.2
⊢ HAdd.hAdd (α := ι × ι → E → G) (β := ι × ι → E → G)
      (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x_1 - f n.2 x_1))
      (-fun (n : ι × ι) (x : E) ↦ f n.1 x_1 - f n.2 x_1) x.1 x.2 =
    -f x.1.1 x.2 + f x.1.2 x.2

Tactic:
simp