n b : ℕ
l : List ℕ
⊢ List.zipWith ((fun i a => a * b ^ i) ∘ succ) (List.range (List.length l)) l =
    List.zipWith (fun i a => b * (a * b ^ i)) (List.range (List.length l)) l
n b : ℕ
l : List ℕ
⊢ List.sum (List.zipWith ((fun i a => a * b ^ i) ∘ succ) (List.range (List.length l)) l) =
    b * List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length l)) l)
suffices
  (List.range l.length).zipWith ((fun i a : ℕ => a * b ^ i) ∘ succ) l =
    (List.range l.length).zipWith (fun i a => b * (a * b ^ i)) l
  by simp [this]
case e_f
n b : ℕ
l : List ℕ
⊢ (fun i a => a * b ^ i) ∘ succ = fun i a => b * (a * b ^ i)
n b : ℕ
l : List ℕ
⊢ List.zipWith ((fun i a => a * b ^ i) ∘ succ) (List.range (List.length l)) l =
    List.zipWith (fun i a => b * (a * b ^ i)) (List.range (List.length l)) l
congr
case e_f.h.h
n b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ ((fun i a => a * b ^ i) ∘ succ) x✝¹ x✝ = b * (x✝ * b ^ x✝¹)
case e_f
n b : ℕ
l : List ℕ
⊢ (fun i a => a * b ^ i) ∘ succ = fun i a => b * (a * b ^ i)
ext
case e_f.h.h
n b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝ * (b ^ x✝¹ * b) = b * (x✝ * b ^ x✝¹)
case e_f.h.h
n b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ ((fun i a => a * b ^ i) ∘ succ) x✝¹ x✝ = b * (x✝ * b ^ x✝¹)
simp [pow_succ]
no goals
case e_f.h.h
n b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝ * (b ^ x✝¹ * b) = b * (x✝ * b ^ x✝¹)
ring
no goals
n b : ℕ
l : List ℕ
this :
  List.zipWith ((fun i a => a * b ^ i) ∘ succ) (List.range (List.length l)) l =
    List.zipWith (fun i a => b * (a * b ^ i)) (List.range (List.length l)) l
⊢ List.sum (List.zipWith ((fun i a => a * b ^ i) ∘ succ) (List.range (List.length l)) l) =
    b * List.sum (List.zipWith (fun i a => a * b ^ i) (List.range (List.length l)) l)
simp [this]