Lean-Workbook Plus 78333: An affine angle has a unique value in the first quadrant

For $0<\theta<\pi/2$, there is exactly one $u\in(0,\pi/2)$ satisfying $u=(\theta+\pi)/3$.

Source: Lean-Workbook row lean_workbook_plus_78333 (Apache-2.0), original record. This repair only restores required imports and namespaces; the mathematical declaration is unchanged.