match exists_eq_true_of_any_eq_true h with
| ⟨x, hx⟩ =>
  exists x
  exact of_decide_eq_true hx
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = true
⊢ ∃ x, p x
no goals