no goals
ι : Type ?u.1621986
𝕜 : Type ?u.1621989
E : Type u_1
F : Type ?u.1621995
A : Type ?u.1621998
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
⊢ IntervalIntegrable f μ a a
constructor <;> simp