α : Type u_1
a : Array α
x : α
⊢ List.get (a.data ++ [x])
      { val := size a, isLt := (_ : (fun xs i => i < size xs) { data := a.data ++ [x] } (size a)) } =
    x
α : Type u_1
a : Array α
x : α
⊢ (push a x)[size a] = x
simp only [push, getElem_eq_data_get, List.concat_eq_append]
no goals
α : Type u_1
a : Array α
x : α
⊢ List.get (a.data ++ [x])
      { val := size a, isLt := (_ : (fun xs i => i < size xs) { data := a.data ++ [x] } (size a)) } =
    x
rw [List.get_append_right] <;> simp [getElem_eq_data_get]