Theorem: Array.get_append_aux_hi (GMLInit/Data/Array/Basic.lean)

State before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : autoParam (as.size + i < (foldl push as bs start stop).size) _auto✝
hb : autoParam (start + i < bs.size) _auto✝
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
simp only [autoParam] at ha hb
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
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]

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
heq : start = stop
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
rw [heq, Nat.sub_self] at hi
State after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < 0
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
heq : start = stop
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]

State before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < 0
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
heq : start = stop
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
contradiction
State after:
no goals

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
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
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
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]

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
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
have : start < bs.size := Nat.lt_of_lt_of_le hstart' hstop
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
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]

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
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
have : as.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]
  rw [Nat.add_assoc]
  apply Nat.add_lt_add_left
  rw [Nat.add_comm]
  rw [Nat.sub_succ']
  rw [Nat.sub_add_cancel]
  exact hi
  rw [Nat.le_sub_iff_add_le hstart]
  rw [Nat.add_comm]
  exact Nat.succ_le_of_lt hstart'
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
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]

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]
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]

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]
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))

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]
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))

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]
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)))

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
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))

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]
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

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']
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

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]
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

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
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

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]
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

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]
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

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'
State after:
no goals

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
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

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]
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

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'
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

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
State after:
no goals

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]
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]

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
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]

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 _
State after:
no goals

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
State after:
no goals

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]
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]

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
State after:
no goals

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
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)]

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]
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)]

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]
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))

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]
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))

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
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)

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']
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

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]
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

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
State after:
no goals

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
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

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]
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

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]
State after:
no goals

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
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)]

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
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)]

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' _ _]
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

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
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

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]
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

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
State after:
no goals

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']
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

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]
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

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
State after:
no goals

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]
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

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
State after:
no goals