-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_indep_chart_source_aux (g : M → H') (he : e ∈ G.maximalAtlas M)
    (xe : x ∈ e.source) (he' : e' ∈ G.maximalAtlas M) (xe' : x ∈ e'.source) :
    P (g ∘ e.symm) (e.symm ⁻¹' s) (e x) ↔ P (g ∘ e'.symm) (e'.symm ⁻¹' s) (e' x)

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)

Tactic:
rw [← hG.right_invariance (compatible_of_mem_maximalAtlas he he')]

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ((g ∘ ↑e.symm) ∘ ↑(e.symm ≫ₕ e').symm) (↑(e.symm ≫ₕ e').symm ⁻¹' (↑e.symm ⁻¹' s)) (↑(e.symm ≫ₕ e') (↑e x)) ↔
    P (g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)

H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑e x ∈ (e.symm ≫ₕ e').source

Proof state:
case refine_2
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
y : H
hy : y ∈ ↑e'.symm ⁻¹' e.source
⊢ y ∈ ↑(e.symm ≫ₕ e').symm ⁻¹' (↑e.symm ⁻¹' s) ↔ y ∈ ↑e'.symm ⁻¹' s

Tactic:
simp_rw [mem_preimage, PartialHomeomorph.coe_trans_symm, PartialHomeomorph.symm_symm,
  Function.comp_apply, e.left_inv hy]

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑(e.symm ≫ₕ e').symm ⁻¹' (↑e.symm ⁻¹' s) =ᶠ[𝓝 (↑e' x)] ↑e'.symm ⁻¹' s

Tactic:
refine (eventually_of_mem ?_ fun y (hy : y ∈ e'.symm ⁻¹' e.source) ↦ ?_).set_eq

Result:
case refine_1
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑e'.symm ⁻¹' e.source ∈ 𝓝 (↑e' x)

case refine_2
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
y : H
hy : y ∈ ↑e'.symm ⁻¹' e.source
⊢ y ∈ ↑(e.symm ≫ₕ e').symm ⁻¹' (↑e.symm ⁻¹' s) ↔ y ∈ ↑e'.symm ⁻¹' s

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑e x ∈ (e.symm ≫ₕ e').source

Tactic:
simp only [xe, xe', mfld_simps]

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
y : H
hy : ↑e.symm (↑e (↑e'.symm y)) = ↑e'.symm y
⊢ ((g ∘ ↑e.symm) ∘ ↑(e.symm ≫ₕ e').symm) y = (g ∘ ↑e'.symm) y

Tactic:
simp only [mfld_simps]

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
y : H
hy : ↑e.symm (↑e (↑e'.symm y)) = ↑e'.symm y
⊢ g (↑e.symm (↑e (↑e'.symm y))) = g (↑e'.symm y)

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ((g ∘ ↑e.symm) ∘ ↑(e.symm ≫ₕ e').symm) (↑(e.symm ≫ₕ e').symm ⁻¹' (↑e.symm ⁻¹' s)) (↑(e.symm ≫ₕ e') (↑e x)) ↔
    P (g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)

H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑e x ∈ (e.symm ≫ₕ e').source

Tactic:
swap

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ ↑e x ∈ (e.symm ≫ₕ e').source

H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
⊢ P ((g ∘ ↑e.symm) ∘ ↑(e.symm ≫ₕ e').symm) (↑(e.symm ≫ₕ e').symm ⁻¹' (↑e.symm ⁻¹' s)) (↑(e.symm ≫ₕ e') (↑e x)) ↔
    P (g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)