From daa660ca996766ca2b4dddb292793997f9bfa8c5 Mon Sep 17 00:00:00 2001
From: Thomas Browning <tb65536@uw.edu>
Date: Wed, 5 Oct 2022 18:04:14 +0000
Subject: [PATCH] feat(set_theory/cardinal/finite): Add `nat.card_fun` (#16799)

This PR adds `nat.card_fun`, a quick consequence of `nat.card_pi`.
---
 src/set_theory/cardinal/finite.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/set_theory/cardinal/finite.lean b/src/set_theory/cardinal/finite.lean
index 253489173c994..0aa0b280c13cd 100644
--- a/src/set_theory/cardinal/finite.lean
+++ b/src/set_theory/cardinal/finite.lean
@@ -84,6 +84,12 @@ card_congr equiv.plift
 lemma card_pi {β : α → Type*} [fintype α] : nat.card (Π a, β a) = ∏ a, nat.card (β a) :=
 by simp_rw [nat.card, mk_pi, prod_eq_of_fintype, to_nat_lift, to_nat_finset_prod]
 
+lemma card_fun [finite α] : nat.card (α → β) = nat.card β ^ nat.card α :=
+begin
+  haveI := fintype.of_finite α,
+  rw [nat.card_pi, finset.prod_const, finset.card_univ, ←nat.card_eq_fintype_card],
+end
+
 @[simp] lemma card_zmod (n : ℕ) : nat.card (zmod n) = n :=
 begin
   cases n,