rw [ProblemPredicate, digits_def' (by decide : 2 ≤ 10) n.succ_pos, List.headI, List.tail_cons,
  List.concat_eq_append] at h1
case h.succ
n : ℕ
h1 : ProblemPredicate (n + 1)
⊢ ProblemPredicate' ((n + 1) / 10) (n + 1)
case h.succ
n : ℕ
h1 :
  (match n.succ % 10 :: digits 10 (n.succ / 10) with
      | [] => default
      | a :: tail => a) =
      6 ∧
    ofDigits 10 (digits 10 (n.succ / 10) ++ [6]) = 4 * (n + 1)
⊢ ProblemPredicate' ((n + 1) / 10) (n + 1)