-- Mathlib/Analysis/Calculus/Taylor.lean
theorem taylor_mean_remainder {f : ℝ → ℝ} {g g' : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x)
    (hf : ContDiffOn ℝ n f (Icc x₀ x))
    (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x))
    (gcont : ContinuousOn g (Icc x₀ x))
    (gdiff : ∀ x_1 : ℝ, x_1 ∈ Ioo x₀ x → HasDerivAt g (g' x_1) x_1)
    (g'_ne : ∀ x_1 : ℝ, x_1 ∈ Ioo x₀ x → g' x_1 ≠ 0) :
    ∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    ((x - x') ^ n / n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'

Proof state:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) / g' y =
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x
⊢ f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y

Tactic:
rw [← h]

Result:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) / g' y =
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x
⊢ ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) / g' y =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y

Proof state:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) / g' y =
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x
⊢ ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) / g' y =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y

Tactic:
field_simp [g'_ne y hy]

Result:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) / g' y =
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x
⊢ (x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (g x - g x₀) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc x₀ x) y

Proof state:
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
⊢ ∃ x' ∈ Ioo x₀ x,
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
      ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'

Tactic:
rcases exists_ratio_hasDerivAt_eq_ratio_slope (fun t => taylorWithinEval f n (Icc x₀ x) t x)
    (fun t => ((n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc 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⟩

Result:
case intro.intro
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y =
    (taylorWithinEval f n (Icc x₀ x) x x - taylorWithinEval f n (Icc x₀ x) x₀ x) * g' y
⊢ ∃ x' ∈ Ioo x₀ x,
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
      ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'

Proof state:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y =
    (taylorWithinEval f n (Icc x₀ x) x x - taylorWithinEval f n (Icc x₀ x) x₀ x) * g' y
⊢ f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y

Tactic:
simp only [taylorWithinEval_self] at h

Result:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y =
    (f x - taylorWithinEval f n (Icc x₀ x) x₀ x) * g' y
⊢ f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y

Proof state:
case intro.intro
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y =
    (taylorWithinEval f n (Icc x₀ x) x x - taylorWithinEval f n (Icc x₀ x) x₀ x) * g' y
⊢ ∃ x' ∈ Ioo x₀ x,
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
      ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'

Tactic:
use y, hy

Result:
case right
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y =
    (taylorWithinEval f n (Icc x₀ x) x x - taylorWithinEval f n (Icc x₀ x) x₀ x) * g' y
⊢ f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y