α : Type u_1
β : Type u_2
γ : Type ?u.54413
δ : Type ?u.54416
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
⊢ (LocalHomeomorph.restr e (e.source ∩ s)).toLocalEquiv.source = (LocalHomeomorph.restr e s).toLocalEquiv.source
α : Type u_1
β : Type u_2
γ : Type ?u.54413
δ : Type ?u.54416
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
⊢ LocalHomeomorph.restr e (e.source ∩ s) = LocalHomeomorph.restr e s
refine' LocalHomeomorph.ext _ _ (fun x => rfl) (fun x => rfl) _
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.54413
δ : Type ?u.54416
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
⊢ (LocalHomeomorph.restr e (e.source ∩ s)).toLocalEquiv.source = (LocalHomeomorph.restr e s).toLocalEquiv.source
simp [e.open_source.interior_eq, ← inter_assoc]