no goals
α : Type u_1
β : Type u_2
γ : Type ?u.27993
δ : Type ?u.27996
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
t : Set β
x : α
y : β
⊢ IsImage e s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s
simp only [IsImage, ext_iff, mem_inter_iff, mem_preimage, and_congr_right_iff]