no goals
α : Type u_2
ι : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NeBot l
inst✝ : IsCountablyGenerated l
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ≥0
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) ≤ ↑I
⊢ ∀ᶠ (i : ι) in l, (∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) ≤ ENNReal.ofReal ↑I
simpa only [ENNReal.ofReal_coe_nnreal] using hbounded