no goals
α : Type u_2
β : Type u_1
γ : Type ?u.48193
δ : Type ?u.48196
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set β
⊢ (LocalEquiv.trans e (LocalEquiv.restr (LocalEquiv.refl β) s)).source = (LocalEquiv.restr e (↑e ⁻¹' s)).source
simp [trans_source]