internlm/Lean-Github huggingface dataset:
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
transitivity (foldl push (as.push bs[start]) bs (start+1) stop)[as.size + i]
Proof state after:
case left
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[as.size + i] = (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + i]

case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + i] = bs[start + i]
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
Tactic:
rw [size_append_aux (start+1) stop (Nat.succ_le_of_lt hstart') hstop]
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.size + i < (as.push bs[start]).size + (stop - (start + 1))
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.size + i < (as.push bs[start]).size + (stop - (start + 1))
Tactic:
rw [size_push]
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.size + i < as.size + 1 + (stop - (start + 1))
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.size + i < as.size + 1 + (stop - (start + 1))
Tactic:
rw [Nat.add_assoc]
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.size + i < as.size + (1 + (stop - (start + 1)))
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ as.size + i < as.size + (1 + (stop - (start + 1)))
Tactic:
apply Nat.add_lt_add_left
Proof state after:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < 1 + (stop - (start + 1))
Theorem: Array.get_append_aux_hi
Proof state before:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < 1 + (stop - (start + 1))
Tactic:
rw [Nat.add_comm]
Proof state after:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < stop - (start + 1) + 1
Theorem: Array.get_append_aux_hi
Proof state before:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < stop - (start + 1) + 1
Tactic:
rw [Nat.sub_succ']
Proof state after:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < stop - start - 1 + 1
Theorem: Array.get_append_aux_hi
Proof state before:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < stop - start - 1 + 1
Tactic:
rw [Nat.sub_add_cancel]
Proof state after:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < stop - start

case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ 1 ≤ stop - start
Theorem: Array.get_append_aux_hi
Proof state before:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < stop - start

case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ 1 ≤ stop - start
Tactic:
exact hi
Proof state after:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ 1 ≤ stop - start
Theorem: Array.get_append_aux_hi
Proof state before:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ 1 ≤ stop - start
Tactic:
rw [Nat.le_sub_iff_add_le hstart]
Proof state after:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ 1 + start ≤ stop
Theorem: Array.get_append_aux_hi
Proof state before:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ 1 + start ≤ stop
Tactic:
rw [Nat.add_comm]
Proof state after:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start + 1 ≤ stop
Theorem: Array.get_append_aux_hi
Proof state before:
case h
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start + 1 ≤ stop
Tactic:
exact Nat.succ_le_of_lt hstart'
Proof state after:
no goals
Theorem: Array.get_append_aux_hi
Proof state before:
case left
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[as.size + i] = (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + i]
Tactic:
congr 1
Proof state after:
case left.e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ foldl push as bs start stop = foldl push (as.push bs[start]) bs (start + 1) stop
Theorem: Array.get_append_aux_hi
Proof state before:
case left.e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ foldl push as bs start stop = foldl push (as.push bs[start]) bs (start + 1) stop
Tactic:
rw [foldl_step]
Proof state after:
case left.e_xs.hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ start < stop

case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size
Theorem: Array.get_append_aux_hi
Proof state before:
case left.e_xs.hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ start < stop

case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size
Tactic:
exact hstart'
Proof state after:
case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size
Theorem: Array.get_append_aux_hi
Proof state before:
case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size
Tactic:
exact hstop
Proof state after:
no goals
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + 0] = bs[start + 0]
Tactic:
transitivity (as.push bs[start])[as.size]
Proof state after:
case left
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + 0] = (as.push bs[start])[as.size]

case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (as.push bs[start])[as.size] = bs[start + 0]
Theorem: Array.get_append_aux_hi
Proof state before:
case left
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + 0] = (as.push bs[start])[as.size]
Tactic:
have h : as.size < (as.push bs[start]).size := by simp; done
Proof state after:
case left
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
h : as.size < (as.push bs[start]).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + 0] = (as.push bs[start])[as.size]
Theorem: Array.get_append_aux_hi
Proof state before:
case left
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
h : as.size < (as.push bs[start]).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + 0] = (as.push bs[start])[as.size]
Tactic:
exact get_append_aux_lo (start+1) stop as.size (Nat.succ_le_of_lt hstart') hstop h _
Proof state after:
no goals
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ as.size < (as.push bs[start]).size
Tactic:
simp
Proof state after:
no goals
Theorem: Array.get_append_aux_hi
Proof state before:
case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (as.push bs[start])[as.size] = bs[start + 0]
Tactic:
rw [get_push_eq]
Proof state after:
case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ bs[start] = bs[start + 0]
Theorem: Array.get_append_aux_hi
Proof state before:
case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
hi : 0 < stop - start
ha : as.size + 0 < (foldl push as bs start stop).size
hb : start + 0 < bs.size
this : as.size + 0 < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ bs[start] = bs[start + 0]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + (i + 1)] = bs[start + (i + 1)]
Tactic:
have : (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start+1) stop).size := by
  rw [size_append_aux (start+1) stop (Nat.succ_le_of_lt hstart') hstop]
  rw [size_push]
  apply Nat.add_lt_add_left
  rw [Nat.sub_succ']
  rw [Nat.lt_sub_iff_add_lt]
  exact hi
Proof state after:
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝¹ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this✝ : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
this : (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + (i + 1)] = bs[start + (i + 1)]
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝¹ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this✝ : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
this : (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + (i + 1)] = bs[start + (i + 1)]
Tactic:
transitivity (foldl push (as.push bs[start]) bs (start+1) stop)[(as.push bs[start]).size + i]
Proof state after:
case left
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝¹ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this✝ : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
this : (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[as.size + (i + 1)] =
    (foldl push (as.push bs[start]) bs (start + 1) stop)[(as.push bs[start]).size + i]

case right
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝¹ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this✝ : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
this : (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[(as.push bs[start]).size + i] = bs[start + (i + 1)]
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
Tactic:
rw [size_append_aux (start+1) stop (Nat.succ_le_of_lt hstart') hstop]
Proof state after:
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (as.push bs[start]).size + i < (as.push bs[start]).size + (stop - (start + 1))
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (as.push bs[start]).size + i < (as.push bs[start]).size + (stop - (start + 1))
Tactic:
rw [size_push]
Proof state after:
α : Type u_1
as bs : Array α
start stop i✝ : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
i : Nat
hi : i + 1 < stop - start
ha : as.size + (i + 1) < (foldl push as bs start stop).size
hb : start + (i + 1) < bs.size
this : as.size + (i + 1) < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ as.size + 1 + i < as.size + 1 + (stop - (start + 1))