H : Type u
H' : Type ?u.74549
M : Type ?u.74552
M' : Type ?u.74555
M'' : Type ?u.74558
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
f : LocalHomeomorph H H
hf : f ∈ G
⊢ LocalHomeomorph.symm f ≫ₕ LocalHomeomorph.refl H ∈ G ∧ LocalHomeomorph.symm (LocalHomeomorph.refl H) ≫ₕ f ∈ G
H : Type u
H' : Type ?u.74549
M : Type ?u.74552
M' : Type ?u.74555
M'' : Type ?u.74558
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
f : LocalHomeomorph H H
hf : f ∈ G
⊢ f ∈ maximalAtlas H G
rintro e (rfl : e = LocalHomeomorph.refl H)
no goals
H : Type u
H' : Type ?u.74549
M : Type ?u.74552
M' : Type ?u.74555
M'' : Type ?u.74558
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
f : LocalHomeomorph H H
hf : f ∈ G
⊢ LocalHomeomorph.symm f ≫ₕ LocalHomeomorph.refl H ∈ G ∧ LocalHomeomorph.symm (LocalHomeomorph.refl H) ≫ₕ f ∈ G
exact ⟨G.trans (G.symm hf) G.id_mem, G.trans (G.symm G.id_mem) hf⟩