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
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
⊢ ContinuousWithinAt f s x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt f s x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
          (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
        ((↑(chartAt H x) : M → H) x)

Tactic:
and_congr_right fun hf ↦ hG.congr_set ?_

Premises used: and_congr_right, StructureGroupoid.LocalInvariantProp.congr_set
-- 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
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
refine :
  ∀ (hf : ContinuousWithinAt f s x),
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s =ᶠ[𝓝 ((↑(chartAt H x) : M → H) x)]
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source)
⊢ ContinuousWithinAt f s x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt f s x ∧
      P ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
          (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
        ((↑(chartAt H x) : M → H) x)

Tactic:
refine and_congr_right fun hf ↦ hG.congr_set ?_

Premises used: and_congr_right, StructureGroupoid.LocalInvariantProp.congr_set
-- 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
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
hf : ContinuousWithinAt f s x
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s =ᶠ[𝓝 ((↑(chartAt H x) : M → H) x)]
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
        (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source)

Tactic:
OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter hf
    (mem_chart_source H x) (chart_source_mem_nhds H' (f x))

Premises used: mem_chart_source, chart_source_mem_nhds, OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_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
s : Set M
x : M
hG : G.LocalInvariantProp G' P
f : M → M'
hf : ContinuousWithinAt f s x
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s =ᶠ[𝓝 ((↑(chartAt H x) : M → H) x)]
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
        (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source)

Tactic:
exact OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter hf
    (mem_chart_source H x) (chart_source_mem_nhds H' (f x))

Premises used: mem_chart_source, chart_source_mem_nhds, OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
rw :
  P ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H))
      ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s) ((↑(e.symm ≫ₕ e') : H → H) ((↑e : M → H) x)) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
rw₁ : (↑e : M → H) x ∈ (e.symm ≫ₕ e').source
⊢ P (g ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)

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

Premises used: StructureGroupoid.compatible_of_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.right_invariance
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
⊢ (↑e : M → H) x ∈ (e.symm ≫ₕ e').source

Tactic:
simp only [xe, xe', mfld_simps]
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
simp_rw :
  P ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H))
      ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
⊢ P ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H))
      ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s) ((↑(e.symm ≫ₕ e') : H → H) ((↑e : M → H) x)) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)

Tactic:
simp_rw [OpenPartialHomeomorph.trans_apply, e.left_inv xe]

Premises used: OpenPartialHomeomorph.trans_apply, OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
rw :
  P (g ∘ (↑e'.symm : H → M)) ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)
rw₁ : (g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H) =ᶠ[𝓝 ((↑e' : M → H) x)] g ∘ (↑e'.symm : H → M)
rw₂ : H → H'
⊢ P ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H))
      ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)

Tactic:
rw [hG.congr_iff]

Premises used: StructureGroupoid.LocalInvariantProp.congr_iff
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
⊢ P (g ∘ (↑e'.symm : H → M)) ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)

Tactic:
hG.congr_set ?_

Premises used: StructureGroupoid.LocalInvariantProp.congr_set
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
refine : (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s =ᶠ[𝓝 ((↑e' : M → H) x)] (↑e'.symm : H → M) ⁻¹' s
⊢ P (g ∘ (↑e'.symm : H → M)) ((↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s) ((↑e' : M → H) x) ↔
    P (g ∘ (↑e'.symm : H → M)) ((↑e'.symm : H → M) ⁻¹' s) ((↑e' : M → H) x)

Tactic:
refine hG.congr_set ?_

Premises used: StructureGroupoid.LocalInvariantProp.congr_set
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
⊢ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s =ᶠ[𝓝 ((↑e' : M → H) x)] (↑e'.symm : H → M) ⁻¹' s

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

Premises used: Filter.Eventually.set_eq, Filter.eventually_of_mem
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
refine_1 : (↑e'.symm : H → M) ⁻¹' e.source ∈ 𝓝 ((↑e' : M → H) x)
refine_2 :
  ∀ (y : H) (hy : y ∈ (↑e'.symm : H → M) ⁻¹' e.source),
    y ∈ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s ↔ y ∈ (↑e'.symm : H → M) ⁻¹' s
⊢ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s =ᶠ[𝓝 ((↑e' : M → H) x)] (↑e'.symm : H → M) ⁻¹' s

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

Premises used: Filter.Eventually.set_eq, Filter.eventually_of_mem
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
⊢ (↑e'.symm : H → M) ⁻¹' e.source ∈ 𝓝 ((↑e' : M → H) x)

Tactic:
(e'.symm.continuousAt <| e'.mapsTo xe').preimage_mem_nhds (e.open_source.mem_nhds ?_)

Premises used: OpenPartialHomeomorph.continuousAt, OpenPartialHomeomorph.open_source, ContinuousAt.preimage_mem_nhds, IsOpen.mem_nhds, OpenPartialHomeomorph.mapsTo, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
refine_1 : (↑e'.symm : H → M) ((↑e' : M → H) x) ∈ e.source
⊢ (↑e'.symm : H → M) ⁻¹' e.source ∈ 𝓝 ((↑e' : M → H) x)

Tactic:
refine (e'.symm.continuousAt <| e'.mapsTo xe').preimage_mem_nhds (e.open_source.mem_nhds ?_)

Premises used: OpenPartialHomeomorph.continuousAt, OpenPartialHomeomorph.open_source, ContinuousAt.preimage_mem_nhds, IsOpen.mem_nhds, OpenPartialHomeomorph.mapsTo, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
refine_1 : x ∈ e.source
⊢ (↑e'.symm : H → M) ((↑e' : M → H) x) ∈ e.source

Tactic:
simp_rw [e'.left_inv xe', xe]

Premises used: OpenPartialHomeomorph.left_inv
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
y : H
hy : y ∈ (↑e'.symm : H → M) ⁻¹' e.source
refine_2 : (↑e.symm : H → M) ((↑(e.symm ≫ₕ e').symm : H → H) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
refine_2₁ : (↑e.symm : H → M) (((↑e.symm.symm : M → H) ∘ (↑e'.symm : H → M)) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
refine_2₂ : (↑e.symm : H → M) (((↑e : M → H) ∘ (↑e'.symm : H → M)) y) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
refine_2₃ : (↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y)) ∈ s ↔ (↑e'.symm : H → M) y ∈ s
⊢ y ∈ (↑(e.symm ≫ₕ e').symm : H → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s ↔ y ∈ (↑e'.symm : H → M) ⁻¹' s

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

Premises used: OpenPartialHomeomorph.left_inv, Function.comp_apply, OpenPartialHomeomorph.symm_symm, OpenPartialHomeomorph.coe_trans_symm, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
⊢ (g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H) =ᶠ[𝓝 ((↑e' : M → H) x)] g ∘ (↑e'.symm : H → M)

Tactic:
((e'.eventually_nhds' _ xe').mpr <| e.eventually_left_inverse xe).mono fun y hy ↦ ?_

Premises used: Iff.mpr, OpenPartialHomeomorph.eventually_left_inverse, Filter.EventuallyEq, Filter.Eventually.mono, OpenPartialHomeomorph.eventually_nhds'
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
refine :
  ∀ (y : H) (hy : (↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y)) = (↑e'.symm : H → M) y),
    ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H)) y = (g ∘ (↑e'.symm : H → M)) y
⊢ (g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H) =ᶠ[𝓝 ((↑e' : M → H) x)] g ∘ (↑e'.symm : H → M)

Tactic:
refine ((e'.eventually_nhds' _ xe').mpr <| e.eventually_left_inverse xe).mono fun y hy ↦ ?_

Premises used: Iff.mpr, OpenPartialHomeomorph.eventually_left_inverse, Filter.Eventually.mono, OpenPartialHomeomorph.eventually_nhds'
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
y : H
hy : (↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y)) = (↑e'.symm : H → M) y
simp : g ((↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y))) = g ((↑e'.symm : H → M) y)
⊢ ((g ∘ (↑e.symm : H → M)) ∘ (↑(e.symm ≫ₕ e').symm : H → H)) y = (g ∘ (↑e'.symm : H → M)) y

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
M : Type u_2
H' : Type u_3
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
inst_3 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e
xe : x ∈ e.source
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas M G) e'
xe' : x ∈ e'.source
y : H
hy : (↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y)) = (↑e'.symm : H → M) y
rw rw₁ : g ((↑e'.symm : H → M) y) = g ((↑e'.symm : H → M) y)
⊢ g ((↑e.symm : H → M) ((↑e : M → H) ((↑e'.symm : H → M) y))) = g ((↑e'.symm : H → M) y)

Tactic:
rw [hy]
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
⊢ ContinuousWithinAt ((↑f : M' → H') ∘ g) s x

Tactic:
have hcont : ContinuousWithinAt (f ∘ g) s x := (f.continuousAt xf).comp_continuousWithinAt hgs
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
hcont : ContinuousWithinAt ((↑f : M' → H') ∘ g) s x
⊢ ((↑f : M' → H') ∘ g) x ∈ (f.symm ≫ₕ f').source

Tactic:
simp only [xf, xf', mfld_simps]
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
hcont : ContinuousWithinAt ((↑f : M' → H') ∘ g) s x
rw : P ((↑(f.symm ≫ₕ f') : H' → H') ∘ (↑f : M' → H') ∘ g) s x ↔ P ((↑f' : M' → H') ∘ g) s x
⊢ P ((↑f : M' → H') ∘ g) s x ↔ P ((↑f' : M' → H') ∘ g) s x

Tactic:
rw [← hG.left_invariance (compatible_of_mem_maximalAtlas hf hf') hcont
      (by simp only [xf, xf', mfld_simps])]

Premises used: StructureGroupoid.compatible_of_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.left_invariance
-- Module: Mathlib.Geometry.Manifold.LocalInvariantProperties
Goal:
H : Type u_1
H' : Type u_3
M' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace H'
inst_2 : TopologicalSpace M'
inst_3 : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
f f' : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
g : H → M'
x : H
s : Set H
hf : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f
xf : g x ∈ f.source
hf' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas M' G') f'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
hcont : ContinuousWithinAt ((↑f : M' → H') ∘ g) s x
⊢ ((↑(f.symm ≫ₕ f') : H' → H') ∘ (↑f : M' → H') ∘ g) x = ((↑f' : M' → H') ∘ g) x

Tactic:
simp only [xf, mfld_simps]