simp only [taylorWithinEval_self] at h
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
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