no goals
α : Type u_2
β✝ : Type ?u.11854
β : α → Type u_1
inst✝ : Fintype α
⊢ Nat.card ((a : α) → β a) = ∏ a : α, Nat.card (β a)
simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, toNat_finset_prod]