no goals
α : Type u
β : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
b : β
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : Finset α → β
⊢ ∏ t in powerset s, f t = ∏ j in range (card s + 1), ∏ t in powersetLen j s, f t
rw [powerset_card_disjiUnion, prod_disjiUnion]