H : Type u_2
M : Type ?u.20880
H' : Type u_3
M' : Type u_4
X : Type u_1
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
g : X → M'
e : LocalHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑(LocalHomeomorph.symm e) (↑e x)) ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g (↑(LocalHomeomorph.symm e) (↑e x)) ∈ f'.source
hgs : ContinuousWithinAt g s (↑(LocalHomeomorph.symm e) (↑e x))
⊢ P (↑f ∘ g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x) ↔
    P (↑f' ∘ g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x)
H : Type u_2
M : Type ?u.20880
H' : Type u_3
M' : Type u_4
X : Type u_1
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
g : X → M'
e : LocalHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
⊢ P (↑f ∘ g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x) ↔
    P (↑f' ∘ g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x)
rw [← e.left_inv xe] at xf xf' hgs
H : Type u_2
M : Type ?u.20880
H' : Type u_3
M' : Type u_4
X : Type u_1
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
g : X → M'
e : LocalHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑(LocalHomeomorph.symm e) (↑e x)) ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g (↑(LocalHomeomorph.symm e) (↑e x)) ∈ f'.source
hgs : ContinuousWithinAt g s (↑(LocalHomeomorph.symm e) (↑e x))
⊢ ContinuousWithinAt (g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x)
H : Type u_2
M : Type ?u.20880
H' : Type u_3
M' : Type u_4
X : Type u_1
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
g : X → M'
e : LocalHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑(LocalHomeomorph.symm e) (↑e x)) ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g (↑(LocalHomeomorph.symm e) (↑e x)) ∈ f'.source
hgs : ContinuousWithinAt g s (↑(LocalHomeomorph.symm e) (↑e x))
⊢ P (↑f ∘ g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x) ↔
    P (↑f' ∘ g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x)
refine' hG.liftPropWithinAt_indep_chart_target_aux2 (g ∘ e.symm) hf xf hf' xf' _
no goals
H : Type u_2
M : Type ?u.20880
H' : Type u_3
M' : Type u_4
X : Type u_1
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
g : X → M'
e : LocalHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑(LocalHomeomorph.symm e) (↑e x)) ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g (↑(LocalHomeomorph.symm e) (↑e x)) ∈ f'.source
hgs : ContinuousWithinAt g s (↑(LocalHomeomorph.symm e) (↑e x))
⊢ ContinuousWithinAt (g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x)
exact hgs.comp (e.symm.continuousAt <| e.mapsTo xe).continuousWithinAt Subset.rfl