Theorem: taylor_mean_remainder_central_aux (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
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
rcases eq_or_ne x₀ x with (rfl | hx')
State after:
case inl
f g g' : ℝ → ℝ
x₀ a b : ℝ
n : ℕ
hab : 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
hx : x₀ ∈ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x₀ ∧
        (f x₀ - taylorWithinEval f n (Icc a b) x₀ x₀) * g' x' =
          ((x₀ - x') ^ n / ↑n ! * (g x₀ - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

case inr
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
hx' : x₀ ≠ x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

State before:
case inr
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
hx' : x₀ ≠ x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
rcases Ne.lt_or_lt hx' with (hx' | hx')
State after:
case inr.inl
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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

case inr.inr
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
hx'✝ : x₀ ≠ x
hx' : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

State before:
case inl
f g g' : ℝ → ℝ
x₀ a b : ℝ
n : ℕ
hab : 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
hx : x₀ ∈ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x₀ ∧
        (f x₀ - taylorWithinEval f n (Icc a b) x₀ x₀) * g' x' =
          ((x₀ - x') ^ n / ↑n ! * (g x₀ - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
simp only [sub_self, taylorWithinEval_self, MulZeroClass.mul_zero, zero_div, zero_smul,
  eq_self_iff_true, exists_prop, and_true_iff, MulZeroClass.zero_mul]
State after:
case inl
f g g' : ℝ → ℝ
x₀ a b : ℝ
n : ℕ
hab : 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
hx : x₀ ∈ Icc a b
⊢ ∃ x' ∈ Ioo a b, x' ≠ x₀

State before:
case inl
f g g' : ℝ → ℝ
x₀ a b : ℝ
n : ℕ
hab : 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
hx : x₀ ∈ Icc a b
⊢ ∃ x' ∈ Ioo a b, x' ≠ x₀
Tactic:
obtain ⟨x', hx'⟩ := ((Ioo_infinite hab).diffₓ (Set.finite_singleton x₀)).Nonempty
State after:
no goals

State before:
case inr.inl
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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
have h₁ : Icc x₀ x ⊆ Icc a b := Icc_subset_Icc hx₀.1 hx.2
State after:
case inr.inl
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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

State before:
case inr.inl
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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
have h₂ : Ioo x₀ x ⊆ Ioo a b := Ioo_subset_Ioo hx₀.1 hx.2
State after:
case inr.inl
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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

State before:
case inr.inl
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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
obtain ⟨y, hy, h⟩ :=
  exists_ratio_hasDerivAt_eq_ratio_slope (fun t => taylorWithinEval f n (Icc a b) t x)
    (fun t => ((n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) hx'
    ((continuousOn_taylorWithinEval (uniqueDiffOn_Icc hab) hf).mono h₁)
    (fun _ hy => taylorWithinEval_hasDerivAt_Ioo _ hab (h₂ hy) hf hf') g g' (gcont.mono h₁)
    fun y hy => gdiff y (h₂ hy)
State after:
case inr.inl.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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

State before:
case inr.inl.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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
refine' ⟨y, h₂ hy, hy.2.Ne, _⟩
State after:
case inr.inl.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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ (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

State before:
case inr.inl.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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ (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
Tactic:
simp only [taylorWithinEval_self] at h
State after:
case inr.inl.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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ (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

State before:
case inr.inl.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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ (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
Tactic:
field_simp [← h, n.factorial_ne_zero]
State after:
case inr.inl.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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ (g x - g x₀) * ((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc a b) y) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y

State before:
case inr.inl.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
hx'✝ : x₀ ≠ x
hx' : x₀ < x
h₁ : Icc x₀ x ⊆ Icc a b
h₂ : Ioo x₀ x ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  (g x - g x₀) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' y
⊢ (g x - g x₀) * ((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc a b) y) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y
Tactic:
ring
State after:
no goals

State before:
case inr.inr
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
hx'✝ : x₀ ≠ x
hx' : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
have h₁ : Icc x x₀ ⊆ Icc a b := Icc_subset_Icc hx.1 hx₀.2
State after:
case inr.inr
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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

State before:
case inr.inr
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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
have h₂ : Ioo x x₀ ⊆ Ioo a b := Ioo_subset_Ioo hx.1 hx₀.2
State after:
case inr.inr
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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

State before:
case inr.inr
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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
obtain ⟨y, hy, h⟩ :=
  exists_ratio_hasDerivAt_eq_ratio_slope (fun t => taylorWithinEval f n (Icc a b) t x)
    (fun t => ((n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) hx'
    ((continuousOn_taylorWithinEval (uniqueDiffOn_Icc hab) hf).mono h₁)
    (fun _ hy => taylorWithinEval_hasDerivAt_Ioo _ hab (h₂ hy) hf hf') g g' (gcont.mono h₁)
    fun y hy => gdiff y (h₂ hy)
State after:
case inr.inr.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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x₀ x - taylorWithinEval f n (Icc a b) x x) * g' y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'

State before:
case inr.inr.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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x₀ x - taylorWithinEval f n (Icc a b) x x) * g' y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo a b),
      x' ≠ x ∧
        (f x - taylorWithinEval f n (Icc a b) x₀ x) * g' x' =
          ((x - x') ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) x'
Tactic:
refine' ⟨y, h₂ hy, hy.1.ne', _⟩
State after:
case inr.inr.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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x₀ x - taylorWithinEval f n (Icc a b) x x) * g' y
⊢ (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

State before:
case inr.inr.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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x₀ x - taylorWithinEval f n (Icc a b) x x) * g' y
⊢ (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
Tactic:
simp only [taylorWithinEval_self] at h
State after:
case inr.inr.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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x₀ x - f x) * g' y
⊢ (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

State before:
case inr.inr.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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x₀ x - f x) * g' y
⊢ (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
Tactic:
rw [← neg_sub, neg_mul, ← h]
State after:
case inr.inr.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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x₀ x - f x) * g' y
⊢ -((g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y) =
    ((x - y) ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) y

State before:
case inr.inr.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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x₀ x - f x) * g' y
⊢ -((g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y) =
    ((x - y) ^ n / ↑n ! * (g x - g x₀)) • iteratedDerivWithin (n + 1) f (Icc a b) y
Tactic:
field_simp [n.factorial_ne_zero]
State after:
case inr.inr.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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x₀ x - f x) * g' y
⊢ -((g x₀ - g x) * ((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc a b) y) * ↑n !) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y * ↑n !

State before:
case inr.inr.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
hx'✝ : x₀ ≠ x
hx' : x < x₀
h₁ : Icc x x₀ ⊆ Icc a b
h₂ : Ioo x x₀ ⊆ Ioo a b
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y =
    (taylorWithinEval f n (Icc a b) x₀ x - f x) * g' y
⊢ -((g x₀ - g x) * ((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc a b) y) * ↑n !) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc a b) y * ↑n !
Tactic:
ring
State after:
no goals