no goals
α : Type u_1
β : Type ?u.313618
γ : Type ?u.313621
ι : Type ?u.313624
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
M : Type u_2
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l : List (α → M)
hl : ∀ (f : α → M), f ∈ l → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => List.prod (List.map (fun f => f x) l)) μ
simpa only [← Pi.list_prod_apply] using l.aestronglyMeasurable_prod' hl