no goals
α : Type u_2
β : Type ?u.131099
γ : Type ?u.131102
ι✝ : Type ?u.131105
inst✝³ : Countable ι✝
f✝ g : α → β
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
m : MeasurableSpace α
ι : Type u_1
f : ι → α → M
s : Finset ι
hf : ∀ (i : ι), i ∈ s → StronglyMeasurable (f i)
⊢ StronglyMeasurable fun a => ∏ i in s, f i a
simpa only [← Finset.prod_apply] using s.stronglyMeasurable_prod' hf