no goals
ι : Type ?u.12999603
𝕜✝ : Type ?u.12999606
E : Type u_2
F : Type ?u.12999612
A : Type ?u.12999615
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
a b : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
r : 𝕜
f : ℝ → E
⊢ (∫ (x : ℝ) in a..b, r • f x ∂μ) = r • ∫ (x : ℝ) in a..b, f x ∂μ
simp only [intervalIntegral, integral_smul, smul_sub]