norm_num at h5
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
h5 : n = 10 * 15384 + 6
⊢ n ≥ 153846
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
h5 : n = 153846
⊢ n ≥ 153846