no goals
α : Type ?u.15121
a : Array α
i : Fin (size a)
j : Nat
v : α
hj : j < size a
h : i.val ≠ j
⊢ j < size (set a i v)
simp [*]
no goals
α : Type u_1
a : Array α
i : Fin (size a)
j : Nat
v : α
hj : j < size a
h : i.val ≠ j
⊢ (set a i v)[j] = a[j]
simp only [set, getElem_eq_data_get, List.get_set_ne h]