If $G$ is a group, Bavard showed that the stable commutator length vanishes on $[G,G]$ if and only if $G$ admits no nontrivial "homogeneous quasimorphisms". These functions (on the space of group $1$-boundaries) are constructed using the Hahn-Banach theorem, but are usually very hard (or impossible) to write down explicitly.
Another example: let $M$ be a triangulated manifold, and suppose we orient every edge of every simplex in such a way that the orientations come from a "total order" on each triangle. We would like to assign positive "lengths" to each edge in such a way that on each triangle, the sum of the values on the "short edges" is equal to the value on the "long edge" (where "short" and "long" are defined according to the orientations). The (finite-dimensional!) Hahn-Banach theorem tells us we can do this if and only if every oriented loop in the 1-skeleton is homologically essential; i.e. "homological positivity" can be improved to "chain positivity". Of course the finite-dimensional Hahn-Banach theorem is just a psychological crutch, but versions of this construction in other categories need the "real" Hahn-Banach theorem (applied to certain spaces of de Rham currents).
