obtain ⟨x', hx'⟩ := ((Ioo_infinite hab).diffₓ (Set.finite_singleton x₀)).Nonempty
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₀
no goals