rw [getElem_eq_data_get]
α : 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
⊢ as.data ++ [bs[start]] ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop
α : 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
⊢ as.data ++ [bs.data.get ⟨start, ⋯⟩] ++ bs.data.extract (start + 1) stop =
    as.data ++ bs.data.get ⟨start, ⋯⟩ :: bs.data.extract (start + 1) stop