rw [mem_def, Array.mem_def, List.mem_iff_get, not_exists] at hx
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ¬x ∈ as
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ∀ (x_1 : Fin (List.length as.content.data)), ¬List.get as.content.data x_1 = x
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x