simp only [getElem_eq_data_get]
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) ↔ ∃ i hi, x[i] = a
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) ↔ ∃ i hi, List.get x.data { val := i, isLt := hi } = a