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
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))
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
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
⊢ i < 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
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
⊢ i < stop - (start + 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
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
⊢ i < 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
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
⊢ i < stop - start - 1
Tactic:
rw [Nat.lt_sub_iff_add_lt]
Proof state after:
case h
α : 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
⊢ i + 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
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
⊢ i + 1 < stop - start
Tactic:
exact hi
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
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]
Tactic:
congr 1
Proof state after:
case left.e_i
α : 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
⊢ as.size + (i + 1) = (as.push bs[start]).size + i
Theorem: Array.get_append_aux_hi
Proof state before:
case left.e_i
α : 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
⊢ as.size + (i + 1) = (as.push bs[start]).size + i
Tactic:
rw [size_push]
Proof state after:
case left.e_i
α : 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
⊢ as.size + (i + 1) = as.size + 1 + i
Theorem: Array.get_append_aux_hi
Proof state before:
case left.e_i
α : 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
⊢ as.size + (i + 1) = as.size + 1 + i
Tactic:
rw [Nat.add_right_comm, Nat.add_assoc]
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
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)]
Tactic:
have hi' : i < stop - (start+1) := by
  rw [Nat.sub_succ']
  rw [Nat.lt_sub_iff_add_lt]
  exact hi
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
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
hi' : i < stop - (start + 1)
⊢ (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:
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
hi' : i < stop - (start + 1)
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[(as.push bs[start]).size + i] = bs[start + (i + 1)]
Tactic:
have : start + 1 + i < bs.size := by rw [Nat.add_assoc, Nat.add_comm 1]; exact hb
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
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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.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:
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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[(as.push bs[start]).size + i] = bs[start + (i + 1)]
Tactic:
rw [get_append_aux_hi (start+1) stop i (Nat.succ_le_of_lt hstart') hstop hi' _ _]
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
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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ bs[start + 1 + i] = bs[start + (i + 1)]

α : 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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ start + 1 + i < bs.size
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
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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ bs[start + 1 + i] = bs[start + (i + 1)]

α : 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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ start + 1 + i < bs.size
Tactic:
congr 1
Proof state after:
case right.e_i
α : 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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ start + 1 + i = start + (i + 1)

α : 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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ start + 1 + i < bs.size
Theorem: Array.get_append_aux_hi
Proof state before:
case right.e_i
α : 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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ start + 1 + i = start + (i + 1)

α : 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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ start + 1 + i < bs.size
Tactic:
rw [Nat.add_right_comm, Nat.add_assoc]
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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ start + 1 + i < bs.size
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
hi' : i < stop - (start + 1)
this : start + 1 + i < bs.size
⊢ start + 1 + i < bs.size
Tactic:
assumption
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
this : (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ i < stop - (start + 1)
Tactic:
rw [Nat.sub_succ']
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
⊢ i < 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
this : (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ i < stop - start - 1
Tactic:
rw [Nat.lt_sub_iff_add_lt]
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
⊢ i + 1 < stop - start
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
⊢ i + 1 < stop - start
Tactic:
exact hi
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
this : (as.push bs[start]).size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
hi' : i < stop - (start + 1)
⊢ start + 1 + i < bs.size
Tactic:
rw [Nat.add_assoc, Nat.add_comm 1]
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
hi' : i < stop - (start + 1)
⊢ start + (i + 1) < bs.size
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
hi' : i < stop - (start + 1)
⊢ start + (i + 1) < bs.size
Tactic:
exact hb
Proof state after:
no goals
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Tactic:
by_cases start = stop with
| isTrue heq =>
  cases heq
  rw [foldl_stop] <;> try assumption
  rw [List.extract_stop]
  rw [List.append_nil]
| isFalse hne =>
  have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
  have : start < bs.size := Nat.lt_of_lt_of_le hstart' hstop
  rw [foldl_step] <;> try assumption
  rw [List.extract_step]
  rw [data_append_aux (start+1) stop] <;> try assumption
  rw [push_data]
  rw [getElem_eq_data_get]
  rw [List.append_assoc]
  rw [List.singleton_append]
Proof state after:
no goals
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Tactic:
cases heq
Proof state after:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ (foldl push as bs start start).data = as.data ++ bs.data.extract start start
Theorem: Array.data_append_aux
Proof state before:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ (foldl push as bs start start).data = as.data ++ bs.data.extract start start
Tactic:
rw [foldl_stop] <;> try assumption
Proof state after:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ as.data = as.data ++ bs.data.extract start start
Theorem: Array.data_append_aux
Proof state before:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ as.data = as.data ++ bs.data.extract start start
Tactic:
rw [List.extract_stop]
Proof state after:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ as.data = as.data ++ []
Theorem: Array.data_append_aux
Proof state before:
case refl
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ as.data = as.data ++ []
Tactic:
rw [List.append_nil]
Proof state after:
no goals
Theorem: Array.data_append_aux
Proof state before:
case refl.hstop
α : Type u_1
as bs : Array α
start : Nat
hstart : start ≤ start
hstop : start ≤ bs.size
⊢ start ≤ bs.size
Tactic:
assumption
Proof state after:
no goals
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Tactic:
have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Theorem: Array.data_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop
Tactic:
have : start < bs.size := Nat.lt_of_lt_of_le hstart' hstop
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push as bs start stop).data = as.data ++ bs.data.extract start stop