α : Type u_1
β : Type ?u.25052
s : Multiset α
this : ↑card (powerset s) = 2 ^ ↑card s
⊢ ↑card (antidiagonal s) = 2 ^ ↑card s
α : Type u_1
β : Type ?u.25052
s : Multiset α
⊢ ↑card (antidiagonal s) = 2 ^ ↑card s
have := card_powerset s
no goals
α : Type u_1
β : Type ?u.25052
s : Multiset α
this : ↑card (powerset s) = 2 ^ ↑card s
⊢ ↑card (antidiagonal s) = 2 ^ ↑card s
rwa [← antidiagonal_map_fst, card_map] at this