exact ⟨a, ha, ha, rfl⟩
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ ∃ a_1 ∈ s, ∃ (i : a_1 ∈ s), f a_1 i = f a ha
no goals