α : Type u_1
β : Type u_2
γ : Type ?u.12409
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card β ^ Finset.card univ = card β ^ card α
α : Type u_1
β : Type u_2
γ : Type ?u.12409
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card (α → β) = card β ^ card α
rw [Fintype.card_pi, Finset.prod_const]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.12409
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card β ^ Finset.card univ = card β ^ card α
rfl