rw [eq_singleton_iff_unique_mem]
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ filter (fun x_1 => f x_1 = f x) s = {x}
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ x ∈ filter (fun x_1 => f x_1 = f x) s ∧ ∀ x_1 ∈ filter (fun x_2 => f x_2 = f x) s, x_1 = x