simp [mapEquiv]
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ (mapEquiv s f).symm { val := f x, property := h } = { val := x, property := ⋯ }
α' : 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}