rw [← eq_div_iff] at h
case h
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)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
case h
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)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  f x - taylorWithinEval f n (Icc a b) x₀ x =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y /
      (-(↑n + 1) * (x - y) ^ n)
hy_ne : x - y ≠ 0
⊢ f x - taylorWithinEval f n (Icc a b) x₀ x = iteratedDerivWithin (n + 1) f (Icc a b) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

case h
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)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (Icc a b)
y : ℝ
hy : y ∈ Ioo a b
hy' : y ≠ x
h :
  (f x - taylorWithinEval f n (Icc a b) x₀ x) * (-(↑n + 1) * (x - y) ^ n) =
    (x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) * iteratedDerivWithin (n + 1) f (Icc a b) y
hy_ne : x - y ≠ 0
⊢ -(↑n + 1) * (x - y) ^ n ≠ 0