interval_cases h : (digits 10 c).length
case inl
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h3 : (digits 10 c).length < 6
⊢ n ≥ 153846
case inl.«0»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 0
h3 : 0 < 6
⊢ n ≥ 153846

case inl.«1»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 1
h3 : 1 < 6
⊢ n ≥ 153846

case inl.«2»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 2
h3 : 2 < 6
⊢ n ≥ 153846

case inl.«3»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 3
h3 : 3 < 6
⊢ n ≥ 153846

case inl.«4»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 4
h3 : 4 < 6
⊢ n ≥ 153846

case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
⊢ n ≥ 153846