The product of two nine-digit integers

Now, \begin{align*} 123456789 \cdot 987654321 &= \left(\dfrac{10^{10} - 91}{81}\right)\left(\dfrac{8 \cdot 10^{10} + 1}{81}\right) \ &= \dfrac{8 \cdot 10^{20} + 10^{10} - 728 \cdot 10^{10} - 91}{81^2} \end{align*} The numerator can be easily calculated with some addition and subtraction. We get: \begin{align*} 123456789 \cdot 987654321 &= \dfrac{8 \cdot 10^{20} + 10^{10} - 728 \cdot 10^{10} - 91}{6561} \ &= \dfrac{799 999 992 729 999 999 909}{6561} \end{align*} Long division isn't too tedious, calculating gives: $123456789 \cdot 987654321 = 121932631112635269$ and we are done.

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