Nested irrational powers

$((\sqrt3)^{\sqrt2})^{\sqrt2}=\sqrt9=3$, with real exponentiation. The formal statement asserts the equality to $\sqrt9$.

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