Solution (source code)

= Solution

For the <Cauchy-Schwarz inequality>, take $\lambda=(\mathbf x\cdot\mathbf y)/(\mathbf y\cdot\mathbf y)$ and use positivity of the <inner product>:
$$
0\leq|\mathbf x-\lambda\mathbf y|^2
=\mathbf x\cdot\mathbf x-\frac{(\mathbf x\cdot\mathbf y)^2}{\mathbf y\cdot\mathbf y}.
$$
Multiplication by $\mathbf y\cdot\mathbf y>0$ proves
$$
\boxed{(\mathbf x\cdot\mathbf y)^2\leq(\mathbf x\cdot\mathbf x)(\mathbf y\cdot\mathbf y).}
$$
Equality holds exactly when $|\mathbf x-\lambda\mathbf y|^2=0$. Positive definiteness of the <inner product> makes this equivalent to $\mathbf x=\lambda\mathbf y$. Conversely, substitution of a scalar multiple gives equality. Thus \b[equality holds precisely for linearly dependent nonzero vectors].