H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.25242
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
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ ContinuousWithinAt (g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x) ∧
      P (↑(chartAt H' (g x)) ∘ g ∘ ↑(LocalHomeomorph.symm (chartAt H x))) (↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s)
        (↑(chartAt H x) x) ↔
    ContinuousWithinAt (g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x) ∧
      P (↑(chartAt H' ((g ∘ ↑(LocalHomeomorph.symm e)) (↑e x))) ∘ g ∘ ↑(LocalHomeomorph.symm e))
        (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x)
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.25242
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
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ LiftPropWithinAt P g s x ↔ LiftPropWithinAt P (g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x)
rw [liftPropWithinAt_self_source, LiftPropWithinAt,
  e.symm.continuousWithinAt_iff_continuousWithinAt_comp_right xe, e.symm_symm]
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.25242
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
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ P (↑(chartAt H' (g x)) ∘ g ∘ ↑(LocalHomeomorph.symm (chartAt H x))) (↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s)
      (↑(chartAt H x) x) ↔
    P (↑(chartAt H' ((g ∘ ↑(LocalHomeomorph.symm e)) (↑e x))) ∘ g ∘ ↑(LocalHomeomorph.symm e))
      (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x)
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.25242
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
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ ContinuousWithinAt (g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x) ∧
      P (↑(chartAt H' (g x)) ∘ g ∘ ↑(LocalHomeomorph.symm (chartAt H x))) (↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s)
        (↑(chartAt H x) x) ↔
    ContinuousWithinAt (g ∘ ↑(LocalHomeomorph.symm e)) (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x) ∧
      P (↑(chartAt H' ((g ∘ ↑(LocalHomeomorph.symm e)) (↑e x))) ∘ g ∘ ↑(LocalHomeomorph.symm e))
        (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x)
refine' and_congr Iff.rfl _
no goals
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.25242
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
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ P (↑(chartAt H' (g x)) ∘ g ∘ ↑(LocalHomeomorph.symm (chartAt H x))) (↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s)
      (↑(chartAt H x) x) ↔
    P (↑(chartAt H' ((g ∘ ↑(LocalHomeomorph.symm e)) (↑e x))) ∘ g ∘ ↑(LocalHomeomorph.symm e))
      (↑(LocalHomeomorph.symm e) ⁻¹' s) (↑e x)
rw [Function.comp_apply, e.left_inv xe, ← Function.comp.assoc,
  hG.liftPropWithinAt_indep_chart_source_aux (chartAt _ (g x) ∘ g) (chart_mem_maximalAtlas G x)
    (mem_chart_source _ x) he xe, Function.comp.assoc]