H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.15284
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
f : M → M'
hf : ContinuousWithinAt f s x
⊢ ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s =ᶠ[𝓝 (↑(chartAt H x) x)]
    (chartAt H x).toLocalEquiv.target ∩
      ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).toLocalEquiv.source)
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.15284
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
f : M → M'
⊢ LiftPropWithinAt P f s x ↔
    ContinuousWithinAt f s x ∧
      P (↑(chartAt H' (f x)) ∘ f ∘ ↑(LocalHomeomorph.symm (chartAt H x)))
        ((chartAt H x).toLocalEquiv.target ∩
          ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).toLocalEquiv.source))
        (↑(chartAt H x) x)
refine' and_congr_right fun hf ↦ hG.congr_set _
no goals
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.15284
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
f : M → M'
hf : ContinuousWithinAt f s x
⊢ ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s =ᶠ[𝓝 (↑(chartAt H x) x)]
    (chartAt H x).toLocalEquiv.target ∩
      ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).toLocalEquiv.source)
exact LocalHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter hf (mem_chart_source H x)
  (chart_source_mem_nhds H' (f x))