rw [get_set_of_ne]
α : 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.set i (as.get j)).set (⋯ ▸ j) (as.get i))[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.set i (as.get j))[k] = as[k]

case a
α : 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
⊢ ↑(⋯ ▸ j) ≠ k