induction j generalizing init i with
| zero =>
  unfold foldl.loop
  simp at h
  simp [List.drop_eq_nil_of_le, h]
| succ j ih =>
  unfold foldl.loop
  have : i < n := by omega
  simp [this, cast]
  generalize f init _ = init'
  have : (i+1) + j = n := by omega
  specialize ih init' (i+1) this
  rw [ih]; clear ih
  congr
  funext ⟨x,hx⟩; simp; omega
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i j : ℕ
h : i + j = n
⊢ foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
no goals