cases as with | mk l =>
simp only [getElem_eq_data_get]
dsimp [push, size] at h ⊢
rw [List.get_of_eq (l.concat_eq_append a)]
if hil : i < l.length
then rw [dif_pos hil]; apply List.get_append_left
else
  rw [dif_neg hil]
  have : i = l.length := by
    refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
    rw [l.length_concat a] at h
    exact Nat.le_of_succ_le_succ h
  simp only [this]
  exact l.get_concat_length a _
α : Type u
a : α
as : Array α
i : Nat
h : i < size (push as a)
⊢ (push as a)[i] = if h : i < size as then as[i] else a
no goals