induction j generalizing i with
| zero =>
  intro acc
  simp at hj; cases hj
  unfold foldl.loop; unfold foldl'.aux
  simp
| succ j' ih =>
  intro acc
  simp_all
  rw [Nat.add_succ, ← Nat.succ_add] at hj
  have hi : i < n := by calc
    _ ≤ Nat.succ i + j' := Nat.le_add_right _ _
    _ = n := hj
  have := ih (i+1) hj (f acc ⟨i,hi⟩)
  clear ih
  unfold foldl.loop; unfold foldl'.aux
  simp [*]
α : Sort u_1
n : ℕ
f : α → Fin n → α
init : α
i j : ℕ
hj : i + j = n
⊢ ∀ (acc : α), foldl.loop n f acc i = foldl'.aux n init (fun i h acc => f acc ⟨i, h⟩) i ⋯ acc
no goals