awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
he' : e' ∈ w_1
x' : ↥s
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ e' = subtypeRestr (chartAt H (↑x' : M)) ⋯

Tactic:
rw [hc'.symm, mem_singleton_iff] at he'

Premises used: Set.mem_singleton_iff, Eq.symm
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
he' : e' ∈ w_1
x' : ↥s
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
he'₁ : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
⊢ (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1

Tactic:
rw [hc'.symm, mem_singleton_iff] at he'

Premises used: Set.mem_singleton_iff, Eq.symm
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
rw : OpenPartialHomeomorph.symm (subtypeRestr (chartAt H (↑x : M)) ⋯) ≫ₕ subtypeRestr (chartAt H (↑x' : M)) ⋯ ∈ G
⊢ e.symm ≫ₕ e' ∈ G

Tactic:
rw [he, he']
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ OpenPartialHomeomorph.symm (subtypeRestr (chartAt H (↑x : M)) ⋯) ≫ₕ subtypeRestr (chartAt H (↑x' : M)) ⋯ ∈ G

Tactic:
G.mem_of_eqOnSource ?_
      (subtypeRestr_symm_trans_subtypeRestr (s := s) _ (chartAt H x) (chartAt H x'))

Premises used: StructureGroupoid.mem_of_eqOnSource, OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr, chartAt, Subtype.val
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
refine :
  OpenPartialHomeomorph.restr (OpenPartialHomeomorph.symm (chartAt H (↑x : M)) ≫ₕ chartAt H (↑x' : M))
      ((toPartialEquiv (chartAt H (↑x : M))).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' (↑s : Set M)) ∈
    G
⊢ OpenPartialHomeomorph.symm (subtypeRestr (chartAt H (↑x : M)) ⋯) ≫ₕ subtypeRestr (chartAt H (↑x' : M)) ⋯ ∈ G

Tactic:
refine G.mem_of_eqOnSource ?_
      (subtypeRestr_symm_trans_subtypeRestr (s := s) _ (chartAt H x) (chartAt H x'))

Premises used: StructureGroupoid.mem_of_eqOnSource, OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr, chartAt, Subtype.val
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
he₁ : OpenPartialHomeomorph.symm (chartAt H (↑x : M)) ≫ₕ chartAt H (↑x' : M) ∈ G
hs :
  IsOpen[inst]
    ((toPartialEquiv (chartAt H (↑x : M))).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' (↑s : Set M))
⊢ OpenPartialHomeomorph.restr (OpenPartialHomeomorph.symm (chartAt H (↑x : M)) ≫ₕ chartAt H (↑x' : M))
      ((toPartialEquiv (chartAt H (↑x : M))).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' (↑s : Set M)) ∈
    G

Tactic:
apply closedUnderRestriction'

Premises used: closedUnderRestriction'
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ OpenPartialHomeomorph.symm (chartAt H (↑x : M)) ≫ₕ chartAt H (↑x' : M) ∈ G

Tactic:
G.compatible (chart_mem_atlas _ _) (chart_mem_atlas _ _)

Premises used: StructureGroupoid.compatible, chart_mem_atlas
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ OpenPartialHomeomorph.symm (chartAt H (↑x : M)) ≫ₕ chartAt H (↑x' : M) ∈ G

Tactic:
exact G.compatible (chart_mem_atlas _ _) (chart_mem_atlas _ _)

Premises used: StructureGroupoid.compatible, chart_mem_atlas
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ IsOpen[inst]
    ((toPartialEquiv (chartAt H (↑x : M))).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' (↑s : Set M))

Tactic:
isOpen_inter_preimage_symm (chartAt _ _) s.2

Premises used: chartAt, TopologicalSpace.Opens.is_open', OpenPartialHomeomorph.isOpen_inter_preimage_symm
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
G : StructureGroupoid H
inst_3 : HasGroupoid M G
s : Opens M
inst_4 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
w : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x : ↥s
he : e = subtypeRestr (chartAt H (↑x : M)) ⋯
hc : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = w
w_1 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
x' : ↥s
he' : e' = subtypeRestr (chartAt H (↑x' : M)) ⋯
hc' : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w_1
⊢ IsOpen[inst]
    ((toPartialEquiv (chartAt H (↑x : M))).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) ⁻¹' (↑s : Set M))

Tactic:
exact isOpen_inter_preimage_symm (chartAt _ _) s.2

Premises used: chartAt, TopologicalSpace.Opens.is_open', OpenPartialHomeomorph.isOpen_inter_preimage_symm
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U : Opens M
x : ↥U
set :
  let e : OpenPartialHomeomorph M H := chartAt H (↑x : M);
  (↑e.symm : H → M) =ᶠ[𝓝 ((↑e : M → H) (↑x : M))]
    Subtype.val (p := fun (x : M) ↦ x ∈ U) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H (↑x : M))) : H → M) =ᶠ[𝓝 ((↑(chartAt H (↑x : M)) : M → H) (↑x : M))]
    Subtype.val (p := fun (x : M) ↦ x ∈ U) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)

Tactic:
set e := chartAt H x.val

Premises used: chartAt, Subtype.val
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U : Opens M
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
apply : (↑e : M → H) (↑x : M) ∈ (e.subtypeRestr ⋯).target
⊢ (e.subtypeRestr ⋯).target ∈ 𝓝 ((↑e : M → H) (↑x : M))

Tactic:
apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds

Premises used: OpenPartialHomeomorph.subtypeRestr, Nonempty.intro, IsOpen.mem_nhds, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U : Opens M
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
⊢ (↑e : M → H) (↑x : M) ∈ (e.subtypeRestr ⋯).target

Tactic:
e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)

Premises used: OpenPartialHomeomorph.map_subtype_source, mem_chart_source, Nonempty.intro
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U : Opens M
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
⊢ (↑e : M → H) (↑x : M) ∈ (e.subtypeRestr ⋯).target

Tactic:
exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)

Premises used: OpenPartialHomeomorph.map_subtype_source, mem_chart_source, Nonempty.intro
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U : Opens M
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
⊢ (e.subtypeRestr ⋯).target ∈ 𝓝 ((↑e : M → H) (↑x : M))

Tactic:
have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
    apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
    exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U : Opens M
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
heUx_nhds : (e.subtypeRestr ⋯).target ∈ 𝓝 ((↑e : M → H) (↑x : M))
⊢ (↑e.symm : H → M) =ᶠ[𝓝 ((↑e : M → H) (↑x : M))]
    Subtype.val (p := fun (x : M) ↦ x ∈ U) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)

Tactic:
Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn ⟨x⟩)

Premises used: Filter.eventuallyEq_of_mem, Nonempty.intro, OpenPartialHomeomorph.subtypeRestr_symm_eqOn
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U : Opens M
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
heUx_nhds : (e.subtypeRestr ⋯).target ∈ 𝓝 ((↑e : M → H) (↑x : M))
⊢ (↑e.symm : H → M) =ᶠ[𝓝 ((↑e : M → H) (↑x : M))]
    Subtype.val (p := fun (x : M) ↦ x ∈ U) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)

Tactic:
exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn ⟨x⟩)

Premises used: Filter.eventuallyEq_of_mem, Nonempty.intro, OpenPartialHomeomorph.subtypeRestr_symm_eqOn
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
apply : (↑e : M → H) (↑x : M) ∈ (e.subtypeRestr ⋯).target
⊢ (e.subtypeRestr ⋯).target ∈ 𝓝 ((↑e : M → H) (↑x : M))

Tactic:
apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds

Premises used: OpenPartialHomeomorph.subtypeRestr, Nonempty.intro, IsOpen.mem_nhds, OpenPartialHomeomorph.open_target
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
⊢ (↑e : M → H) (↑x : M) ∈ (e.subtypeRestr ⋯).target

Tactic:
e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)

Premises used: OpenPartialHomeomorph.map_subtype_source, mem_chart_source, Nonempty.intro
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
⊢ (↑e : M → H) (↑x : M) ∈ (e.subtypeRestr ⋯).target

Tactic:
exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)

Premises used: OpenPartialHomeomorph.map_subtype_source, mem_chart_source, Nonempty.intro
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
⊢ (e.subtypeRestr ⋯).target ∈ 𝓝 ((↑e : M → H) (↑x : M))

Tactic:
have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
    apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
    exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
heUx_nhds : (e.subtypeRestr ⋯).target ∈ 𝓝 ((↑e : M → H) (↑x : M))
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H (inclusion hUV x))) :
      H →
        ↥V) =ᶠ[𝓝
      ((↑(chartAt H (inclusion hUV x)) : ↥V → H) (Set.inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))]
    inclusion hUV ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)

Tactic:
Filter.eventuallyEq_of_mem heUx_nhds <| e.subtypeRestr_symm_eqOn_of_le ⟨x⟩
    ⟨Opens.inclusion hUV x⟩ hUV

Premises used: Filter.eventuallyEq_of_mem, TopologicalSpace.Opens.inclusion, Nonempty.intro, OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
U V : Opens M
hUV : U ≤ V
x : ↥U
e : OpenPartialHomeomorph M H := chartAt H (↑x : M)
heUx_nhds : (e.subtypeRestr ⋯).target ∈ 𝓝 ((↑e : M → H) (↑x : M))
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H (inclusion hUV x))) :
      H →
        ↥V) =ᶠ[𝓝
      ((↑(chartAt H (inclusion hUV x)) : ↥V → H) (Set.inclusion (s := (↑U : Set M)) (t := (↑V : Set M)) hUV x))]
    inclusion hUV ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → ↥U)

Tactic:
exact Filter.eventuallyEq_of_mem heUx_nhds <| e.subtypeRestr_symm_eqOn_of_le ⟨x⟩
    ⟨Opens.inclusion hUV x⟩ hUV

Premises used: Filter.eventuallyEq_of_mem, TopologicalSpace.Opens.inclusion, Nonempty.intro, OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
G : StructureGroupoid H
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (atlas H ↥s) e'
obtain :
  ∀ (x : ↥s) (this : e' = subtypeRestr (chartAt H (↑x : M)) hs),
    (e.subtypeRestr hs).symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e.subtypeRestr hs ∈ G
⊢ (e.subtypeRestr hs).symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e.subtypeRestr hs ∈ G

Tactic:
obtain ⟨x, this⟩ := Opens.chart_eq hs he'

Premises used: TopologicalSpace.Opens.chart_eq
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
G : StructureGroupoid H
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (atlas H ↥s) e'
x : ↥s
this : e' = subtypeRestr (chartAt H (↑x : M)) hs
rw :
  (e.subtypeRestr hs).symm ≫ₕ subtypeRestr (chartAt H (↑x : M)) hs ∈ G ∧
    OpenPartialHomeomorph.symm (subtypeRestr (chartAt H (↑x : M)) hs) ≫ₕ e.subtypeRestr hs ∈ G
⊢ (e.subtypeRestr hs).symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e.subtypeRestr hs ∈ G

Tactic:
rw [this]
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
G : StructureGroupoid H
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (atlas H ↥s) e'
x : ↥s
this : e' = subtypeRestr (chartAt H (↑x : M)) hs
⊢ (e.subtypeRestr hs).symm ≫ₕ subtypeRestr (chartAt H (↑x : M)) hs ∈ G ∧
    OpenPartialHomeomorph.symm (subtypeRestr (chartAt H (↑x : M)) hs) ≫ₕ e.subtypeRestr hs ∈ G

Tactic:
⟨G.trans_restricted he (chart_mem_atlas H (x : M)) hs,
         G.trans_restricted (chart_mem_atlas H (x : M)) he hs⟩

Premises used: chart_mem_atlas, StructureGroupoid.trans_restricted, And.intro, Subtype.val
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
M : Type u_2
inst : TopologicalSpace H
inst_1 : TopologicalSpace M
inst_2 : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
G : StructureGroupoid H
inst_3 : HasGroupoid M G
inst_4 : ClosedUnderRestriction G
e' : OpenPartialHomeomorph.{u_2, u} (↥s) H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (atlas H ↥s) e'
x : ↥s
this : e' = subtypeRestr (chartAt H (↑x : M)) hs
⊢ (e.subtypeRestr hs).symm ≫ₕ subtypeRestr (chartAt H (↑x : M)) hs ∈ G ∧
    OpenPartialHomeomorph.symm (subtypeRestr (chartAt H (↑x : M)) hs) ≫ₕ e.subtypeRestr hs ∈ G

Tactic:
exact ⟨G.trans_restricted he (chart_mem_atlas H (x : M)) hs,
         G.trans_restricted (chart_mem_atlas H (x : M)) he hs⟩
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M_1 : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M_1
inst_2 : ChartedSpace H M_1
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : HasGroupoid M G
c c' : OpenPartialHomeomorph M H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c'
change : c.symm ≫ₕ OpenPartialHomeomorph.refl M ≫ₕ c' ∈ G
⊢ c.symm ≫ₕ Homeomorph.toOpenPartialHomeomorph (Homeomorph.refl M) ≫ₕ c' ∈ G

Tactic:
change OpenPartialHomeomorph.symm c ≫ₕ OpenPartialHomeomorph.refl M ≫ₕ c' ∈ G

Premises used: OpenPartialHomeomorph.symm, OpenPartialHomeomorph.refl
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M_1 : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M_1
inst_2 : ChartedSpace H M_1
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : HasGroupoid M G
c c' : OpenPartialHomeomorph M H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c'
rw : c.symm ≫ₕ c' ∈ G
⊢ c.symm ≫ₕ OpenPartialHomeomorph.refl M ≫ₕ c' ∈ G

Tactic:
rw [OpenPartialHomeomorph.refl_trans]

Premises used: OpenPartialHomeomorph.refl_trans
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
H' : Type u_1
M_1 : Type u_2
M' : Type u_3
M'' : Type u_4
inst : TopologicalSpace H
inst_1 : TopologicalSpace M_1
inst_2 : ChartedSpace H M_1
inst_3 : TopologicalSpace M'
inst_4 : TopologicalSpace M''
G : StructureGroupoid H
inst_5 : ChartedSpace H M'
inst_6 : ChartedSpace H M''
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
inst_9 : HasGroupoid M G
c c' : OpenPartialHomeomorph M H
hc : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c
hc' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) c'
⊢ c.symm ≫ₕ c' ∈ G

Tactic:
G.compatible hc hc'

Premises used: StructureGroupoid.compatible