no goals
H : Type u
H' : Type ?u.74250
M : Type ?u.74253
M' : Type ?u.74256
M'' : Type ?u.74259
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
⊢ LocalHomeomorph.refl H ∈ atlas H H
simp