no goals
ι : Type ?u.13951224
𝕜✝ : Type ?u.13951227
E : Type ?u.13951230
F : Type ?u.13951233
A : Type ?u.13951236
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
a b : ℝ
μ : MeasureTheory.Measure ℝ
f : ℝ → ℝ
⊢ (∫ (x : ℝ) in a..b, ↑(f x) ∂μ) = ↑(∫ (x : ℝ) in a..b, f x ∂μ)
simp only [intervalIntegral, integral_ofReal, IsROrC.ofReal_sub]