apply PartialEquiv.IsImage.of_image_eq
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ e.IsImage s (↑e '' s)
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e '' s