Both double-angle values from sine and cosine

Find $\cos(2\alpha)$ and $\sin(2\alpha)$ if $\cos\alpha = \frac{4}{5}$ and $\sin\alpha = \frac{3}{5}$.

Source: InternLM Lean-Workbook, record lean_workbook_56440 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.