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