ring
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
no goals