no goals
α : Type ?u.44886
a : Array α
x : α
i : Nat
h : i < size a
⊢ i < size (push a x)
simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
no goals
α : Type u_1
a : Array α
x : α
i : Nat
h : i < size a
⊢ (push a x)[i] = a[i]
simp only [push, getElem_eq_data_get, List.concat_eq_append, List.get_append_left, h]