X : Type u_3
Y : Type u_1
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocallyHomeomorphOn g t
hf : IsLocallyHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ g ∘ f = ↑e
X : Type u_3
Y : Type u_1
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocallyHomeomorphOn g t
hf : IsLocallyHomeomorphOn f s
h : Set.MapsTo f s t
⊢ IsLocallyHomeomorphOn (g ∘ f) s
intro x hx
case intro.intro
X : Type u_3
Y : Type u_1
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
t : Set Y
hf : IsLocallyHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
eg : LocalHomeomorph Y Z
hxg : f x ∈ eg.source
hg : IsLocallyHomeomorphOn (↑eg) t
⊢ ∃ e, x ∈ e.source ∧ ↑eg ∘ f = ↑e
X : Type u_3
Y : Type u_1
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocallyHomeomorphOn g t
hf : IsLocallyHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ g ∘ f = ↑e
obtain ⟨eg, hxg, rfl⟩ := hg (f x) (h hx)
case intro.intro.intro.intro
X : Type u_3
Y : Type u_1
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
s : Set X
t : Set Y
x : X
hx : x ∈ s
eg : LocalHomeomorph Y Z
hg : IsLocallyHomeomorphOn (↑eg) t
ef : LocalHomeomorph X Y
hxf : x ∈ ef.source
hf : IsLocallyHomeomorphOn (↑ef) s
h : Set.MapsTo (↑ef) s t
hxg : ↑ef x ∈ eg.source
⊢ ∃ e, x ∈ e.source ∧ ↑eg ∘ ↑ef = ↑e
case intro.intro
X : Type u_3
Y : Type u_1
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
t : Set Y
hf : IsLocallyHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
eg : LocalHomeomorph Y Z
hxg : f x ∈ eg.source
hg : IsLocallyHomeomorphOn (↑eg) t
⊢ ∃ e, x ∈ e.source ∧ ↑eg ∘ f = ↑e
obtain ⟨ef, hxf, rfl⟩ := hf x hx
no goals
case intro.intro.intro.intro
X : Type u_3
Y : Type u_1
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
s : Set X
t : Set Y
x : X
hx : x ∈ s
eg : LocalHomeomorph Y Z
hg : IsLocallyHomeomorphOn (↑eg) t
ef : LocalHomeomorph X Y
hxf : x ∈ ef.source
hf : IsLocallyHomeomorphOn (↑ef) s
h : Set.MapsTo (↑ef) s t
hxg : ↑ef x ∈ eg.source
⊢ ∃ e, x ∈ e.source ∧ ↑eg ∘ ↑ef = ↑e
exact ⟨ef.trans eg, ⟨hxf, hxg⟩, rfl⟩