This question is not precise, but I believe has a precise formulation.

Consider a mathematical theorem which gives an equivalency between two conditions. As an extreme example:

\begin{theorem} A compact 3-manifold is simply-connected if and only if it is homeomorphic to the 3-sphere. \end{theorem} The if direction is an exercise in a first course in algebraic topology, and the only if direction is a celebrated result of Perelman.

The question is, are there results which have been shown that one direction of a proof is "harder" than the other?

Certain equivalence proofs seem to have the same complexity in both directions, when all the steps of the proof are reversible.

I think this can be formulated as a precise way, by asking for the length of a proof in a standard proof system. One might also be able to give a precise formulation in terms of the Kolmogorov complexity of a proof.

On the other hand, I can imagine results of the sort that say that for any equivalency, there is a proof system for which one direction is shorter than the other, and another proof system where the reverse holds. So I'm not certain that this question is well-defined. But I think it is well-defined for certain proof systems.

So a more precise question: Is there an equivalence theorem and a proof system, for which it has been shown that one direction of a proof must have a longer proof than the other direction?