-- Mathlib/Analysis/Calculus/Taylor.lean
theorem exists_taylor_mean_remainder_bound {f : ℝ → E} {a b : ℝ} {n : ℕ} (hab : a ≤ b)
    (hf : ContDiffOn ℝ (n + 1) f (Icc a b)) :
    ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)

Proof state:
case inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)

Tactic:
use SupSet.sSup (g '' Icc a b) / (n !)

Result:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
⊢ ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) / ↑n ! * (x - a) ^ (n + 1)

Proof state:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) * (x - a) ^ (n + 1) / ↑n !

Tactic:
refine taylor_mean_remainder_bound hab hf hx fun y => ?_

Result:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
y : ℝ
⊢ y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ sSup (g '' Icc a b)

Proof state:
case inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)

Tactic:
let g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖

Result:
case inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)

Tactic:
rcases eq_or_lt_of_le hab with (rfl | h)

Result:
case inl
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
⊢ ∃ C, ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1)

case inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
⊢ ∃ C, ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1)

Proof state:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) / ↑n ! * (x - a) ^ (n + 1)

Tactic:
rw [div_mul_eq_mul_div₀]

Result:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) * (x - a) ^ (n + 1) / ↑n !

Proof state:
case inl
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
⊢ ∃ C, ∀ x ∈ Icc a a, ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1)

Tactic:
refine ⟨0, fun x hx => ?_⟩

Result:
case inl
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
x : ℝ
hx : x ∈ Icc a a
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ 0 * (x - a) ^ (n + 1)

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
x : ℝ
hx : x ∈ Icc a a
⊢ x = a

Tactic:
simpa [← le_antisymm_iff] using hx

Result:
no goals

Proof state:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
⊢ ∀ x ∈ Icc a b, ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) / ↑n ! * (x - a) ^ (n + 1)

Tactic:
intro x hx

Result:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) / ↑n ! * (x - a) ^ (n + 1)

Proof state:
case inl
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
x : ℝ
hx : x ∈ Icc a a
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ 0 * (x - a) ^ (n + 1)

Tactic:
have : x = a := by simpa [← le_antisymm_iff] using hx

Result:
case inl
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
x : ℝ
hx : x ∈ Icc a a
this : x = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ 0 * (x - a) ^ (n + 1)

Proof state:
case inl
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a : ℝ
n : ℕ
hab : a ≤ a
hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)
x : ℝ
hx : x ∈ Icc a a
this : x = a
⊢ ‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ 0 * (x - a) ^ (n + 1)

Tactic:
simp [← this]

Result:
no goals

Proof state:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y => ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
y : ℝ
⊢ y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ sSup (g '' Icc a b)

Tactic:
exact (hf.continuousOn_iteratedDerivWithin rfl.le <| uniqueDiffOn_Icc h).norm.le_sSup_image_Icc

Result:
no goals