Solution
= Solution
Take the divergence of the field equation. Commuting <derivatives> and antisymmetry of $F^{\mu\nu}$ give
$$
\partial_\nu\partial_\mu F^{\mu\nu}=0.
$$
Current conservation then yields
$$
-m^2\partial_\nu A^\nu=-\mu_0\partial_\nu J^\nu=0.
$$
For $m>0$,
$$
\boxed{\partial_\mu A^\mu=0.}
$$
This is the <Lorenz constraint in Proca theory>; it follows dynamically rather than being a gauge choice.