no goals
H : Type u_1
M : Type ?u.71024
H' : Type ?u.71027
M' : Type ?u.71030
X : Type ?u.71033
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : TopologicalSpace H'
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : TopologicalSpace X
G✝ : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f✝ f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x✝ : M
Q : (H → H) → Set H → H → Prop
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : LocalHomeomorph H H
x : H
⊢ x ∈ f.source ∪ f.sourceᶜ
simp_rw [union_compl_self, mem_univ]