no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.76640
e : α ≃ β
e' : β ≃ γ
⊢ (toLocalEquiv (e.trans e')).source = (LocalEquiv.trans (toLocalEquiv e) (toLocalEquiv e')).source
simp [LocalEquiv.trans_source, Equiv.toLocalEquiv]