feedback on first lean function

Stream: new members

[Francisco Giordano]

I've written my first non-trivial Lean function and would really appreciate feedback from more experienced Lean users about what I could be doing better.

My goal was to iterate through a list with an index like foldlIdx, but with the index proven to be in-range via Fin.

def foldlIdx (l : List a) (f : Fin l.length → b → a → b) (init : b) : b :=
  let rec foldlIdx' state (i : Nat) (l' : List a) (h : l.length = l'.length + i) :=
    match l' with
    | [] => state
    | x :: l'' =>
      let isLt : i < l.length := by
        rw [h]
        simp
        exact Nat.lt_add_of_pos_left (Nat.succ_pos _)
      let h' := by
        rw [h]
        simp
        rw [Nat.succ_eq_add_one, Nat.add_right_comm, Nat.add_assoc]
      let state' := f ⟨i, isLt⟩ state x
      foldlIdx' state' (i + 1) l'' h'
  foldlIdx' init 0 l rfl