-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem closedUnderRestriction_iff_id_le (G : StructureGroupoid H) :
    ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G

Proof state:
case h.e'_5
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ ofSet s hs = (PartialHomeomorph.refl H).restr s

Tactic:
ext

Result:
case h.e'_5.h
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs) x✝ = ↑((PartialHomeomorph.refl H).restr s) x✝

case h.e'_5.hinv
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs).symm x✝ = ↑((PartialHomeomorph.refl H).restr s).symm x✝

case h.e'_5.hs.h
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ x✝ ∈ (ofSet s hs).source ↔ x✝ ∈ ((PartialHomeomorph.refl H).restr s).source

Proof state:
case mpr.closedUnderRestriction.a
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : PartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ∈ idRestrGroupoid

Tactic:
exact idRestrGroupoid_mem hs

Result:
no goals

Proof state:
case mpr
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ClosedUnderRestriction G

Tactic:
constructor

Result:
case mpr.closedUnderRestriction
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ∀ {e : PartialHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen s → e.restr s ∈ G

Proof state:
case mpr.closedUnderRestriction
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ∀ {e : PartialHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen s → e.restr s ∈ G

Tactic:
intro e he s hs

Result:
case mpr.closedUnderRestriction
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : PartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ e.restr s ∈ G

Proof state:
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G

Tactic:
constructor

Result:
case mp
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ ClosedUnderRestriction G → idRestrGroupoid ≤ G

case mpr
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ idRestrGroupoid ≤ G → ClosedUnderRestriction G

Proof state:
case mp.intro.intro
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ ofSet s hs ∈ G

Tactic:
convert closedUnderRestriction' G.id_mem hs

Result:
case h.e'_5
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ ofSet s hs = (PartialHomeomorph.refl H).restr s

Proof state:
case mpr
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ idRestrGroupoid ≤ G → ClosedUnderRestriction G

Tactic:
intro h

Result:
case mpr
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
⊢ ClosedUnderRestriction G

Proof state:
case mp.intro.intro
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ e ∈ G

Tactic:
refine G.mem_of_eqOnSource ?_ hes

Result:
case mp.intro.intro
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ ofSet s hs ∈ G

Proof state:
case mpr.closedUnderRestriction
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : PartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ≫ₕ e ∈ G

Tactic:
refine G.trans ?_ he

Result:
case mpr.closedUnderRestriction
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : PartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ∈ G

Proof state:
case mp
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
⊢ ClosedUnderRestriction G → idRestrGroupoid ≤ G

Tactic:
intro _i

Result:
case mp
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ idRestrGroupoid ≤ G

Proof state:
case mp
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ ∀ e ∈ idRestrGroupoid, e ∈ G

Tactic:
rintro e ⟨s, hs, hes⟩

Result:
case mp.intro.intro
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
⊢ e ∈ G

Proof state:
case mp
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ idRestrGroupoid ≤ G

Tactic:
rw [StructureGroupoid.le_iff]

Result:
case mp
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ ∀ e ∈ idRestrGroupoid, e ∈ G

Proof state:
case h.e'_5.hinv
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs).symm x✝ = ↑((PartialHomeomorph.refl H).restr s).symm x✝

Tactic:
simp [hs]

Result:
no goals

Proof state:
case h.e'_5.h
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ ↑(ofSet s hs) x✝ = ↑((PartialHomeomorph.refl H).restr s) x✝

Tactic:
rw [PartialHomeomorph.restr_apply, PartialHomeomorph.refl_apply, id, ofSet_apply, id_eq]

Result:
no goals

Proof state:
case h.e'_5.hs.h
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
e : PartialHomeomorph H H
s : Set H
hs : IsOpen s
hes : e ≈ ofSet s hs
x✝ : H
⊢ x✝ ∈ (ofSet s hs).source ↔ x✝ ∈ ((PartialHomeomorph.refl H).restr s).source

Tactic:
simp [hs.interior_eq]

Result:
no goals

Proof state:
case mpr.closedUnderRestriction
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : PartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ e.restr s ∈ G

Tactic:
rw [← ofSet_trans (e : PartialHomeomorph H H) hs]

Result:
case mpr.closedUnderRestriction
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : PartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ≫ₕ e ∈ G

Proof state:
case mpr.closedUnderRestriction
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : PartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ∈ G

Tactic:
apply StructureGroupoid.le_iff.mp h

Result:
case mpr.closedUnderRestriction.a
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : PartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen s
⊢ ofSet s hs ∈ idRestrGroupoid