no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.49198
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
⊢ (LocalEquiv.trans (LocalEquiv.restr e s) e').source = (LocalEquiv.restr (LocalEquiv.trans e e') s).source
simp [trans_source, inter_comm, inter_assoc]