rw [← e.symm_image_target_eq_source]
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
hs : s ⊆ e.target
⊢ ↑e.symm '' s ⊆ e.source
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
hs : s ⊆ e.target
⊢ ↑e.symm '' s ⊆ ↑e.symm '' e.target