n b : ℕ
L : List ℕ
⊢ List.foldr (fun x y => ↑x + b * y) 0 L = List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length L)) L)
n b : ℕ
L : List ℕ
⊢ ofDigits b L = List.sum (List.mapIdx (fun i a => a * b ^ i) L)
rw [List.mapIdx_eq_enum_map, List.enum_eq_zip_range, List.map_uncurry_zip_eq_zipWith,
  ofDigits_eq_foldr]
case nil
n b : ℕ
⊢ List.foldr (fun x y => ↑x + b * y) 0 [] =
    List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length [])) [])

case cons
n b hd : ℕ
tl : List ℕ
hl :
  List.foldr (fun x y => ↑x + b * y) 0 tl =
    List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length tl)) tl)
⊢ List.foldr (fun x y => ↑x + b * y) 0 (hd :: tl) =
    List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length (hd :: tl))) (hd :: tl))
n b : ℕ
L : List ℕ
⊢ List.foldr (fun x y => ↑x + b * y) 0 L = List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length L)) L)
induction' L with hd tl hl
no goals
case nil
n b : ℕ
⊢ List.foldr (fun x y => ↑x + b * y) 0 [] =
    List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length [])) [])
simp
no goals
case cons
n b hd : ℕ
tl : List ℕ
hl :
  List.foldr (fun x y => ↑x + b * y) 0 tl =
    List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length tl)) tl)
⊢ List.foldr (fun x y => ↑x + b * y) 0 (hd :: tl) =
    List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length (hd :: tl))) (hd :: tl))
simpa [List.range_succ_eq_map, List.zipWith_map_left, ofDigits_eq_sum_map_with_index_aux] using
  Or.inl hl