Mean value theorem

import Mathlib

theorem mean_value_thm {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) (hf' : DifferentiableOn ℝ f (Set.Ioo a b)) : ∃ c ∈ Set.Ioo a b, deriv f c = (f b - f a) / (b - a) :=  exists_deriv_eq_slope f hab hf hf'