no goals
α : Type u_1
β : Type ?u.9814
γ : Type ?u.9817
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_2
t : (a : α) → Finset (δ a)
⊢ Finset.card (piFinset t) = ∏ a : α, Finset.card (t a)
simp [Fintype.piFinset, card_map]