case mp
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ ClosedUnderRestriction G → idRestrGroupoid ≤ G

case mpr
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ idRestrGroupoid ≤ G → ClosedUnderRestriction G
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G
constructor
case mp
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ idRestrGroupoid ≤ G
case mp
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ ClosedUnderRestriction G → idRestrGroupoid ≤ G
intro _i
case mp
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ ∀ (e : LocalHomeomorph H H), e ∈ idRestrGroupoid → e ∈ G
case mp
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ idRestrGroupoid ≤ G
apply StructureGroupoid.le_iff.mpr
case mp.intro.intro
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ e ∈ G
case mp
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ ∀ (e : LocalHomeomorph H H), e ∈ idRestrGroupoid → e ∈ G
rintro e ⟨s, hs, hes⟩
case mp.intro.intro
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ ofSet s hs ∈ G
case mp.intro.intro
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ e ∈ G
refine' G.eq_on_source _ hes
case h.e'_4
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ ofSet s hs = LocalHomeomorph.restr (LocalHomeomorph.refl H) s
case mp.intro.intro
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ ofSet s hs ∈ G
convert closedUnderRestriction' G.id_mem hs
case h.e'_4.h
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs) x✝ = ↑(LocalHomeomorph.restr (LocalHomeomorph.refl H) s) x✝

case h.e'_4.hinv
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(LocalHomeomorph.symm (ofSet s hs)) x✝ =
    ↑(LocalHomeomorph.symm (LocalHomeomorph.restr (LocalHomeomorph.refl H) s)) x✝

case h.e'_4.hs.h
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ x✝ ∈ (ofSet s hs).toLocalEquiv.source ↔ x✝ ∈ (LocalHomeomorph.restr (LocalHomeomorph.refl H) s).toLocalEquiv.source
case h.e'_4
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ ofSet s hs = LocalHomeomorph.restr (LocalHomeomorph.refl H) s
ext
no goals
case h.e'_4.h
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs) x✝ = ↑(LocalHomeomorph.restr (LocalHomeomorph.refl H) s) x✝
rw [LocalHomeomorph.restr_apply, LocalHomeomorph.refl_apply, id, ofSet_apply, id_eq]
no goals
case h.e'_4.hinv
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(LocalHomeomorph.symm (ofSet s hs)) x✝ =
    ↑(LocalHomeomorph.symm (LocalHomeomorph.restr (LocalHomeomorph.refl H) s)) x✝
simp [hs]
no goals
case h.e'_4.hs.h
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : LocalHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ x✝ ∈ (ofSet s hs).toLocalEquiv.source ↔ x✝ ∈ (LocalHomeomorph.restr (LocalHomeomorph.refl H) s).toLocalEquiv.source
simp [hs.interior_eq]
case mpr
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ClosedUnderRestriction G
case mpr
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ idRestrGroupoid ≤ G → ClosedUnderRestriction G
intro h
case mpr.closedUnderRestriction
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ∀ {e : LocalHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen s → LocalHomeomorph.restr e s ∈ G
case mpr
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ClosedUnderRestriction G
constructor
case mpr.closedUnderRestriction
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : LocalHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ LocalHomeomorph.restr e s ∈ G
case mpr.closedUnderRestriction
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ∀ {e : LocalHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen s → LocalHomeomorph.restr e s ∈ G
intro e he s hs
case mpr.closedUnderRestriction
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : LocalHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ≫ₕ e ∈ G
case mpr.closedUnderRestriction
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : LocalHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ LocalHomeomorph.restr e s ∈ G
rw [← ofSet_trans (e : LocalHomeomorph H H) hs]
case mpr.closedUnderRestriction
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : LocalHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ∈ G
case mpr.closedUnderRestriction
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : LocalHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ≫ₕ e ∈ G
refine' G.trans _ he
case mpr.closedUnderRestriction.a
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : LocalHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ∈ idRestrGroupoid
case mpr.closedUnderRestriction
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : LocalHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ∈ G
apply StructureGroupoid.le_iff.mp h
no goals
case mpr.closedUnderRestriction.a
H : Type u
H' : Type ?u.37363
M : Type ?u.37366
M' : Type ?u.37369
M'' : Type ?u.37372
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : LocalHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ∈ idRestrGroupoid
exact idRestrGroupoid_mem hs