apply exists_mul_eq_setInterval hf_cont hg_int hg_nonneg h_int <;> try simp
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Ici a)
hg_int : IntegrableOn g (Set.Ici a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Ici a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Ici a)
⊢ ∃ c ∈ Set.Ici a, ∫ (x : ℝ) in Set.Ici a, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Ici a, g x ∂μ
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Ici a)
hg_int : IntegrableOn g (Set.Ici a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Ici a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Ici a)
⊢ IsPreconnected (Set.Ici a)

a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Ici a)
hg_int : IntegrableOn g (Set.Ici a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Ici a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Ici a)
⊢ IsClosed (Set.Ici a)