X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
intro x hx
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
obtain ⟨e, hx, he⟩ := h x hx
no goals
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
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⟩
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
rw [he x hx]
no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
exact e.map_source' hx
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
rw [he x hx]
no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
exact e.left_inv' hx
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
rw [he _ (e.map_target' hy)]
no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.404
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
exact e.right_inv' hy