no goals
α : Type u_1
β : Type u_2
γ : Type ?u.40108
δ : Type ?u.40111
e✝ : LocalEquiv α β
e' : LocalEquiv β γ
e : LocalEquiv α β
s : Set α
h : e.source ⊆ s
⊢ (LocalEquiv.restr e s).source = e.source
simp [inter_eq_self_of_subset_left h]