awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))
⊢ (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G

Tactic:
have : (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G := by
    apply G.mem_of_eqOnSource (closedUnderRestriction' (he e' he').1 hs'')
    exact e.restr_symm_trans (e.open_source.inter hs) hs'' inter_subset_left
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))
this : (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G
⊢ (e.restr s).symm ≫ₕ e' ∈ G

Tactic:
G.mem_of_eqOnSource this ?_

Premises used: StructureGroupoid.mem_of_eqOnSource
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))
this : (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G
refine : (e.restr s).symm ≫ₕ e' ≈ (e.restr (e.source ∩ s)).symm ≫ₕ e'
⊢ (e.restr s).symm ≫ₕ e' ∈ G

Tactic:
refine G.mem_of_eqOnSource this ?_

Premises used: StructureGroupoid.mem_of_eqOnSource
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))
this : (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G
⊢ (e.restr s).symm ≫ₕ e' ≈ (e.restr (e.source ∩ s)).symm ≫ₕ e'

Tactic:
EqOnSource.trans' (Setoid.symm e.restr_inter_source).symm' (eqOnSource_refl e')

Premises used: OpenPartialHomeomorph.restr_inter_source, OpenPartialHomeomorph.EqOnSource.trans', OpenPartialHomeomorph.eqOnSource_refl, Setoid.symm, OpenPartialHomeomorph.EqOnSource.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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e : M → H) '' (e.source ∩ s))
this : (e.restr (e.source ∩ s)).symm ≫ₕ e' ∈ G
⊢ (e.restr s).symm ≫ₕ e' ≈ (e.restr (e.source ∩ s)).symm ≫ₕ e'

Tactic:
exact EqOnSource.trans' (Setoid.symm e.restr_inter_source).symm' (eqOnSource_refl e')

Premises used: OpenPartialHomeomorph.restr_inter_source, OpenPartialHomeomorph.EqOnSource.trans', OpenPartialHomeomorph.eqOnSource_refl, Setoid.symm, OpenPartialHomeomorph.EqOnSource.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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
rw : IsOpen[inst_1] (e'.source ∩ s)
⊢ IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))

Tactic:
rw [isOpen_image_iff_of_subset_source e' inter_subset_left]

Premises used: OpenPartialHomeomorph.isOpen_image_iff_of_subset_source, Set.inter_subset_left
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
⊢ IsOpen[inst_1] (e'.source ∩ s)

Tactic:
e'.open_source.inter hs

Premises used: OpenPartialHomeomorph.open_source, IsOpen.inter
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
⊢ IsOpen[inst_1] (e'.source ∩ s)

Tactic:
exact e'.open_source.inter hs

Premises used: OpenPartialHomeomorph.open_source, IsOpen.inter
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
⊢ IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))

Tactic:
have hs'' : IsOpen (e' '' (e'.source ∩ s)) := by
    rw [isOpen_image_iff_of_subset_source e' inter_subset_left]
    exact e'.open_source.inter hs
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' rw : IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))
⊢ IsOpen[inst] (e'.target ∩ (↑e'.symm : H → M) ⁻¹' s)

Tactic:
rw [← image_source_inter_eq']

Premises used: OpenPartialHomeomorph.image_source_inter_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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))
⊢ IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))

Tactic:
isOpen_image_source_inter e' hs

Premises used: OpenPartialHomeomorph.isOpen_image_source_inter
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))
⊢ IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))

Tactic:
exact isOpen_image_source_inter e' hs

Premises used: OpenPartialHomeomorph.isOpen_image_source_inter
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))
⊢ IsOpen[inst] (e'.target ∩ (↑e'.symm : H → M) ⁻¹' s)

Tactic:
have ht : IsOpen (e'.target ∩ e'.symm ⁻¹' s) := by
    rw [← image_source_inter_eq']
    exact isOpen_image_source_inter e' hs
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))
ht : IsOpen[inst] (e'.target ∩ (↑e'.symm : H → M) ⁻¹' s)
⊢ e'.symm ≫ₕ e.restr s ∈ G

Tactic:
G.mem_of_eqOnSource (closedUnderRestriction' (he e' he').2 ht) (e.symm_trans_restr e' hs)

Premises used: StructureGroupoid.mem_of_eqOnSource, OpenPartialHomeomorph.symm_trans_restr, And.right, closedUnderRestriction'
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e e' : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (atlas H M) e'
s : Set M
hs : IsOpen[inst_1] s
hs'' : IsOpen[inst] ((↑e' : M → H) '' (e'.source ∩ s))
ht : IsOpen[inst] (e'.target ∩ (↑e'.symm : H → M) ⁻¹' s)
⊢ e'.symm ≫ₕ e.restr s ∈ G

Tactic:
exact G.mem_of_eqOnSource (closedUnderRestriction' (he e' he').2 ht) (e.symm_trans_restr e' hs)

Premises used: StructureGroupoid.mem_of_eqOnSource, OpenPartialHomeomorph.symm_trans_restr, And.right, closedUnderRestriction'
-- 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
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
e : OpenPartialHomeomorph M H
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) e
s : Set M
hs : IsOpen[inst_1] s
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (StructureGroupoid.maximalAtlas M G) (e.restr s)

Tactic:
fun _e' he' ↦ ⟨restr_mem_maximalAtlas_aux1 G he he' hs, restr_mem_maximalAtlas_aux2 G he he' hs⟩

Premises used: Set.Mem, _private.0.restr_mem_maximalAtlas_aux1, setOf, _private.0.restr_mem_maximalAtlas_aux2, And.intro, StructureGroupoid.maximalAtlas
-- 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
α : Type u_5
inst_3 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
x : α
rw : Membership.mem (γ := Set α) univ x
⊢ x ∈ e.source

Tactic:
rw [h]
-- 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
α : Type u_5
inst_3 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
x : α
⊢ Membership.mem (γ := Set α) univ x

Tactic:
apply mem_univ

Premises used: Set.mem_univ
-- 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
α : Type u_5
inst_3 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
x : α
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph α H)) {e} e

Tactic:
tauto
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
x : α
⊢ chartAt H x = e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
x : α
⊢ (toPartialEquiv (chartAt H x)).source = univ

Tactic:
h
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
e' : OpenPartialHomeomorph α H
h' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) ChartedSpace.atlas e'
⊢ e' = e

Tactic:
h'

Premises used: Set.Mem, setOf, Set.singleton
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst_2 : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e'
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e''
rw : e.symm ≫ₕ e ∈ G
⊢ e'.symm ≫ₕ e'' ∈ G

Tactic:
rw [e.singletonChartedSpace_mem_atlas_eq h e' he',
        e.singletonChartedSpace_mem_atlas_eq h e'' he'']

Premises used: OpenPartialHomeomorph.singletonChartedSpace_mem_atlas_eq
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst_2 : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e'
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e''
⊢ e.symm ≫ₕ e ∈ G

Tactic:
G.mem_of_eqOnSource ?_ e.symm_trans_self

Premises used: StructureGroupoid.mem_of_eqOnSource, OpenPartialHomeomorph.symm_trans_self
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst_2 : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e'
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e''
refine : ofSet e.target ⋯ ∈ G
⊢ e.symm ≫ₕ e ∈ G

Tactic:
refine G.mem_of_eqOnSource ?_ e.symm_trans_self

Premises used: StructureGroupoid.mem_of_eqOnSource, OpenPartialHomeomorph.symm_trans_self
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst_2 : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e'
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e''
⊢ ClosedUnderRestriction G

Tactic:
assumption
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst_2 : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e'
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e''
⊢ idRestrGroupoid ≤ G

Tactic:
have hle : idRestrGroupoid ≤ G := (closedUnderRestriction_iff_id_le G).mp (by assumption)
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst_2 : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e'
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e''
hle : idRestrGroupoid ≤ G
⊢ ofSet e.target ⋯ ∈ G

Tactic:
StructureGroupoid.le_iff.mp hle _ (idRestrGroupoid_mem _)

Premises used: StructureGroupoid.le_iff, idRestrGroupoid_mem, Iff.mp
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
e : OpenPartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst_2 : ClosedUnderRestriction G
e' e'' : OpenPartialHomeomorph α H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e'
he'' : Membership.mem (γ := Set (OpenPartialHomeomorph α H)) (atlas H α) e''
hle : idRestrGroupoid ≤ G
⊢ ofSet e.target ⋯ ∈ G

Tactic:
exact StructureGroupoid.le_iff.mp hle _ (idRestrGroupoid_mem _)

Premises used: StructureGroupoid.le_iff, idRestrGroupoid_mem, Iff.mp
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
inst_2 : Nonempty α
f : α → H
h : IsOpenEmbedding f
x : α
⊢ (↑(chartAt H x) : α → H) = f

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
α : Type u_5
inst_1 : TopologicalSpace α
inst_2 : Nonempty α
f : α → H
h : IsOpenEmbedding f
G : StructureGroupoid H
inst_3 : ClosedUnderRestriction G
⊢ HasGroupoid α G

Tactic:
(h.toOpenPartialHomeomorph f).singleton_hasGroupoid (toOpenPartialHomeomorph_source _ _) G

Premises used: Topology.IsOpenEmbedding.toOpenPartialHomeomorph_source, Topology.IsOpenEmbedding.toOpenPartialHomeomorph, OpenPartialHomeomorph.singleton_hasGroupoid
-- 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
x : ↥s
simp :
  ∃ (i : ↥s),
    Eq (α := OpenPartialHomeomorph.{u_2, u} (↥s) H) (subtypeRestr (chartAt H (↑x : M)) ⋯)
      (subtypeRestr (chartAt H (↑i : M)) ⋯)
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (⋃ (x : ↥s), {subtypeRestr (chartAt H (↑x : M)) ⋯})
    (subtypeRestr (chartAt H (↑x : M)) ⋯)

Tactic:
simp only [mem_iUnion, mem_singleton_iff]

Premises used: Set.mem_iUnion, Set.mem_singleton_iff
-- 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
x w : ↥s
h :
  Eq (α := OpenPartialHomeomorph.{u_2, u} (↥s) H) (subtypeRestr (chartAt H (↑x : M)) ⋯)
    (subtypeRestr (chartAt H (↑x : M)) ⋯)
⊢ ∃ (i : ↥s),
    Eq (α := OpenPartialHomeomorph.{u_2, u} (↥s) H) (subtypeRestr (chartAt H (↑x : M)) ⋯)
      (subtypeRestr (chartAt H (↑i : M)) ⋯)

Tactic:
use x
-- 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
s : Opens M
x : ↥s
⊢ Eq (α := OpenPartialHomeomorph.{u_2, u} (↥s) H) (chartAt H x) (subtypeRestr (chartAt H (↑x : M)) ⋯)

Tactic:
rfl

Premises used: rfl
-- 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
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
e : OpenPartialHomeomorph.{u_2, u} (↥s) H
he : Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (atlas H ↥s) e
rcases :
  ∀ (xset : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (he : e ∈ xset) (x : ↥s)
    (hx :
      (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = xset),
    ∃ (x : ↥s), e = subtypeRestr (chartAt H (↑x : M)) hs
⊢ ∃ (x : ↥s), e = subtypeRestr (chartAt H (↑x : M)) hs

Tactic:
rcases he with ⟨xset, ⟨x, hx⟩, he⟩
-- 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
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
e : OpenPartialHomeomorph.{u_2, u} (↥s) H
xset : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
he : e ∈ xset
x : ↥s
hx : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = xset
⊢ e ∈ xset

Tactic:
he
-- 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
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
e : OpenPartialHomeomorph.{u_2, u} (↥s) H
xset : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
he : e ∈ xset
x : ↥s
hx : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = xset
⊢ Membership.mem (γ := Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) {subtypeRestr (chartAt H (↑x : M)) hs} e

Tactic:
convert! he
-- 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
s : Opens M
hs : Nonempty.{u_2 + 1} ↥s
e : OpenPartialHomeomorph.{u_2, u} (↥s) H
xset : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)
he : e ∈ xset
x : ↥s
hx : (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x = xset
⊢ ∃ (x : ↥s), e = subtypeRestr (chartAt H (↑x : M)) hs

Tactic:
exact ⟨x, mem_singleton_iff.mp (by convert! he)⟩
-- Module: Mathlib.Geometry.Manifold.HasGroupoid
Goal:
H : Type u
inst : TopologicalSpace H
t : Opens H
ht : Nonempty.{u + 1} ↥t
e' : OpenPartialHomeomorph (↥t) H
he' : Membership.mem (γ := Set (OpenPartialHomeomorph (↥t) H)) (atlas H ↥t) e'
⊢ ∃ (x : ↥t), e' = subtypeRestr (chartAt H (↑x : H)) ht

Tactic:
chart_eq ht he'

Premises used: TopologicalSpace.Opens.chart_eq
-- 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)
he : e ∈ w
x : ↥s
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
rw :
  ∀ (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 : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H)) (he' : e' ∈ w) (x' : ↥s)
    (hc' :
      (fun (x : ↥s) ↦ ({subtypeRestr (chartAt H (↑x : M)) ⋯} : Set (OpenPartialHomeomorph.{u_2, u} (↥s) H))) x' = w),
    e.symm ≫ₕ e' ∈ G
⊢ e.symm ≫ₕ e' ∈ G

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

Premises used: Set.mem_singleton_iff, Eq.symm