no goals
α : Type u_1
a : Array α
i j : Fin (size a)
k : Nat
⊢ (swap a i j)[k]? = if j.val = k then some a[i.val] else if i.val = k then some a[j.val] else a[k]?
simp [swap_def, get?_set, ← getElem_fin_eq_data_get]