no goals
α : Type u_3
β : Type u_4
γ : Type u_1
δ : Type u_2
e : LocalEquiv α β
e' : LocalEquiv β γ
e'' : LocalEquiv γ δ
⊢ (LocalEquiv.trans (LocalEquiv.trans e e') e'').source = (LocalEquiv.trans e (LocalEquiv.trans e' e'')).source
simp [trans_source, @preimage_comp α β γ, inter_assoc]