awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
e_s : s ∩ {x : M | (fun (x : M) ↦ s x = t x) x} = t ∩ {x : M | (fun (x : M) ↦ s x = t x) x}
⊢ LiftPropWithinAt P g (s ∩ {x : M | (fun (x : M) ↦ s x = t x) x}) x =
    LiftPropWithinAt P g (t ∩ {x : M | (fun (x : M) ↦ s x = t x) x}) x

Tactic:
congr 1
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ s ∩ {x : M | (fun (x : M) ↦ s x = t x) x} = t ∩ {x : M | (fun (x : M) ↦ s x = t x) x}

Tactic:
aesop
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
hs : s ∈ 𝓝 x
rwa : ∀ (h : LiftPropWithinAt P g (univ ∩ s) x) (hs : s ∈ 𝓝 x), LiftPropAt P g x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : LiftPropWithinAt P g univ x) (hs : s ∈ 𝓝 x), LiftPropAt P g x
⊢ LiftPropAt P g x

Tactic:
rwa [← univ_inter s, hG.liftPropWithinAt_inter hs] at h

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter, Set.univ_inter
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropAt P g x
hs : s ∈ 𝓝 x
rwa : LiftPropWithinAt P g (univ ∩ s) x
rwa₁ rwa₂ rwa₃ rwa₄ : LiftPropWithinAt P g univ x
⊢ LiftPropWithinAt P g s x

Tactic:
rwa [← univ_inter s, hG.liftPropWithinAt_inter hs]

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter, Set.univ_inter
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
x : M
hx : x ∈ s
rcases : ∀ (u : Set M) (u_open : IsOpen[inst_1] u) (xu : x ∈ u) (hu : LiftPropOn P g (s ∩ u)), LiftPropWithinAt P g s x
⊢ LiftPropWithinAt P g s x

Tactic:
rcases h x hx with ⟨u, u_open, xu, hu⟩
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
x : M
hx : x ∈ s
u : Set M
u_open : IsOpen[inst_1] u
xu : x ∈ u
hu : LiftPropOn P g (s ∩ u)
⊢ LiftPropWithinAt P g (s ∩ u) x

Tactic:
have := hu x ⟨hx, xu⟩
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
x : M
hx : x ∈ s
u : Set M
u_open : IsOpen[inst_1] u
xu : x ∈ u
hu : LiftPropOn P g (s ∩ u)
this : LiftPropWithinAt P g (s ∩ u) x
rwa : u ∈ 𝓝 x
⊢ LiftPropWithinAt P g s x

Tactic:
rwa [hG.liftPropWithinAt_inter] at this

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_inter
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
x : M
hx : x ∈ s
u : Set M
u_open : IsOpen[inst_1] u
xu : x ∈ u
hu : LiftPropOn P g (s ∩ u)
this : LiftPropWithinAt P g (s ∩ u) x
⊢ u ∈ 𝓝 x

Tactic:
u_open.mem_nhds xu

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
x : M
hx : x ∈ s
u : Set M
u_open : IsOpen[inst_1] u
xu : x ∈ u
hu : LiftPropOn P g (s ∩ u)
this : LiftPropWithinAt P g (s ∩ u) x
⊢ u ∈ 𝓝 x

Tactic:
exact u_open.mem_nhds xu

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g u
rw : LiftPropOn P g univ
⊢ LiftProp P g

Tactic:
rw [← liftPropOn_univ]

Premises used: StructureGroupoid.liftPropOn_univ
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g u
⊢ LiftPropOn P g univ

Tactic:
hG.liftPropOn_of_locally_liftPropOn fun x _ ↦ ?_

Premises used: StructureGroupoid.LocalInvariantProp.liftPropOn_of_locally_liftPropOn
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g u
refine :
  ∀ (x : M), Membership.mem (γ := Set M) univ x → ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (univ ∩ u)
⊢ LiftPropOn P g univ

Tactic:
refine hG.liftPropOn_of_locally_liftPropOn fun x _ ↦ ?_

Premises used: StructureGroupoid.LocalInvariantProp.liftPropOn_of_locally_liftPropOn
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g u
x : M
h_1 : Membership.mem (γ := Set M) univ x
⊢ ∃ (u : Set M), IsOpen[inst_1] u ∧ x ∈ u ∧ LiftPropOn P g (univ ∩ u)

Tactic:
simp [h x]
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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:
⟨h.1.congr_of_eventuallyEq h₁ hx, ?_⟩

Premises used: ChartedSpace.LiftPropWithinAt.continuousWithinAt, ContinuousWithinAt.congr_of_eventuallyEq, ChartedSpace.LiftPropWithinAt.mk
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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
refine :
  P ((↑(chartAt H' (g' x)) : M' → H') ∘ g' ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
⊢ LiftPropWithinAt P g' s x

Tactic:
refine ⟨h.1.congr_of_eventuallyEq h₁ hx, ?_⟩
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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
simp_rw :
  (↑(chartAt H' (g' x)) : M' → H')
      (g' ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) x))) =
    (↑(chartAt H' (g x)) : M' → H')
      (g ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) x)))
simp_rw₁ : (↑(chartAt H' (g' x)) : M' → H') (g' x) = (↑(chartAt H' (g x)) : M' → H') (g x)
⊢ ((↑(chartAt H' (g' x)) : M' → H') ∘ g' ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(chartAt H x) : M → H) x) =
    ((↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(chartAt H x) : M → H) x)

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

Premises used: mem_chart_source, chartAt, OpenPartialHomeomorph.left_inv, Function.comp_apply
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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
refine :
  (↑(chartAt H' (g' x)) : M' → H') ∘
      g' ∘
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) :
          H → M) =ᶠ[𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s] (↑(chartAt H x) : M → H) x]
    (↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)
⊢ P ((↑(chartAt H' (g' x)) : M' → H') ∘ g' ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) 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

Premises used: ChartedSpace.LiftPropWithinAt.prop, StructureGroupoid.LocalInvariantProp.congr_nhdsWithin'
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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
simp_rw :
  ∀ᶠ (x_1 : H) in 𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s] (↑(chartAt H x) : M → H) x,
    (↑(chartAt H' (g' x)) : M' → H') (g' ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) x_1)) =
      (↑(chartAt H' (g x)) : M' → H') (g ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) x_1))
⊢ (↑(chartAt H' (g' x)) : M' → H') ∘
      g' ∘
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) :
          H → M) =ᶠ[𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s] (↑(chartAt H x) : M → H) x]
    (↑(chartAt H' (g x)) : M' → H') ∘ g ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)

Tactic:
simp_rw [EventuallyEq, Function.comp_apply]

Premises used: Filter.EventuallyEq, Function.comp_apply
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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
rw : ∀ᶠ (x_1 : M) in 𝓝[s] x, (↑(chartAt H' (g' x)) : M' → H') (g' x_1) = (↑(chartAt H' (g x)) : M' → H') (g x_1)
⊢ ∀ᶠ (x_1 : H) in 𝓝[(↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s] (↑(chartAt H x) : M → H) x,
    (↑(chartAt H' (g' x)) : M' → H') (g' ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) x_1)) =
      (↑(chartAt H' (g x)) : M' → H') (g ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) 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)]

Premises used: mem_chart_source, chartAt, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.eventually_nhdsWithin', Eq
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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
rw : (↑(chartAt H' (g x)) : M' → H') (g' y) = (↑(chartAt H' (g x)) : M' → H') (g y)
rw₁ rw₂ : (↑(chartAt H' (g x)) : M' → H') (g y) = (↑(chartAt H' (g x)) : M' → H') (g y)
⊢ (↑(chartAt H' (g' x)) : M' → H') (g' y) = (↑(chartAt H' (g x)) : M' → H') (g y)

Tactic:
rw [hx, hy]
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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)) : M' → H') (g' x_1) = (↑(chartAt H' (g x)) : M' → H') (g x_1)

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

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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
h₂ : x ∈ s
⊢ LiftPropWithinAt P g' s x

Tactic:
liftPropWithinAt_congr_of_eventuallyEq hG h h₁ (mem_of_mem_nhdsWithin h₂ h₁ :)

Premises used: mem_of_mem_nhdsWithin, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ LiftPropWithinAt P g' s x ↔ LiftPropWithinAt P g s x

Tactic:
⟨fun h ↦ hG.liftPropWithinAt_congr_of_eventuallyEq h h₁.symm hx.symm,
    fun h ↦ hG.liftPropWithinAt_congr_of_eventuallyEq h h₁ hx⟩

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq, Iff.intro, Eq.symm, Filter.EventuallyEq.symm
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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₁ : ∀ y ∈ s, g' y = g y
hx : g' x = g x
⊢ LiftPropWithinAt P g' s x ↔ LiftPropWithinAt P g s x

Tactic:
hG.liftPropWithinAt_congr_iff_of_eventuallyEq (eventually_nhdsWithin_of_forall h₁) hx

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq, eventually_nhdsWithin_of_forall
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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₁ : ∀ y ∈ s, g' y = g y
hx : x ∈ s
⊢ LiftPropWithinAt P g' s x ↔ LiftPropWithinAt P g s x

Tactic:
hG.liftPropWithinAt_congr_iff_of_eventuallyEq (eventually_nhdsWithin_of_forall h₁) (h₁ _ hx)

Premises used: StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_eventuallyEq, eventually_nhdsWithin_of_forall
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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₁ : ∀ y ∈ s, g' y = g y
hx : g' x = g x
⊢ LiftPropWithinAt P g' s x

Tactic:
(hG.liftPropWithinAt_congr_iff h₁ hx).mpr h

Premises used: Iff.mpr, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : 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₁ : ∀ y ∈ s, g' y = g y
hx : x ∈ s
⊢ LiftPropWithinAt P g' s x

Tactic:
(hG.liftPropWithinAt_congr_iff h₁ (h₁ _ hx)).mpr h

Premises used: Iff.mpr, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
x : M
hG : G.LocalInvariantProp G' P
h₁ simp_rw : g' =ᶠ[𝓝 x] g
⊢ g' =ᶠ[𝓝[univ] x] g

Tactic:
simp_rw [nhdsWithin_univ, h₁]

Premises used: nhdsWithin_univ
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropAt P g x
h₁ : g' =ᶠ[𝓝 x] g
⊢ LiftPropAt P g' x

Tactic:
(hG.liftPropAt_congr_iff_of_eventuallyEq h₁).mpr h

Premises used: Iff.mpr, StructureGroupoid.LocalInvariantProp.liftPropAt_congr_iff_of_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : LiftPropOn P g s
h₁ : ∀ y ∈ s, g' y = g y
⊢ LiftPropOn P g' s

Tactic:
fun x hx ↦ hG.liftPropWithinAt_congr (h x hx) h₁ (h₁ x hx)

Premises used: ChartedSpace.LiftPropOn, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h₁ : ∀ y ∈ s, g' y = g y
⊢ LiftPropOn P g' s ↔ LiftPropOn P g s

Tactic:
⟨fun h ↦ hG.liftPropOn_congr h fun y hy ↦ (h₁ y hy).symm, fun h ↦ hG.liftPropOn_congr h h₁⟩

Premises used: StructureGroupoid.LocalInvariantProp.liftPropOn_congr, Iff.intro, Eq.symm