. exact ContinuousOn.integrableOn_Icc (ContinuousOn.mul hf_cont hg_cont)
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ IntegrableOn (fun x => f x * g x) (Set.Icc a b)
no goals