no goals
M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
l : List (α → M)
hl : ∀ (f : α → M), f ∈ l → AEMeasurable f
⊢ AEMeasurable fun x => prod (map (fun f => f x) l)
simpa only [← Pi.list_prod_apply] using l.aemeasurable_prod' hl