no goals
α : Type u_1
s✝ t : Finset α
inst✝ : DecidableEq (Finset α)
s : Finset α
⊢ powerset s = Finset.biUnion (range (card s + 1)) fun i => powersetLen i s
simpa only [disjiUnion_eq_biUnion] using powerset_card_disjiUnion s