internlm/Lean-Github huggingface dataset:
Theorem: Array.init_succ
Proof 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
Proof 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 := ⋯ })
Theorem: Array.init_succ
Proof 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
Proof 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 := ⋯ })
Theorem: Array.init_succ
Proof 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']
Proof 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 := ⋯ })
Theorem: Array.init_succ
Proof 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)]
Proof 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 := ⋯ })
Theorem: Array.init_succ
Proof 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
Proof 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 := ⋯ })
Theorem: Array.init_succ
Proof 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
Proof 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 := ⋯ })
Theorem: Array.init_succ
Proof 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
Proof 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 := ⋯ })
Theorem: Array.init_succ
Proof 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
Proof 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 := ⋯ })
Theorem: Array.init_succ
Proof 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
Proof 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
Theorem: Array.init_succ
Proof 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
Proof 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
Theorem: Array.init_succ
Proof 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]
Proof state after:
no goals