simp only [Array.getElem_swap, castIndex, Nat.add_left_cancel_iff]
α : Type u
x : Subarray α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
⊢ (Array.swap x.as (castIndex x i) (castIndex x j))[x.start + k] =
    if ↑j = k then x.as[x.start + ↑i] else if ↑i = k then x.as[x.start + ↑j] else x.as[x.start + k]
no goals