no goals
ι : Type ?u.770262
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f g : α → β
⊢ ∏ x in s, piecewise t f g x = (∏ x in s ∩ t, f x) * ∏ x in s \ t, g x
erw [prod_ite, filter_mem_eq_inter, ← sdiff_eq_filter]