match h : Finite.any fun x => decide (p x) with
| true =>
  apply decide_eq_true
  match exists_eq_true_of_any_eq_true h with
  | ⟨x, hx⟩ =>
    exists x
    exact of_decide_eq_true hx
| false =>
  apply decide_eq_false
  intro ⟨x, hx⟩
  absurd forall_eq_false_of_any_eq_false h x
  rw [decide_eq_true hx]
  trivial
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∃ x, p x) = Finite.any fun x => decide (p x)
no goals