no goals
α : Type u_1
β : Type u_2
γ : Type ?u.31956
δ : Type ?u.31959
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑(LocalEquiv.symm e) ⁻¹' s
rw [inter_comm, e.leftInvOn.image_inter', image_source_eq_target, inter_comm]