tauto
α β : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
S : Finset α
x : α
f : α → β
b : α
a3_left : b ∈ S ∧ ¬b = x
a1 : ¬f b = f x
a2 : ∃ a, (a ∈ S ∧ ¬a = x) ∧ f a = f b
⊢ b ∈ S ∧ f b = f b
no goals