rw [List.set_comm _ _ _ h]
α : Type u
as : Array α
i j : Fin (size as)
h : ¬i.val = j.val
⊢ 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)
no goals