α : Type u_1
β : Type ?u.73860
γ : Type ?u.73863
δ : Type ?u.73866
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
⊢ LocalHomeomorph.restr (ofSet s hs) (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))
α : Type u_1
β : Type ?u.73860
γ : Type ?u.73863
δ : Type ?u.73866
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
⊢ LocalHomeomorph.trans (ofSet s hs) (ofSet s' hs') = ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))
rw [(ofSet s hs).trans_ofSet hs']
no goals
α : Type u_1
β : Type ?u.73860
γ : Type ?u.73863
δ : Type ?u.73866
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
hs : IsOpen s
s' : Set α
hs' : IsOpen s'
⊢ LocalHomeomorph.restr (ofSet s hs) (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') (_ : IsOpen (s ∩ s'))
ext <;> simp [hs'.interior_eq]