rcases x with ⟨x,hx⟩
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
⊢ f.toFun ↑((mapEquiv s f).symm x) = ↑x
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α'
hx : x ∈ map f s
⊢ f.toFun ↑((mapEquiv s f).symm { val := x, property := hx }) = ↑{ val := x, property := hx }