case nil
n : ℕ
⊢ ofDigits 1 [] = List.sum []

case cons
n head✝ : ℕ
tail✝ : List ℕ
ih : ofDigits 1 tail✝ = List.sum tail✝
⊢ ofDigits 1 (head✝ :: tail✝) = List.sum (head✝ :: tail✝)
n : ℕ
L : List ℕ
⊢ ofDigits 1 L = List.sum L
induction' L with _ _ ih
no goals
case nil
n : ℕ
⊢ ofDigits 1 [] = List.sum []
rfl
no goals
case cons
n head✝ : ℕ
tail✝ : List ℕ
ih : ofDigits 1 tail✝ = List.sum tail✝
⊢ ofDigits 1 (head✝ :: tail✝) = List.sum (head✝ :: tail✝)
simp [ofDigits, List.sum_cons, ih]