∀ {a b : ℝ} {f f' g : ℝ → ℝ},
  (∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) →
    ContinuousOn f' (Set.uIcc a b) →
      ContinuousOn g (f '' Set.uIcc a b) → ∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x