dsimp only [swap]
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ (swap x i j).val = (set (set x i x[↑j]) j x[↑i]).val
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ Array.swap x.val (Fin.cast (_ : n = Array.size x.val) i) (Fin.cast (_ : n = Array.size x.val) j) =
    (set (set x i x[↑j]) j x[↑i]).val