The potential attains its minimum at $\phi_{\min}$, Eq. (21)

Let $V=V_1+V_2$ be the potential of Eq. (19), with $A>0$, $\phi_c>0$, and suppose the effective self-coupling is positive, $\tilde\alpha=\alpha+4A^4/\phi_c^4>0$ (equivalently $\alpha>-4A^4/\phi_c^4$). Define

Then $V(\phi_{\min})\le V(\phi)$ for every real $\phi$, i.e. the minimum of the potential occurs at $\phi_{\min}$ (Eq. (21)).

Formalization Note Lean's real square root returns $0$ for negative arguments. When $m^2\ge4A^4/\phi_c^2$ the radicand is negative, $\phi_{\min}=0$, and the statement says that the minimum is at the origin, which is correct in that regime. In the regime the paper has in mind ($m^2\ll4A^4/\phi_c^2$) the radicand is positive and $\phi_{\min}\approx\phi_c$.