simp [eq_singleton_iff_unique_mem]
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y y' : α
h1 : y' ∈ s
⊢ filter (fun x => f x = f y') s = {y} ↔ f y' = f y
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y y' : α
h1 : y' ∈ s
⊢ ((y ∈ s ∧ y = y') ∧ ∀ x ∈ s, x = y' → x = y) ↔ y' = y