no goals
α : Type u_1
β : Type u_2
γ : Type ?u.32478
δ : Type ?u.32481
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s = e.target ∩ ↑(LocalEquiv.symm e) ⁻¹' s
rw [← e.image_source_inter_eq', inter_eq_self_of_subset_right h]