theorem
intervalIntegral.integral_deriv_eq_sub_uIoo
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ℝ → E}
{a b : ℝ}
(hcont : ContinuousOn f (Set.uIcc a b))
(hderiv : ∀ x ∈ Set.uIoo a b, DifferentiableAt ℝ f x)
(hint : IntervalIntegrable (deriv f) MeasureTheory.volume a b)
: