case nil
n b : ℕ
l2 : List ℕ
⊢ ofDigits b ([] ++ l2) = ofDigits b [] + b ^ List.length [] * ofDigits b l2

case cons
n b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ List.length tl * ofDigits b l2
⊢ ofDigits b (hd :: tl ++ l2) = ofDigits b (hd :: tl) + b ^ List.length (hd :: tl) * ofDigits b l2
n b : ℕ
l1 l2 : List ℕ
⊢ ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ List.length l1 * ofDigits b l2
induction' l1 with hd tl IH
no goals
case nil
n b : ℕ
l2 : List ℕ
⊢ ofDigits b ([] ++ l2) = ofDigits b [] + b ^ List.length [] * ofDigits b l2
simp [ofDigits]
case cons
n b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ List.length tl * ofDigits b l2
⊢ ↑hd + b * (ofDigits b tl + b ^ List.length tl * ofDigits b l2) =
    ↑hd + b * ofDigits b tl + b * b ^ List.length tl * ofDigits b l2
case cons
n b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ List.length tl * ofDigits b l2
⊢ ofDigits b (hd :: tl ++ l2) = ofDigits b (hd :: tl) + b ^ List.length (hd :: tl) * ofDigits b l2
rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']
no goals
case cons
n b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ List.length tl * ofDigits b l2
⊢ ↑hd + b * (ofDigits b tl + b ^ List.length tl * ofDigits b l2) =
    ↑hd + b * ofDigits b tl + b * b ^ List.length tl * ofDigits b l2
ring