have hjk : ((size_set as i (get as j)).symm ▸ j).val ≠ k := by
  intro h
  cases h
  apply hjk
  apply Fin.val_eq_val_of_heq
  rw [size_set]
  elim_casts
  reflexivity
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ (as.swap i j)[k] = as[k]
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ (as.swap i j)[k] = as[k]