-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem singleton_hasGroupoid (h : e.source = Set.univ) (G : StructureGroupoid H)
    [ClosedUnderRestriction G] : @HasGroupoid _ _ _ _ (e.singletonChartedSpace h) G :=
  { __ := e.singletonChartedSpace h
    compatible

Proof state:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : PartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
⊢ ∀ {e_1 e' : PartialHomeomorph α H}, e_1 ∈ atlas H α → e' ∈ atlas H α → e_1.symm ≫ₕ e' ∈ G

Tactic:
intro e' e'' he' he''

Result:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : PartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : PartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ e'.symm ≫ₕ e'' ∈ G

Proof state:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : PartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : PartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ e.symm ≫ₕ e ∈ G

Tactic:
refine G.mem_of_eqOnSource ?_ e.symm_trans_self

Result:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : PartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : PartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ ofSet e.target ⋯ ∈ G

Proof state:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : PartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : PartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ ClosedUnderRestriction G

Tactic:
assumption

Result:
no goals

Proof state:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : PartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : PartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ ofSet e.target ⋯ ∈ G

Tactic:
have hle : idRestrGroupoid ≤ G := (closedUnderRestriction_iff_id_le G).mp (by assumption)

Result:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : PartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : PartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
hle : idRestrGroupoid ≤ G
⊢ ofSet e.target ⋯ ∈ G

Proof state:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : PartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : PartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ e'.symm ≫ₕ e'' ∈ G

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

Result:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : PartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : PartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
⊢ e.symm ≫ₕ e ∈ G

Proof state:
H : Type u
inst✝² : TopologicalSpace H
α : Type u_5
inst✝¹ : TopologicalSpace α
e : PartialHomeomorph α H
h : e.source = univ
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
e' e'' : PartialHomeomorph α H
he' : e' ∈ atlas H α
he'' : e'' ∈ atlas H α
hle : idRestrGroupoid ≤ G
⊢ ofSet e.target ⋯ ∈ G

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

Result:
no goals