rw [inter_eq_self_of_subset_right h, eq_comm, inter_eq_right]
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e '' s
case h
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s ⊆ e.target