no goals
α : Type u_1
β : Type ?u.327416
γ : Type ?u.327419
ι : Type ?u.327422
inst✝⁵ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f g : α → β
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
s : Multiset (α → M)
hs : ∀ (f : α → M), f ∈ s → AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => Multiset.prod (Multiset.map (fun f => f x) s)) μ
simpa only [← Pi.multiset_prod_apply] using s.aestronglyMeasurable_prod' hs