rw [get_swap]
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.swap k ⟨as.size - 1, ⋯⟩)[i] = if i = ↑k then as[as.size - 1] else as[i]
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else if i = ↑⟨as.size - 1, ⋯⟩ then as[k] else as[i]) =
    if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size