rw [get_set]
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[↑i] = as[↑j]
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (if ↑(⋯ ▸ j) = ↑i then as.get i else (as.set i (as.get j))[↑i]) = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size