Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr.hv
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ContinuousOn (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) [[x₀, x]]

pp: case inr.huu'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt (fun t ↦ (x - t) ^ k / ↑k !) (deriv (fun t ↦ (x - t) ^ k / ↑k !) x_1) x_1

pp: case inr.hvv'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) (deriv (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1)
      x_1

pp: case inr.hu'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ IntervalIntegrable (deriv fun t ↦ (x - t) ^ k / ↑k !) MeasureTheory.volume x₀ x

pp: case inr.hv'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ IntervalIntegrable (deriv fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) MeasureTheory.volume x₀ x

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

Goal state after:
case inr.huu'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt (fun t ↦ (x - t) ^ k / ↑k !) (deriv (fun t ↦ (x - t) ^ k / ↑k !) x_1) x_1

case inr.hvv'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ ∀ x_1 ∈ Ioo (min x₀ x) (max x₀ x),
    HasDerivAt (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) (deriv (fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) x_1)
      x_1

case inr.hu'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ IntervalIntegrable (deriv fun t ↦ (x - t) ^ k / ↑k !) MeasureTheory.volume x₀ x

case inr.hv'
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ IntervalIntegrable (deriv fun t ↦ iteratedDerivWithin k f [[x₀, x]] t) MeasureTheory.volume x₀ x