have h5 : c > 153 := by linarith
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 3 + c = 4 * (10 * c + 6)
⊢ False
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 3 + c = 4 * (10 * c + 6)
h5 : c > 153
⊢ False