no goals
ι : Type ?u.9461654
𝕜 : Type ?u.9461657
E : Type u_1
F : Type ?u.9461663
A : Type ?u.9461666
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
⊢ (∫ (x : ℝ) in a..b, 0 ∂μ) = 0
simp [intervalIntegral]