no goals
α : Type u_1
β : Type u_2
γ : Type ?u.47735
δ : Type ?u.47738
e : LocalEquiv α β
e' : LocalEquiv β γ
⊢ (LocalEquiv.trans (LocalEquiv.refl α) e).source = e.source
simp [trans_source, preimage_id]