no goals
ι : Type ?u.14415591
𝕜 : Type u_1
E : Type u_3
F : Type u_2
A : Type ?u.14415603
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : CompleteSpace E
inst✝⁴ : NormedSpace ℝ E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
f : ℝ → E
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
a b : ℝ
φ : ℝ → F →L[𝕜] E
hφ : IntervalIntegrable φ μ a b
v : F
⊢ ↑(∫ (x : ℝ) in a..b, φ x ∂μ) v = ∫ (x : ℝ) in a..b, ↑(φ x) v ∂μ
simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def v, coe_smul', Pi.smul_apply]