no goals
α : Type u_1
β : Type ?u.2694217
γ : Type ?u.2694220
γ₂ : Type ?u.2694223
δ : Type ?u.2694226
ι : Sort y
s t u : Set α
inst✝ : MeasurableSpace α
f : α → ℝ≥0
μ : MeasureTheory.Measure α
h : AEMeasurable fun x => ↑(f x)
⊢ AEMeasurable f
simpa only [Real.toNNReal_coe] using h.real_toNNReal