Theorem: SimpleFunc.coe_prod (RandomGraphs/simple_func.lean)

State before:
ι : 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)
Tactic:
induction s using Finset.cons_induction <;> simp [*]
State after:
no goals