An exponential power with logarithmic exponent

Given $a=e$ and $b=\ln 2$, both are irrational but $a^b = 2$ which is rational.

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