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