simp [hx]
α : Type u_1
β : Type u_2
inst✝³ : Nonempty α
inst✝² : Nonempty β
s : Set α
t : Set β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
⊢ ↑(PartialEquiv.ofSetEquiv e) x = ↑(e ⟨x, hx⟩)
no goals