no goals
ι : Type ?u.13831725
𝕜 : Type ?u.13831728
E : Type u_1
F : Type ?u.13831734
A : Type ?u.13831737
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
c : ℝ≥0∞
⊢ (∫ (x : ℝ) in a..b, f x ∂c • μ) = ENNReal.toReal c • ∫ (x : ℝ) in a..b, f x ∂μ
simp only [intervalIntegral, Measure.restrict_smul, integral_smul_measure, smul_sub]