induction s using Finset.cons_induction <;> simp [*]
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : CommMonoid β
f : ι → SimpleFunc α β
s : Finset ι
⊢ ↑(∏ i in s, f i) = ∏ i in s, ↑(f i)
no goals