induction m generalizing n k init with
| zero =>
  rewrite [zero_eq, Nat.zero_add] at h; cases h
  simp only [fold'TR.loop, zero_eq]
| succ m IH =>
  rewrite [Nat.succ_add] at h; cases h
  dsimp [fold'TR.loop]
  have := fun a => IH a (n+1) (m+n+1) rfl f
  conv at this =>
    ext a; lhs; arg 5; rewrite [fold'_succ]
  rewrite [← this init]
  apply congrArg; apply congrFun; apply congrArg
  apply Fin.eq_of_val_eq
  simp only [Nat.succ_sub_succ_eq_sub, Nat.add_sub_cancel_left]
  rfl
case h.h.h.h
α : Type u_1
init : α
m n k : Nat
h : m + n = k
f : Fin k → α → α
⊢ fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) = fold' k f init
no goals