-- Mathlib/Analysis/Calculus/Taylor.lean
theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x)
    (hf : ContDiffOn ℝ n f (Icc x₀ x))
    (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)) :
    ∃ x' ∈ Ioo x₀ x, f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
      iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x₀) ^ (n + 1) / (n + 1)!

Proof state:
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
y : ℝ
hy : x₀ < y ∧ y < x
⊢ x - y ≠ 0

Tactic:
rw [sub_ne_zero]

Result:
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
y : ℝ
hy : x₀ < y ∧ y < x
⊢ x ≠ y

Proof state:
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
⊢ ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0

Tactic:
intro y hy

Result:
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
y : ℝ
hy : y ∈ Ioo x₀ x
⊢ (x - y) ^ n ≠ 0

Proof state:
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
y : ℝ
hy : y ∈ Ioo x₀ x
⊢ (x - y) ^ n ≠ 0

Tactic:
refine pow_ne_zero _ ?_

Result:
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
y : ℝ
hy : y ∈ Ioo x₀ x
⊢ x - y ≠ 0

Proof state:
case right
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (Icc x₀ x) y
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (Icc x₀ x) y * ((↑n + 1) * ↑n !) =
    iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (x - x₀) ^ (n + 1) * (↑n ! * ((↑n + 1) * (x - y) ^ n))

Tactic:
ring

Result:
no goals

Proof state:
case intro.intro
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (Icc x₀ x) y
⊢ ∃ x' ∈ Ioo x₀ x,
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
      iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
use y, hy

Result:
case right
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (Icc x₀ x) y
⊢ f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Proof state:
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0
⊢ ∃ x' ∈ Ioo x₀ x,
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
      iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
have hg' : ∀ y : ℝ, y ∈ Ioo x₀ x → -(↑n + 1) * (x - y) ^ n ≠ 0 := fun y hy =>
  mul_ne_zero (neg_ne_zero.mpr (Nat.cast_add_one_ne_zero n)) (xy_ne y hy)

Result:
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
⊢ ∃ x' ∈ Ioo x₀ x,
    f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
      iteratedDerivWithin (n + 1) f (Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Proof state:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ < x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
⊢ ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)

Tactic:
fun_prop

Result:
no goals

Proof state:
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
y : ℝ
hy : y ∈ Ioo x₀ x
⊢ x - y ≠ 0

Tactic:
rw [mem_Ioo] at hy

Result:
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
y : ℝ
hy : x₀ < y ∧ y < x
⊢ x - y ≠ 0

Proof state:
case right
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (Icc x₀ x) y
⊢ f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
rw [h, neg_div, ← div_neg, neg_mul, neg_neg]

Result:
case right
f : ℝ → ℝ
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 (fun t => (x - t) ^ (n + 1)) (Icc x₀ x)
xy_ne : ∀ y ∈ Ioo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ Ioo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ Ioo x₀ x
h :
  f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (Icc x₀ x) y
⊢ ((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1) / ((↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f (Icc x₀ x) y =
    iteratedDerivWithin (n + 1) f (Icc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!