no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.45647
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ (LocalEquiv.trans e e').source = ↑(LocalEquiv.symm e) '' (e.target ∩ e'.source)
rw [e.trans_source', e.symm_image_target_inter_eq]