Theorem: Tutorial.exists_hasDerivAt_eq_zero (Tutorial/Advanced/Analysis/Lecture2.lean)

State before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
⊢ ∃ c ∈ Ioo a b, f' c = 0
Tactic:
sorry
State after:
no goals