Theorem: Array.init_succ (LeanSAT/Upstream/ToStd.lean)

State before:
α : Type ?u.11694
n : Nat
f : Fin (Nat.succ n) → α
i : Fin n
⊢ n < Nat.succ n
Tactic:
exact Nat.le_refl _
State after:
no goals

State before:
α : Type ?u.11694
n : Nat
f : Fin (Nat.succ n) → α
⊢ n < Nat.succ n
Tactic:
exact Nat.le_refl _
State after:
no goals

State before:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
⊢ init (Nat.succ n) f = push (init n fun i => f { val := ↑i, isLt := ⋯ }) (f { val := n, isLt := ⋯ })
Tactic:
simp [init, Id.run, forIn', Std.Range.forIn']
State after:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
⊢ Std.Range.forIn'.loop { start := 0, stop := Nat.succ n, step := 1 }.start
      { start := 0, stop := Nat.succ n, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) (Nat.succ n) 0 ⋯ #[] =
    push
      (Std.Range.forIn'.loop { start := 0, stop := n, step := 1 }.start { start := 0, stop := n, step := 1 }.stop 1
        (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n 0 ⋯ #[])
      (f { val := n, isLt := ⋯ })

State before:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
⊢ Std.Range.forIn'.loop { start := 0, stop := Nat.succ n, step := 1 }.start
      { start := 0, stop := Nat.succ n, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) (Nat.succ n) 0 ⋯ #[] =
    push
      (Std.Range.forIn'.loop { start := 0, stop := n, step := 1 }.start { start := 0, stop := n, step := 1 }.stop 1
        (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n 0 ⋯ #[])
      (f { val := n, isLt := ⋯ })
Tactic:
suffices ∀ i (hi : i ≤ n) o (_ : o.size = n-i),
  Std.Range.forIn'.loop (m := Id) 0 n.succ 1
    (fun i h r => ForInStep.yield (push r (f ⟨i, h.2⟩)))
    i.succ (n-i)
    (Nat.zero_le _)
    o
  = push (Std.Range.forIn'.loop (m := Id) 0 n 1
    (fun i h r => ForInStep.yield (push r (f ⟨i, Nat.le_step h.2⟩)))
    i (n-i)
    (Nat.zero_le _)
    o) (f ⟨n, Nat.lt_succ_self n⟩)
  by
  have := this n (Nat.le_refl _) #[] (by simp)
  simp at this
  exact this
State after:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
⊢ ∀ (i : Nat),
    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 := ⋯ })

State before:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
⊢ ∀ (i : Nat),
    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 := ⋯ })
Tactic:
intro i hi o ho
State after:
α : 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 := ⋯ })

State before:
α : 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 := ⋯ })
Tactic:
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]
State after:
no goals

State before:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
this :
  ∀ (i : Nat),
    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 := ⋯ })
⊢ Std.Range.forIn'.loop { start := 0, stop := Nat.succ n, step := 1 }.start
      { start := 0, stop := Nat.succ n, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) (Nat.succ n) 0 ⋯ #[] =
    push
      (Std.Range.forIn'.loop { start := 0, stop := n, step := 1 }.start { start := 0, stop := n, step := 1 }.stop 1
        (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n 0 ⋯ #[])
      (f { val := n, isLt := ⋯ })
Tactic:
have := this n (Nat.le_refl _) #[] (by simp)
State after:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
this✝ :
  ∀ (i : Nat),
    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 := ⋯ })
this :
  Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
      (Nat.succ n) (n - n) ⋯ #[] =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n (n - n) ⋯ #[])
      (f { val := n, isLt := ⋯ })
⊢ Std.Range.forIn'.loop { start := 0, stop := Nat.succ n, step := 1 }.start
      { start := 0, stop := Nat.succ n, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) (Nat.succ n) 0 ⋯ #[] =
    push
      (Std.Range.forIn'.loop { start := 0, stop := n, step := 1 }.start { start := 0, stop := n, step := 1 }.stop 1
        (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n 0 ⋯ #[])
      (f { val := n, isLt := ⋯ })

State before:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
this✝ :
  ∀ (i : Nat),
    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 := ⋯ })
this :
  Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
      (Nat.succ n) (n - n) ⋯ #[] =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n (n - n) ⋯ #[])
      (f { val := n, isLt := ⋯ })
⊢ Std.Range.forIn'.loop { start := 0, stop := Nat.succ n, step := 1 }.start
      { start := 0, stop := Nat.succ n, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) (Nat.succ n) 0 ⋯ #[] =
    push
      (Std.Range.forIn'.loop { start := 0, stop := n, step := 1 }.start { start := 0, stop := n, step := 1 }.stop 1
        (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n 0 ⋯ #[])
      (f { val := n, isLt := ⋯ })
Tactic:
simp at this
State after:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
this✝ :
  ∀ (i : Nat),
    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 := ⋯ })
this :
  Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
      (Nat.succ n) 0 ⋯ #[] =
    push (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n 0 ⋯ #[])
      (f { val := n, isLt := ⋯ })
⊢ Std.Range.forIn'.loop { start := 0, stop := Nat.succ n, step := 1 }.start
      { start := 0, stop := Nat.succ n, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) (Nat.succ n) 0 ⋯ #[] =
    push
      (Std.Range.forIn'.loop { start := 0, stop := n, step := 1 }.start { start := 0, stop := n, step := 1 }.stop 1
        (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n 0 ⋯ #[])
      (f { val := n, isLt := ⋯ })

State before:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
this✝ :
  ∀ (i : Nat),
    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 := ⋯ })
this :
  Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
      (Nat.succ n) 0 ⋯ #[] =
    push (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n 0 ⋯ #[])
      (f { val := n, isLt := ⋯ })
⊢ Std.Range.forIn'.loop { start := 0, stop := Nat.succ n, step := 1 }.start
      { start := 0, stop := Nat.succ n, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) (Nat.succ n) 0 ⋯ #[] =
    push
      (Std.Range.forIn'.loop { start := 0, stop := n, step := 1 }.start { start := 0, stop := n, step := 1 }.stop 1
        (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n 0 ⋯ #[])
      (f { val := n, isLt := ⋯ })
Tactic:
exact this
State after:
no goals

State before:
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
this :
  ∀ (i : Nat),
    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 := ⋯ })
⊢ size #[] = n - n
Tactic:
simp
State after:
no goals

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
⊢ Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
      (Nat.succ Nat.zero) (n - Nat.zero) ⋯ o =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) Nat.zero
        (n - Nat.zero) ⋯ o)
      (f { val := n, isLt := ⋯ })
Tactic:
unfold Std.Range.forIn'.loop
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 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 := ⋯ })

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
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 := ⋯ })

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 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 := ⋯ })
Tactic:
simp
State after:
no goals

State before:
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 := ⋯ })
Tactic:
conv => lhs; unfold Std.Range.forIn'.loop
State after:
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 := ⋯ })

State before:
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 := ⋯ })
Tactic:
conv => rhs; unfold Std.Range.forIn'.loop
State after:
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
      (if hu : n - Nat.succ i < n then
        match 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 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) fuel
                (n - Nat.succ i + 1) ⋯ b
      else pure o)
      (f { val := n, isLt := ⋯ })

State before:
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
      (if hu : n - Nat.succ i < n then
        match 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 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) fuel
                (n - Nat.succ i + 1) ⋯ b
      else pure o)
      (f { val := n, isLt := ⋯ })
Tactic:
simp
State after:
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 h : n - Nat.succ i < Nat.succ n then
      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 - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
    else o) =
    push
      (if h : n - Nat.succ i < n then
        Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i
          (n - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
      else o)
      (f { val := n, isLt := ⋯ })

State before:
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 h : n - Nat.succ i < Nat.succ n then
      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 - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
    else o) =
    push
      (if h : n - Nat.succ i < n then
        Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i
          (n - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
      else o)
      (f { val := n, isLt := ⋯ })
Tactic:
have hn := Nat.sub_lt_of_pos_le (Nat.succ_pos _) hi
State after:
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
hn : n - Nat.succ i < n
⊢ (if h : n - Nat.succ i < Nat.succ n then
      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 - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
    else o) =
    push
      (if h : n - Nat.succ i < n then
        Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i
          (n - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
      else o)
      (f { val := n, isLt := ⋯ })

State before:
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
hn : n - Nat.succ i < n
⊢ (if h : n - Nat.succ i < Nat.succ n then
      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 - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
    else o) =
    push
      (if h : n - Nat.succ i < n then
        Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i
          (n - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
      else o)
      (f { val := n, isLt := ⋯ })
Tactic:
have hn' : n - Nat.succ i < Nat.succ n := Nat.le_step hn
State after:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
⊢ (if h : n - Nat.succ i < Nat.succ n then
      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 - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
    else o) =
    push
      (if h : n - Nat.succ i < n then
        Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i
          (n - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
      else o)
      (f { val := n, isLt := ⋯ })

State before:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
⊢ (if h : n - Nat.succ i < Nat.succ n then
      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 - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
    else o) =
    push
      (if h : n - Nat.succ i < n then
        Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i
          (n - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ }))
      else o)
      (f { val := n, isLt := ⋯ })
Tactic:
simp [hn, hn']
State after:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
⊢ 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 - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i
        (n - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
      (f { val := n, isLt := ⋯ })

State before:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
⊢ 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 - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i
        (n - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
      (f { val := n, isLt := ⋯ })
Tactic:
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)]
State after:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = 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 - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i
        (n - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
      (f { val := n, isLt := ⋯ })

State before:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = 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 - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i
        (n - Nat.succ i + 1) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
      (f { val := n, isLt := ⋯ })
Tactic:
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
State after:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
⊢ ∀ (j : Nat),
    j = n - Nat.succ i + 1 →
      Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
          (Nat.succ i) j ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
        push
          (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i j ⋯
            (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
          (f { val := n, isLt := ⋯ })

State before:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
⊢ ∀ (j : Nat),
    j = n - Nat.succ i + 1 →
      Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
          (Nat.succ i) j ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
        push
          (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i j ⋯
            (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
          (f { val := n, isLt := ⋯ })
Tactic:
intro j hj
State after:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
j : Nat
hj : j = n - Nat.succ i + 1
⊢ Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
      (Nat.succ i) j ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i j ⋯
        (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
      (f { val := n, isLt := ⋯ })

State before:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
j : Nat
hj : j = n - Nat.succ i + 1
⊢ Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
      (Nat.succ i) j ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i j ⋯
        (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
      (f { val := n, isLt := ⋯ })
Tactic:
rw [this] at hj
State after:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
j : Nat
hj : j = 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) j ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i j ⋯
        (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
      (f { val := n, isLt := ⋯ })

State before:
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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
j : Nat
hj : j = 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) j ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i j ⋯
        (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
      (f { val := n, isLt := ⋯ })
Tactic:
cases hj
State after:
case succ.refl
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = 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) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i (n - i) ⋯
        (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
      (f { val := n, isLt := ⋯ })

State before:
case succ.refl
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = 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) ⋯ (push o (f { val := n - Nat.succ i, isLt := ⋯ })) =
    push
      (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i (n - i) ⋯
        (push o (f { val := n - Nat.succ i, isLt := ⋯ })))
      (f { val := n, isLt := ⋯ })
Tactic:
apply ih
State after:
case succ.refl.hi
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
⊢ i ≤ n

case succ.refl.ho
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
⊢ size (push o (f { val := n - Nat.succ i, isLt := ⋯ })) = n - i

State before:
case succ.refl.hi
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
⊢ i ≤ n

case succ.refl.ho
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
⊢ size (push o (f { val := n - Nat.succ i, isLt := ⋯ })) = n - i
Tactic:
exact Nat.le_of_lt hi
State after:
case succ.refl.ho
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
⊢ size (push o (f { val := n - Nat.succ i, isLt := ⋯ })) = n - i

State before:
case succ.refl.ho
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
this : n - Nat.succ i + 1 = n - i
⊢ size (push o (f { val := n - Nat.succ i, isLt := ⋯ })) = n - i
Tactic:
simp [ho, this]
State after:
no goals

State before:
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
⊢ n - Nat.succ i + 1 = n - i
Tactic:
simp [Nat.sub_succ]
State after:
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
⊢ Nat.pred (n - i) + 1 = n - i

State before:
α : 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
hn : n - Nat.succ i < n
hn' : n - Nat.succ i < Nat.succ n
⊢ Nat.pred (n - i) + 1 = n - i
Tactic:
rw [Nat.add_one, Nat.succ_pred_eq_of_pos (Nat.zero_lt_sub_of_lt hi)]
State after:
no goals