no goals
ι : Type ?u.13121336
𝕜✝ : Type ?u.13121339
E : Type u_2
F : Type ?u.13121345
A : Type ?u.13121348
inst✝⁴ : NormedAddCommGroup E
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
a b : ℝ
f✝ g : ℝ → E
μ : MeasureTheory.Measure ℝ
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
inst✝ : NormedSpace 𝕜 E
f : ℝ → 𝕜
c : E
⊢ (∫ (x : ℝ) in a..b, f x • c ∂μ) = (∫ (x : ℝ) in a..b, f x ∂μ) • c
simp only [intervalIntegral_eq_integral_uIoc, integral_smul_const, smul_assoc]