intro h
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
⊢ ↑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
⊢ (as.set i x)[j] = as[j]