rcases List.get_of_mem ha.val with ⟨i, hi⟩
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
ha : a ∈ as
⊢ ∃ i, as[i] = a
case intro
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
ha : a ∈ as
i : Fin as.data.length
hi : as.data.get i = a
⊢ ∃ i, as[i] = a