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

State before:
f : ℝ → ℝ
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)
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x') ^ n / ↑n ! * (x - x₀)
Tactic:
rcases taylor_mean_remainder_central hab hx hx₀ hf hf' continuousOn_id
    (fun _ _ => hasDerivAt_id _) fun _ _ => by simp with
  ⟨y, hy, h⟩
State after:
case intro.intro
f : ℝ → ℝ
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)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x') ^ n / ↑n ! * (x - x₀)

State before:
case intro.intro
f : ℝ → ℝ
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)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      f x - taylorWithinEval f n (Icc a b) x₀ x =
        iteratedDerivWithin (n + 1) f (Icc a b) x' * (x - x') ^ n / ↑n ! * (x - x₀)
Tactic:
refine' ⟨y, hy, _⟩
State after:
case intro.intro
f : ℝ → ℝ
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)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n / ↑n ! * (x - x₀)

State before:
case intro.intro
f : ℝ → ℝ
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)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n / ↑n ! * (x - x₀)
Tactic:
rw [h]
State after:
case intro.intro
f : ℝ → ℝ
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)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n / ↑n ! * (x - x₀)

State before:
case intro.intro
f : ℝ → ℝ
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)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n / ↑n ! * (x - x₀)
Tactic:
field_simp [n.factorial_ne_zero]
State after:
case intro.intro
f : ℝ → ℝ
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)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ (x - y) ^ n * (x - x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n * (x - x₀)

State before:
case intro.intro
f : ℝ → ℝ
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)
y : ℝ
hy : y ∈ Ioo a b
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    ((x - y) ^ n / ↑n ! * (id x - id x₀) / 1) • iteratedDerivWithin (n + 1) f (Icc a b) y
⊢ (x - y) ^ n * (x - x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y =
    iteratedDerivWithin (n + 1) f (Icc a b) y * (x - y) ^ n * (x - x₀)
Tactic:
ring
State after:
no goals

State before:
f : ℝ → ℝ
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)
x✝¹ : ℝ
x✝ : x✝¹ ∈ Ioo a b
⊢ 1 ≠ 0
Tactic:
simp
State after:
no goals