next heq =>
  have : j.val = i.val := by
    rw [←heq]
    apply Fin.val_eq_val_of_heq
    rw [size_set]
    elim_casts
    reflexivity
  simp [get_eq_getElem, this]
case isTrue
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ↑(⋯ ▸ j) = ↑i
⊢ as.get i = as[↑j]

case isFalse
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (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
case isFalse
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (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