no goals
ι : Type ?u.14661329
𝕜 : Type u_1
E : Type u_2
F : Type u_3
A : Type ?u.14661341
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
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
⊢ (∫ (x : ℝ) in a..b, ↑L (f x) ∂μ) = ↑L (∫ (x : ℝ) in a..b, f x ∂μ)
simp_rw [intervalIntegral, L.integral_comp_comm hf.1, L.integral_comp_comm hf.2, L.map_sub]