∀ {ι : Type u_1} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] {p : ι → Prop} [inst_1 : DecidablePred p] {f : ι → M₀}
  {s : Finset ι}, (∏ i ∈ s, if p i then f i else 0) = if ∀ i ∈ s, p i then ∏ i ∈ s, f i else 0