simp only [Array.filter]
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
⊢ a[i] ∈ (Array.filter p a 0).data
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data