-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_indep_chart_target_aux {g : X → M'} {e : PartialHomeomorph X H} {x : X}
    {s : Set X} (xe : x ∈ e.source) (hf : f ∈ G'.maximalAtlas M') (xf : g x ∈ f.source)
    (hf' : f' ∈ G'.maximalAtlas M') (xf' : g x ∈ f'.source) (hgs : ContinuousWithinAt g s x) :
    P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x) ↔ P (f' ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x)

Proof state:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : PartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑e.symm (↑e x)) ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g (↑e.symm (↑e x)) ∈ f'.source
hgs : ContinuousWithinAt g s (↑e.symm (↑e x))
⊢ ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
exact hgs.comp (e.symm.continuousAt <| e.mapsTo xe).continuousWithinAt Subset.rfl

Result:
no goals

Proof state:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : PartialHomeomorph 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 ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
rw [← e.left_inv xe] at xf xf' hgs

Result:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : PartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑e.symm (↑e x)) ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g (↑e.symm (↑e x)) ∈ f'.source
hgs : ContinuousWithinAt g s (↑e.symm (↑e x))
⊢ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Proof state:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : PartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑e.symm (↑e x)) ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g (↑e.symm (↑e x)) ∈ f'.source
hgs : ContinuousWithinAt g s (↑e.symm (↑e x))
⊢ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
refine hG.liftPropWithinAt_indep_chart_target_aux2 (g ∘ e.symm) hf xf hf' xf' ?_

Result:
H : Type u_1
H' : Type u_3
M' : Type u_4
X : Type u_5
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : X → M'
e : PartialHomeomorph X H
x : X
s : Set X
xe : x ∈ e.source
hf : f ∈ maximalAtlas M' G'
xf : g (↑e.symm (↑e x)) ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g (↑e.symm (↑e x)) ∈ f'.source
hgs : ContinuousWithinAt g s (↑e.symm (↑e x))
⊢ ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)