no goals
M : Type u_3
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : MeasureTheory.Measure α
f : ι → α → M
s : Finset ι
hf : ∀ (i : ι), i ∈ s → Measurable (f i)
⊢ Measurable fun a => ∏ i in s, f i a
simpa only [← Finset.prod_apply] using s.measurable_prod' hf