no goals
α : Type u_1
β : Type u_2
γ : Type ?u.31535
δ : Type ?u.31538
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
e' : LocalEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ↑e '' (e.source ∩ e'.source) = e.target ∩ e'.target
rw [hs.inter_eq, ht.inter_eq, image_empty]