Lean-Workbook Plus 43717: Exponential identity

For every real $x$, $\frac{e^x}{4+5e^{3x}}\frac{e^{-x}}{e^{-x}}=\frac1{4e^{-x}+5e^{2x}}$. This asserts the algebraic identity used in the source’s limit discussion.

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