-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_iff {f : M → M'} :
    LiftPropWithinAt P f s x ↔
      ContinuousWithinAt f s x ∧
        P (chartAt H' (f x) ∘ f ∘ (chartAt H x).symm)
          ((chartAt H x).target ∩ (chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source))
          (chartAt H x x)

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
⊢ LiftPropWithinAt P f s x ↔
    ContinuousWithinAt f s x ∧
      P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm)
        ((chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)) (↑(chartAt H x) x)

Tactic:
rw [liftPropWithinAt_iff']

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
⊢ ContinuousWithinAt f s x ∧
      P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔
    ContinuousWithinAt f s x ∧
      P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm)
        ((chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)) (↑(chartAt H x) x)

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
⊢ ContinuousWithinAt f s x ∧
      P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔
    ContinuousWithinAt f s x ∧
      P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm)
        ((chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)) (↑(chartAt H x) x)

Tactic:
refine and_congr_right fun hf ↦ hG.congr_set ?_

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
hf : ContinuousWithinAt f s x
⊢ ↑(chartAt H x).symm ⁻¹' s =ᶠ[𝓝 (↑(chartAt H x) x)]
    (chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
hf : ContinuousWithinAt f s x
⊢ ↑(chartAt H x).symm ⁻¹' s =ᶠ[𝓝 (↑(chartAt H x) x)]
    (chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)

Tactic:
exact PartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter hf
  (mem_chart_source H x) (chart_source_mem_nhds H' (f x))

Result:
no goals