[Merged by Bors] - feat(archive/imo): formalize IMO 1962 problem Q1

[lacker]

The problem statement:

Find the smallest natural number $n$ which has the following properties:
(a) Its decimal representation has 6 as the last digit.
(b) If the last digit 6 is erased and placed in front of the remaining digits,
the resulting number is four times as large as the original number $n$.

This is a proof that 153846 is the smallest member of the set satisfying these conditions.

---

• depends on: [Merged by Bors] - feat(data/nat/digits): add norm_digits tactic #4452

[jcommelin]

Please fix the PR title.

[jsm28]

without_digits should imply (6 * 10 ^ (nat.digits 10 c).length) % 39 = 24, which should be testable for each number of digits using norm_num, no linarith needed.

[jsm28]

That is, 6 * 10 ^ (nat.digits 10 c).length = 39 * c + 24.

[lacker]

without_digits should imply (6 * 10 ^ (nat.digits 10 c).length) % 39 = 24, which should be testable for each number of digits using norm_num, no linarith needed.

I tried it this way, and it does work, but the solution ends up being more complicated than this is right now. It doesn't shorten the logic for each number of digits - see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/unexpected.20.22bit0.22.2C.20.22bit1.22.20etc for discussion - and it requires the extra proof of (6 * 10 ^ (nat.digits 10 c).length) % 39 = 24. So I suggest keeping this part as linarith applications.

[bryangingechen]

@lacker I pushed a few changes. Mostly stylistic, but I also removed solutions_nonempty since it's implicit in imo1962_q1.

If you're happy with my edits, feel free to merge.

bors d+

[bors]

✌️ lacker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[lacker]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests