case nil
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
⊢ ofDigits b [] = List.foldr (fun x y => ↑x + b * y) 0 []

case cons
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
⊢ ofDigits b (d :: L) = List.foldr (fun x y => ↑x + b * y) 0 (d :: L)
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
L : List ℕ
⊢ ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
induction' L with d L ih
no goals
case nil
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
⊢ ofDigits b [] = List.foldr (fun x y => ↑x + b * y) 0 []
rfl
case cons
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
⊢ ↑d + b * ofDigits b L = ↑d + b * List.foldr (fun x y => ↑x + b * y) 0 L
case cons
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
⊢ ofDigits b (d :: L) = List.foldr (fun x y => ↑x + b * y) 0 (d :: L)
dsimp [ofDigits]
no goals
case cons
n : ℕ
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
⊢ ↑d + b * ofDigits b L = ↑d + b * List.foldr (fun x y => ↑x + b * y) 0 L
rw [ih]