induction i generalizing o with
| zero =>
  unfold Std.Range.forIn'.loop
  unfold Std.Range.forIn'.loop
  simp
| succ i ih =>
  conv => lhs; unfold Std.Range.forIn'.loop
  conv => rhs; unfold Std.Range.forIn'.loop
  simp
  have hn := Nat.sub_lt_of_pos_le (Nat.succ_pos _) hi
  have hn' : n - Nat.succ i < Nat.succ n := Nat.le_step hn
  simp [hn, hn']
  have : n - Nat.succ i + 1 = n - i := by
    simp [Nat.sub_succ]
    rw [Nat.add_one, Nat.succ_pred_eq_of_pos (Nat.zero_lt_sub_of_lt hi)]
  suffices ∀ j, j = n - Nat.succ i + 1 →
    Std.Range.forIn'.loop (m := Id)  _ _ _ _ _ j (Nat.zero_le _) _
    = push (Std.Range.forIn'.loop (m := Id) _ _ _ _ _ j (Nat.zero_le _) _) _
    from this _ rfl
  intro j hj
  rw [this] at hj
  cases hj
  apply ih
  exact Nat.le_of_lt hi
  simp [ho, this]
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
hi : i ≤ n
o : Array α
ho : size o = n - i
⊢ Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
      (Nat.succ i) (n - i) ⋯ o =
    push (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i (n - i) ⋯ o)
      (f { val := n, isLt := ⋯ })
no goals