I have the following proof which I think might use the axiom of choice implicitly:
Let $\mathcal{A}$ be a pairwise disjoint cover of a set $S\neq \emptyset$ such that $A\cap S\neq \emptyset$ for all $A\in \mathcal{A}$. Then $\vert \mathcal{A}\vert \leq \vert S\vert$, since we have an surjective function $\Phi:S\to \mathcal{A}$ by choosing for all $s\in S$ the unique set $A\in\mathcal{A}$ for which $s\in A$. It seems to me that this map is indeed well defined since the assumptions on $\mathcal{A}$ ensure such an $A$, but this feels like there is a choice being made here.
I would appreciate if someone could point out if I'm overlooking something, or just overcomplicating the argument.
Yes, of course there is a use of AC here. You are proving, in effect, that if there is a surjection from $X$ onto $Y$, then there is an injection from $Y$ into $X$.
This is known as "The Partition Principle", and I have minced many a word on that topic over this site and the interwebs. It implies, for example, that every infinite set has a countably infinite subset, or that every well-ordered family of non-empty sets admits a choice function. Both of these are known to be unprovable from $\sf ZF$.
You might ask whether or not The Partition Principle implies the Axiom of Choice, that is, do we need the full power of AC to prove this statement. And the answer is that we do not know yet. This has been open for over a century. Very recently a proof was suggested using a new technique, but there are several significant flaws and gap in that paper, so the problem is still open.