intro h
α✝ : Type ?u.2597
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
⊢ Finite.any p = true → ∃ x, p x = true
α✝ : Type ?u.2597
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = true
⊢ ∃ x, p x = true