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

State before:
f g g' : ℝ → ℝ
x₀ x a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
obtain ⟨y, hy, hyx, h⟩ := taylor_mean_remainder_central_aux hab hx hx₀ hf hf' gcont gdiff
State after:
case intro.intro.intro
f g g' : ℝ → ℝ
x₀ x a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    ((x - y) ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc a b) x'

State before:
case intro.intro.intro
f g g' : ℝ → ℝ
x₀ x a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    ((x - y) ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
refine' ⟨y, hy, _⟩
State after:
case intro.intro.intro
f g g' : ℝ → ℝ
x₀ x a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    ((x - y) ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc a b) y

State before:
case intro.intro.intro
f g g' : ℝ → ℝ
x₀ x a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    ((x - y) ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc a b) y
Tactic:
rw [smul_eq_mul] at h
State after:
case intro.intro.intro
f g g' : ℝ → ℝ
x₀ x a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    (x - y) ^ n / ↑n ! * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc a b) y

State before:
case intro.intro.intro
f g g' : ℝ → ℝ
x₀ x a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    (x - y) ^ n / ↑n ! * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc a b) y
Tactic:
rw [smul_eq_mul, div_mul_eq_mul_div, ← h, mul_div_cancel]
State after:
case intro.intro.intro.h
f g g' : ℝ → ℝ
x₀ x a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    (x - y) ^ n / ↑n ! * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ g' y ≠ 0

State before:
case intro.intro.intro.h
f g g' : ℝ → ℝ
x₀ x a b : ℝ
n : ℕ
hab : a < b
hx : x ∈ Icc a b
hx₀ : x₀ ∈ Icc a b
hf : ContDiffOn ℝ (↑n) f (Icc a b)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)
gcont : ContinuousOn g (Icc a b)
gdiff : ∀ y ∈ Ioo a b, HasDerivAt g (g' y) y
g'_ne : ∀ y ∈ Ioo a b, g' y ≠ 0
y : ℝ
hy : y ∈ Ioo a b
hyx : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y =
    (x - y) ^ n / ↑n ! * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ g' y ≠ 0
Tactic:
exact g'_ne _ hy
State after:
no goals