no goals
α : Type u_1
β : Type u_2
γ : Type ?u.30560
δ : Type ?u.30563
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
s : Set α
t : Set β
x : α
y : β
e' : LocalEquiv α β
h : IsImage e s t
h' : IsImage e' s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t
rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]