H : Type u_1
M : Type u_2
H' : Type ?u.64061
M' : Type ?u.64064
X : Type ?u.64067
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
hG : LocalInvariantProp G G Q
hQ : ∀ (y : H), Q id univ y
⊢ ∀ (x : M), Q (↑(chartAt H (id x)) ∘ id ∘ ↑(LocalHomeomorph.symm (chartAt H x))) univ (↑(chartAt H x) x)
H : Type u_1
M : Type u_2
H' : Type ?u.64061
M' : Type ?u.64064
X : Type ?u.64067
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
hG : LocalInvariantProp G G Q
hQ : ∀ (y : H), Q id univ y
⊢ LiftProp Q id
simp_rw [liftProp_iff, continuous_id, true_and_iff]
no goals
H : Type u_1
M : Type u_2
H' : Type ?u.64061
M' : Type ?u.64064
X : Type ?u.64067
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
hG : LocalInvariantProp G G Q
hQ : ∀ (y : H), Q id univ y
⊢ ∀ (x : M), Q (↑(chartAt H (id x)) ∘ id ∘ ↑(LocalHomeomorph.symm (chartAt H x))) univ (↑(chartAt H x) x)
exact fun x ↦ hG.congr' ((chartAt H x).eventually_right_inverse <| mem_chart_target H x) (hQ _)