-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_congr_of_eventuallyEq (h : LiftPropWithinAt P g s x) (h₁ : g' =ᶠ[𝓝[s] x] g)
    (hx : g' x = g x) : LiftPropWithinAt P g' s 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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ∀ᶠ (x_1 : H) in 𝓝[↑(chartAt H x).symm ⁻¹' s] ↑(chartAt H x) x,
    ↑(chartAt H' (g' x)) (g' (↑(chartAt H x).symm x_1)) = ↑(chartAt H' (g x)) (g (↑(chartAt H x).symm x_1))

Tactic:
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)]

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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp 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)

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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ P (↑(chartAt H' (g' x)) ∘ g' ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)

Tactic:
refine hG.congr_nhdsWithin' ?_
  (by simp_rw [Function.comp_apply, (chartAt H x).left_inv (mem_chart_source H x), hx]) h.2

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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ↑(chartAt H' (g' x)) ∘ g' ∘ ↑(chartAt H x).symm =ᶠ[𝓝[↑(chartAt H x).symm ⁻¹' s] ↑(chartAt H x) x]
    ↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm

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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp 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)

Tactic:
exact h₁.mono fun y hy ↦ by rw [hx, hy]

Result:
no goals

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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ (↑(chartAt H' (g' x)) ∘ g' ∘ ↑(chartAt H x).symm) (↑(chartAt H x) x) =
    (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x) x)

Tactic:
simp_rw [Function.comp_apply, (chartAt H x).left_inv (mem_chart_source H x), hx]

Result:
no goals

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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp 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)

Tactic:
rw [hx, hy]

Result:
no goals

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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ↑(chartAt H' (g' x)) ∘ g' ∘ ↑(chartAt H x).symm =ᶠ[𝓝[↑(chartAt H x).symm ⁻¹' s] ↑(chartAt H x) x]
    ↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm

Tactic:
simp_rw [EventuallyEq, Function.comp_apply]

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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ∀ᶠ (x_1 : H) in 𝓝[↑(chartAt H x).symm ⁻¹' s] ↑(chartAt H x) x,
    ↑(chartAt H' (g' x)) (g' (↑(chartAt H x).symm x_1)) = ↑(chartAt H' (g x)) (g (↑(chartAt H x).symm x_1))

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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ LiftPropWithinAt P g' s x

Tactic:
refine ⟨h.1.congr_of_eventuallyEq h₁ hx, ?_⟩

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
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ P (↑(chartAt H' (g' x)) ∘ g' ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)