H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ P (↑(chartAt H' (g' x)) ∘ g' ∘ ↑(LocalHomeomorph.symm (chartAt H x))) (↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s)
    (↑(chartAt H x) x)
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ LiftPropWithinAt P g' s x
refine' ⟨h.1.congr_of_eventuallyEq h₁ hx, _⟩
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ↑(chartAt H' (g' x)) ∘
      g' ∘ ↑(LocalHomeomorph.symm (chartAt H x)) =ᶠ[𝓝[↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s] ↑(chartAt H x) x]
    ↑(chartAt H' (g x)) ∘ g ∘ ↑(LocalHomeomorph.symm (chartAt H x))
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ P (↑(chartAt H' (g' x)) ∘ g' ∘ ↑(LocalHomeomorph.symm (chartAt H x))) (↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s)
    (↑(chartAt H x) x)
refine' hG.congr_nhdsWithin' _
  (by simp_rw [Function.comp_apply, (chartAt H x).left_inv (mem_chart_source H x), hx]) h.2
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ∀ᶠ (x_1 : H) in 𝓝[↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s] ↑(chartAt H x) x,
    ↑(chartAt H' (g' x)) (g' (↑(LocalHomeomorph.symm (chartAt H x)) x_1)) =
      ↑(chartAt H' (g x)) (g (↑(LocalHomeomorph.symm (chartAt H x)) x_1))
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ↑(chartAt H' (g' x)) ∘
      g' ∘ ↑(LocalHomeomorph.symm (chartAt H x)) =ᶠ[𝓝[↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s] ↑(chartAt H x) x]
    ↑(chartAt H' (g x)) ∘ g ∘ ↑(LocalHomeomorph.symm (chartAt H x))
simp_rw [EventuallyEq, Function.comp_apply]
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ∀ᶠ (x_1 : M) in 𝓝[s] x, ↑(chartAt H' (g' x)) (g' x_1) = ↑(chartAt H' (g x)) (g x_1)
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ∀ᶠ (x_1 : H) in 𝓝[↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s] ↑(chartAt H x) x,
    ↑(chartAt H' (g' x)) (g' (↑(LocalHomeomorph.symm (chartAt H x)) x_1)) =
      ↑(chartAt H' (g x)) (g (↑(LocalHomeomorph.symm (chartAt H x)) x_1))
rw [(chartAt H x).eventually_nhdsWithin'
  (fun y ↦ chartAt H' (g' x) (g' y) = chartAt H' (g x) (g y)) (mem_chart_source H x)]
no goals
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ∀ᶠ (x_1 : M) in 𝓝[s] x, ↑(chartAt H' (g' x)) (g' x_1) = ↑(chartAt H' (g x)) (g x_1)
exact h₁.mono fun y hy ↦ by rw [hx, hy]
no goals
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ (↑(chartAt H' (g' x)) ∘ g' ∘ ↑(LocalHomeomorph.symm (chartAt H x))) (↑(chartAt H x) x) =
    (↑(chartAt H' (g x)) ∘ g ∘ ↑(LocalHomeomorph.symm (chartAt H x))) (↑(chartAt H x) x)
simp_rw [Function.comp_apply, (chartAt H x).left_inv (mem_chart_source H x), hx]
no goals
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.41226
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
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
y : M
hy : g' y = g y
⊢ ↑(chartAt H' (g' x)) (g' y) = ↑(chartAt H' (g x)) (g y)
rw [hx, hy]