no goals
α : Type u_2
β : Type ?u.330452
γ : Type ?u.330455
ι✝ : Type ?u.330458
inst✝⁵ : Countable ι✝
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
f✝ g : α → β
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
ι : Type u_1
f : ι → α → M
s : Finset ι
hf : ∀ (i : ι), i ∈ s → AEStronglyMeasurable (f i) μ
⊢ AEStronglyMeasurable (fun a => ∏ i in s, f i a) μ
simpa only [← Finset.prod_apply] using s.aestronglyMeasurable_prod' hf