H : Type u_1
M : Type u_2
H' : Type ?u.58167
M' : Type ?u.58170
X : Type ?u.58173
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x✝ : M
Q : (H → H) → Set H → H → Prop
hG✝ : LocalInvariantProp G G' P
inst✝ : HasGroupoid M G
hG : LocalInvariantProp G G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : H
hx : x ∈ e.target
⊢ LiftPropWithinAt Q (↑(LocalHomeomorph.symm e)) e.target x
H : Type u_1
M : Type u_2
H' : Type ?u.58167
M' : Type ?u.58170
X : Type ?u.58173
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG✝ : LocalInvariantProp G G' P
inst✝ : HasGroupoid M G
hG : LocalInvariantProp G G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
⊢ LiftPropOn Q (↑(LocalHomeomorph.symm e)) e.target
intro x hx
H : Type u_1
M : Type u_2
H' : Type ?u.58167
M' : Type ?u.58170
X : Type ?u.58173
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x✝ : M
Q : (H → H) → Set H → H → Prop
hG✝ : LocalInvariantProp G G' P
inst✝ : HasGroupoid M G
hG : LocalInvariantProp G G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : H
hx : x ∈ e.target
⊢ e.target ∈ 𝓝 x
H : Type u_1
M : Type u_2
H' : Type ?u.58167
M' : Type ?u.58170
X : Type ?u.58173
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x✝ : M
Q : (H → H) → Set H → H → Prop
hG✝ : LocalInvariantProp G G' P
inst✝ : HasGroupoid M G
hG : LocalInvariantProp G G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : H
hx : x ∈ e.target
⊢ LiftPropWithinAt Q (↑(LocalHomeomorph.symm e)) e.target x
apply hG.liftPropWithinAt_of_liftPropAt_of_mem_nhds
  (hG.liftPropAt_symm_of_mem_maximalAtlas hQ he hx)
no goals
H : Type u_1
M : Type u_2
H' : Type ?u.58167
M' : Type ?u.58170
X : Type ?u.58173
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x✝ : M
Q : (H → H) → Set H → H → Prop
hG✝ : LocalInvariantProp G G' P
inst✝ : HasGroupoid M G
hG : LocalInvariantProp G G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
x : H
hx : x ∈ e.target
⊢ e.target ∈ 𝓝 x
exact IsOpen.mem_nhds e.open_target hx