rw [← h1.right, ofDigits_append, ofDigits_digits, ofDigits_singleton, add_comm, mul_comm]
case h.succ.right
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)
⊢ 6 * 10 ^ (digits 10 ((n + 1) / 10)).length + (n + 1) / 10 = 4 * (n + 1)
no goals