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