lean_workbook_plus_78367
ProvedNote that (here, in contrast to above, the overline means repeating, not the number). It is well known that fractions of simply rotate the digits around. For example, starts with the digit and equals . If you've never seen this before, go ahead and divide out the other fractions to see! Knowing this, the problem actually becomes very easy if it is short answer. Since , and is only a rotation of the digits, specifically , we can find that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78367 : 6 * (142857) = 857142 := by sorry
Source