Does the axiom of choice have any use for finite sets? It is well known that certain properties of infinite sets can only be shown using (some form of) the axiom of choice. I'm reading some introductory lectures about ZFC and I was wondering if there are any properties of finite sets that only hold under AC.

There are two remarks that may be relevant here.
(1) This depends on what you mean by "finite sets". Even for (infinite setts of) pairs the axiom of choice is does not follow from ZF if one looks at an infinite collection. This is popularly known as the "pairs of socks" version of AC which is one of the weakest ones.
(2) If you mean that the family of sets itself is finite, then AC can be proved in ZF by induction, i.e., it is automatic, but this is only true if your background logic is classical.  For intuitionistic logic, the axiom of choice can be very powerful even for finite sets.  For example, there is a theorem that the axiom of choice implies the law of excluded middle; in this sense the introduction of AC "defeats" the intuitionistic logic and turns the situation into a classical one.
