exact Array.foldl_induction motive h_base h_inductive i i_in_bounds i_in_bounds pai
α : Type u_1
a : Array α
p : α → Bool
i : Nat
i_in_bounds : i < a.size
pai : p a[i] = true
motive : Nat → Array α → Prop :=
  fun idx acc => ∀ (i : Nat) (i_in_bounds : i < a.size), i < idx → p a[i] = true → a[i] ∈ acc.data
h_base : motive 0 #[]
f : Array α → α → Array α := fun acc x => if p x = true then acc.push x else acc
f_def : f = fun acc x => if p x = true then acc.push x else acc
h_inductive : ∀ (idx : Fin a.size) (acc : Array α), motive (↑idx) acc → motive (↑idx + 1) (f acc a[idx])
⊢ a[i] ∈ (Array.foldl (fun r a => if p a = true then r.push a else r) #[] a 0).data
no goals