König's inequality:
If $\kappa_\alpha<\lambda_\alpha$ for all $\alpha<\mu$, then $\sum\kappa_\alpha<\prod\lambda_\alpha$.
In order to prove this inequality, we need to provide an injection and show there is no surjection, but I failed to see why AC is needed in the proof. Surely the definition of cardinal product needs AC, but we can view it as a set, not a cardinal, just like Cantor's argument showing $A\prec2^A$.
König’s inequality in its full form implies the axiom of choice. Let $\{A_i:i\in I\}$ be a set of non-empty sets. Clearly $|\varnothing|<|A_i|$ for each $i\in I$, so by König’s inequality we have
$$0<\left|\prod_{i\in I}A_i\right|$$
and hence
$$\prod_{i\in I}A_i\ne\varnothing\;.$$
This is one of the many equivalent forms of $\mathsf{AC}$.