no goals
ι : Type ?u.13362421
𝕜✝ : Type ?u.13362424
E : Type ?u.13362427
F : Type ?u.13362430
A : Type ?u.13362433
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
r : 𝕜
f : ℝ → 𝕜
⊢ (∫ (x : ℝ) in a..b, f x * r ∂μ) = (∫ (x : ℝ) in a..b, f x ∂μ) * r
simpa only [mul_comm r] using integral_const_mul r f