exact helper_5_digit h4
c n : ℕ
h2 : ProblemPredicate' c n
h1 : ↑(digits 10 c).length = 5
h3 : 6 * 10 ^ 5 + ↑c = 6 * 10 ^ (digits 10 c).length + ↑c
h4 : 6 * 10 ^ 5 + ↑c = 4 * (10 * ↑c + 6)
⊢ ↑c = 15384
no goals