no goals
α✝ : Type ?u.55973
β : Type ?u.55976
n : ℕ
α : Type u_1
inst✝¹ : Fintype α
k : ℕ
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = Nat.choose (Fintype.card α + k - 1) k
rw [card_sym_eq_multichoose, Nat.multichoose_eq]