if h : i.1 = j.1 then
  cases Fin.eq_of_val_eq h; rfl
else
  rw [List.set_comm _ _ _ h]
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)
no goals