Theorem: taylor_mean_remainder_unordered (ExponentialRamsey/Prereq/Mathlib/Analysis/Calculus/Taylor.lean)

State before:
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn g (uIcc 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
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (uIcc x₀ x) x'
Tactic:
rcases Ne.lt_or_lt hx with (hx₀ | hx₀)
State after:
case inl
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn g (uIcc 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₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (uIcc x₀ x) x'

case inr
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn g (uIcc 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₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (uIcc x₀ x) x'

State before:
case inr
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn g (uIcc 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₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (uIcc x₀ x) x'
Tactic:
rw [uIcc_of_ge hx₀.le] at hf hf' gcont ⊢
State after:
case inr
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (uIoo x₀ x)
gcont : ContinuousOn g (Icc 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₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo 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'

State before:
case inr
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (uIoo x₀ x)
gcont : ContinuousOn g (Icc 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₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo 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:
rw [uIoo_of_ge hx₀.le] at g'_ne gdiff hf' ⊢
State after:
case inr
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
hx₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : 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'

State before:
case inr
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
hx₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : 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⟩
State after:
case inr.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
hx₀ : x < x₀
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',
    ∃ (_ : 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'

State before:
case inr.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
hx₀ : x < x₀
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',
    ∃ (_ : 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
State after:
case h
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
hx₀ : x < x₀
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

State before:
case h
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
hx₀ : x < x₀
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
State after:
case h
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
hx₀ : x < x₀
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 - f 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

State before:
case h
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
hx₀ : x < x₀
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 - f 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:
rw [mul_comm, ← div_left_inj' (g'_ne y hy), mul_div_cancel _ (g'_ne y hy)] at h
State after:
case h
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
hx₀ : x < x₀
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 =
    taylorWithinEval f n (Icc x x₀) x₀ x - f 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

State before:
case h
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
hx₀ : x < x₀
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 =
    taylorWithinEval f n (Icc x x₀) x₀ x - f 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 [← neg_sub, ← h]
State after:
case h
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
hx₀ : x < x₀
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 =
    taylorWithinEval f n (Icc x x₀) x₀ x - f 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

State before:
case h
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
hx₀ : x < x₀
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 =
    taylorWithinEval f n (Icc x x₀) x₀ x - f 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, n.factorial_ne_zero]
State after:
case h
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
hx₀ : x < x₀
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 =
    taylorWithinEval f n (Icc x x₀) x₀ x - f x
⊢ -((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) * (↑n ! * g' y)) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc x x₀) y * (↑n ! * g' y)

State before:
case h
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
hx₀ : x < x₀
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 =
    taylorWithinEval f n (Icc x x₀) x₀ x - f x
⊢ -((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) * (↑n ! * g' y)) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc x x₀) y * (↑n ! * g' y)
Tactic:
ring
State after:
no goals

State before:
case inl
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn g (uIcc 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₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (uIcc x₀ x) x'
Tactic:
rw [uIcc_of_le hx₀.le] at hf hf' gcont ⊢
State after:
case inl
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn g (Icc 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₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo 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'

State before:
case inl
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn g (Icc 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₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo 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:
rw [uIoo_of_le hx₀.le] at g'_ne gdiff hf' ⊢
State after:
case inl
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
hx₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : 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'

State before:
case inl
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
hx₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : 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:
exact taylor_mean_remainder hx₀ hf hf' gcont gdiff g'_ne
State after:
no goals