simp only [List.any_eq_true, List.mem_iff_get]
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (List.any as.data fun b => decide (a = b)) = true ↔ a ∈ as.data
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) ↔ ∃ n, List.get as.data n = a