no goals
α : Type ?u.1025603
β : Type ?u.1025606
ι : Type ?u.1025609
E : Type ?u.1025612
F : Type ?u.1025615
𝕜 : Type ?u.1025618
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : Integrable f
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}
simp