[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
⊢ IsLocallyHomeomorphOn f s
[PROOFSTEP]
intro x hx
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ f = ↑e
[PROOFSTEP]
obtain ⟨e, hx, he⟩ := h x hx
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx✝ : x ∈ s
e : LocalHomeomorph X Y
hx : x ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
⊢ ∃ e, x ∈ e.source ∧ f = ↑e
[PROOFSTEP]
exact
  ⟨{ e with
      toFun := f
      map_source' := fun x hx => by rw [he x hx]; exact e.map_source' hx
      left_inv' := fun x hx => by rw [he x hx]; exact e.left_inv' hx
      right_inv' := fun y hy => by rw [he _ (e.map_target' hy)]; exact e.right_inv' hy
      continuous_toFun := (continuousOn_congr he).mpr e.continuous_toFun },
    hx, rfl⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x✝ : X
hx✝¹ : x✝ ∈ s
e : LocalHomeomorph X Y
hx✝ : x✝ ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx : x ∈ e.source
⊢ f x ∈ e.target
[PROOFSTEP]
rw [he x hx]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x✝ : X
hx✝¹ : x✝ ∈ s
e : LocalHomeomorph X Y
hx✝ : x✝ ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx : x ∈ e.source
⊢ ↑e x ∈ e.target
[PROOFSTEP]
exact e.map_source' hx
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x✝ : X
hx✝¹ : x✝ ∈ s
e : LocalHomeomorph X Y
hx✝ : x✝ ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx : x ∈ e.source
⊢ LocalEquiv.invFun e.toLocalEquiv (f x) = x
[PROOFSTEP]
rw [he x hx]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x✝ : X
hx✝¹ : x✝ ∈ s
e : LocalHomeomorph X Y
hx✝ : x✝ ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx : x ∈ e.source
⊢ LocalEquiv.invFun e.toLocalEquiv (↑e x) = x
[PROOFSTEP]
exact e.left_inv' hx
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx✝ : x ∈ s
e : LocalHomeomorph X Y
hx : x ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
y : Y
hy : y ∈ e.target
⊢ f (LocalEquiv.invFun e.toLocalEquiv y) = y
[PROOFSTEP]
rw [he _ (e.map_target' hy)]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx✝ : x ∈ s
e : LocalHomeomorph X Y
hx : x ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
y : Y
hy : y ∈ e.target
⊢ ↑e (LocalEquiv.invFun e.toLocalEquiv y) = y
[PROOFSTEP]
exact e.right_inv' hy
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
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
[PROOFSTEP]
intro x hx
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
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
[PROOFSTEP]
obtain ⟨eg, hxg, rfl⟩ := hg (f x) (h hx)
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
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
[PROOFSTEP]
obtain ⟨ef, hxf, rfl⟩ := hf x hx
[GOAL]
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
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
[PROOFSTEP]
exact ⟨ef.trans eg, ⟨hxf, hxg⟩, rfl⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
⊢ IsLocallyHomeomorph f ↔ IsLocallyHomeomorphOn f Set.univ
[PROOFSTEP]
simp only [IsLocallyHomeomorph, IsLocallyHomeomorphOn, Set.mem_univ, forall_true_left]
