have : j.val = i.val := by
  rw [←heq]
  apply Fin.val_eq_val_of_heq
  rw [size_set]
  elim_casts
  reflexivity
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ as.get i = as[↑j]
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
this : ↑j = ↑i
⊢ as.get i = as[↑j]