. next pa_idx =>
  simp only [← i_eq_idx] at pa_idx
  exact False.elim $ pa_idx pai
case inr.isFalse
α : 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
idx : Fin a.size
acc : Array α
ih : motive (↑idx) acc
i : Nat
i_in_bounds : i < a.size
i_lt_idx_add_one : i < ↑idx + 1
pai : p a[i] = true
i_eq_idx : i = ↑idx
h✝ : ¬p a[↑idx] = true
⊢ a[i] ∈ acc.data
no goals