Theorem: LeanColls.Range.fold_def (LeanColls/Data/Range.lean)

State before:
β : Type u_1
init : β
r : Range
f : β → ℕ → β
⊢ fold r f init = Fin.foldl r.size (fun acc i => f acc (r.get i)) init
Tactic:
simp [fold, foldl, Fin.foldl]
State after:
β : 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

State before:
β : 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
Tactic:
sorry
State after:
no goals