Lean-Workbook Plus 11366: Trigonometric inequality

Prove that $\sin x+\cos x\leq\sqrt 2$ , where $\ x\in\left(0,\frac{\pi}{2}\right)$ .

Source: Lean-Workbook row lean_workbook_plus_11366 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.