simp [fold, foldl, Fin.foldl]
β : Type u_1
init : β
r : Range
f : β → ℕ → β
⊢ fold r f init = Fin.foldl r.size (fun acc i => f acc (r.get i)) init
β : Type u_1
init : β
r : Range
f : β → ℕ → β
⊢ foldl.aux r f r.start ⋯ init = Fin.foldl.loop r.size (fun acc i => f acc (r.get i)) init 0