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

case a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑(⋯ ▸ j) = ↑j