simp only [Array.data_swap]
case h
α : Type u
as : Array α
i j : Fin (size as)
⊢ (swap as i j).data = (swap as j i).data
case h
α : Type u
as : Array α
i j : Fin (size as)
⊢ List.set (List.set as.data i.val (get as j)) j.val (get as i) =
    List.set (List.set as.data j.val (get as i)) i.val (get as j)