no goals
α : Type u_1
β : Type u_2
γ : Type ?u.40463
δ : Type ?u.40466
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x : α
y : β
⊢ IsImage e s t ↔ e.target ∩ ↑(LocalHomeomorph.symm e) ⁻¹' (e.source ∩ s) = e.target ∩ t
rw [iff_symm_preimage_eq, ← image_source_inter_eq, ← image_source_inter_eq']