Asymmetric $A \iff B$ proofs

This is not exactly about an equivalence. But the same question can be raised whether, in an existence and uniqueness theorem, the proof of existence uses proven uniqueness, or the converse. I have one example of both situations:

In elliptic linear PDE, one often apply Lax-Milgram Theorem. The proof of existence does involve the quite obvious uniqueness.

More involved : the KdV equation $u_t+uu_x+u_{xxx}=0$ admits an infinite list of conserved quantities, parametrized by a natural integer (Gardner, Greene, Kruskal & Miura) $$I_n=\int_{-\infty}^{+\infty}\left((d^nu/dx^n)^2+\cdots\right)dx.$$ I proved that the list is complete (there does nt exist other invariants in the form of an integral involving $u$ and finitely many derivatives), and the proof needs the knowledge of the list.

The proof of the Shephard-Todd theorem proceeds exactly that way. The theorem can be stated as:

For a finite subgroup $G\subset GL(n,\mathbb C)$ the following are equivalent:

(A) $G$ is generated by complex reflections (i.e., elements $g$ with $\text{rank}(g-\mathbf1_n)=1$).

(B) The ring of invariants $\mathbb C[x_1,\ldots,x_n]^G$ is a polynomial ring.

First, Shephard-Todd prove $A\Rightarrow B$ by classifying all complex reflection groups and then proceed by inspection (Chevalley found later a conceptual proof of this direction).

To prove $B\Rightarrow A$ let $H\subseteq G$ be the subgroup generated by all complex reflections. From $A\Rightarrow B$ one gets that $\mathbb C[x_1,\ldots,x_n]^H=\mathbb C[y_1,\ldots,y_n]=:P$ is a polynomial ring. By assumption $\mathbb C[x_1,\ldots,x_n]^G=\mathbb C[z_1,\ldots,z_n]=:Q$. The ring extension $P|Q$ is, by construction, unramified in codimension one. On the other hand it is ramified along the zero set of the Jacobian $\det(\partial z_i/\partial y_j)$. So $P=Q$ and therefore $H=G$.

Lafforgue's proof of the Langlands correspondence over function fields provides an important example.

The Langlands correspondence over a function field can be expressed, roughly, as an "if and only if" statement:

An assignment of conjugacy classes in $GL_n$ to the closed points of an algebraic curve $X$ over a finite field $k$ is the set of Frobenius conjugacy classes of some irreducible $n$-dimensional $\operatorname{Gal}(k(X))$-representation of and only if it is the set of Satake parameters of some cuspidal automorphic form on $GL_n(k(X))$.

L. Lafforgue proved both directions of this. He proved the "if" direction directly, by a geometric argument involving the moduli space of shtukas, building on work of Drinfeld and others. He deduced the "only if" direction from the "if" direction for smaller $n$ via the converse theorem.

V. Lafforgue generalized the "if" to an arbitrary group, but the second part breaks down in the case of a general group as the converse theorem is not available there.