no goals
α : Type ?u.14725
a : Array α
i : Fin (size a)
v : α
⊢ i.val < size (set a i v)
simp [i.2]
no goals
α : Type u_1
a : Array α
i : Fin (size a)
v : α
⊢ (set a i v)[i.val] = v
simp only [set, getElem_eq_data_get, List.get_set_eq]