case inl hi =>
  split at h
  case inl => simp_all
  case inr => exact go h
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
hi : idx < size as
h : (if p as[idx] = true then some as[idx] else findP?.loop (idx + 1) as p) = some a
⊢ p a = true
no goals