conv => lhs; unfold Std.Range.forIn'.loop
case succ
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
ih :
  i ≤ n →
    ∀ (o : Array α),
      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 := ⋯ })
hi : Nat.succ i ≤ n
o : Array α
ho : size o = n - Nat.succ i
⊢ Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
      (Nat.succ (Nat.succ i)) (n - Nat.succ i) ⋯ o =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) (Nat.succ i)
        (n - Nat.succ i) ⋯ o)
      (f { val := n, isLt := ⋯ })
case succ
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
ih :
  i ≤ n →
    ∀ (o : Array α),
      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 := ⋯ })
hi : Nat.succ i ≤ n
o : Array α
ho : size o = n - Nat.succ i
⊢ (if hu : n - Nat.succ i < Nat.succ n then
      match Nat.succ (Nat.succ i) with
      | 0 => pure o
      | Nat.succ fuel => do
        let __do_lift ← ForInStep.yield (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
        match __do_lift with
          | ForInStep.done b => pure b
          | ForInStep.yield b =>
            Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
              fuel (n - Nat.succ i + 1) ⋯ b
    else pure o) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) (Nat.succ i)
        (n - Nat.succ i) ⋯ o)
      (f { val := n, isLt := ⋯ })