have hj' : j < as.size := as.size_set i x ▸ hj
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
⊢ (as.set i x)[j] = as[j]
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
hj' : j < as.size
⊢ (as.set i x)[j] = as[j]