Theorem: Finite.exists_eq_true_of_any_eq_true (GMLInit/Class/Finite.lean)

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

State before:
α✝ : Type ?u.2597
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = true
⊢ ∃ x, p x = true
Tactic:
match Fin.exists_eq_true_of_any_eq_true h with
| ⟨i, h⟩ => exists (Finite.get α i)
State after:
no goals

State before:
α✝ : Type ?u.2597
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h✝ : Finite.any p = true
i : Fin toArray.size
h : p (Finite.get α i) = true
⊢ ∃ x, p x = true
Tactic:
exists (Finite.get α i)
State after:
no goals