Theorem: Tutorial.exists_hasDerivAt_eq_slope (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)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
Tactic:
sorry
State after:
no goals