-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem StructureGroupoid.restriction_mem_maximalAtlas_subtype
    {e : PartialHomeomorph M H} (he : e ∈ atlas H M)
    (hs : Nonempty e.source) [HasGroupoid M G] [ClosedUnderRestriction G] :
    let s := { carrier := e.source, is_open' := e.open_source : Opens M }
    let t := { carrier := e.target, is_open' := e.open_target : Opens H }
    ∀ c' ∈ atlas H t, e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ c' ∈ G.maximalAtlas s

Proof state:
case intro
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : PartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
goal : PartialHomeomorph (↑e.source) H :=
  e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this
⊢ e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this ∈ maximalAtlas (↥s) G

Tactic:
have : goal ≈ e.subtypeRestr (s := s) hs :=
  (goal.eqOnSource_iff (e.subtypeRestr (s := s) hs)).mpr
    ⟨by
      simp only [trans_toPartialEquiv, PartialEquiv.trans_source,
        Homeomorph.toPartialHomeomorph_source, toFun_eq_coe, Homeomorph.toPartialHomeomorph_apply,
        Opens.partialHomeomorphSubtypeCoe_source, preimage_univ, inter_self, subtypeRestr_source,
        goal, s]
      exact Subtype.coe_preimage_self _ |>.symm, by intro _ _; rfl⟩

Result:
case intro
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : PartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this✝ : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this✝
goal : PartialHomeomorph (↑e.source) H :=
  e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this✝
this : goal ≈ e.subtypeRestr hs
⊢ e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this✝ ∈ maximalAtlas (↥s) G

Proof state:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : PartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
goal : PartialHomeomorph (↑e.source) H :=
  e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this
x✝ : ↑e.source
a✝ : x✝ ∈ goal.source
⊢ ↑goal.toPartialEquiv x✝ = ↑(e.subtypeRestr hs).toPartialEquiv x✝

Tactic:
rfl

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
⊢ let s := { carrier := e.source, is_open' := ⋯ };
  let t := { carrier := e.target, is_open' := ⋯ };
  ∀ c' ∈ atlas H ↥t, e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ c' ∈ maximalAtlas (↥s) G

Tactic:
intro s t c' hc'

Result:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : PartialHomeomorph (↥t) H
hc' : c' ∈ atlas H ↥t
⊢ e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ c' ∈ maximalAtlas (↥s) G

Proof state:
case intro
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : PartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this✝ : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this✝
goal : PartialHomeomorph (↑e.source) H :=
  e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this✝
this : goal ≈ e.subtypeRestr hs
⊢ e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this✝ ∈ maximalAtlas (↥s) G

Tactic:
exact G.mem_maximalAtlas_of_eqOnSource (M := s) this (G.restriction_in_maximalAtlas he hs)

Result:
no goals

Proof state:
case intro
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : PartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
⊢ e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ (PartialHomeomorph.refl H).subtypeRestr this ∈ maximalAtlas (↥s) G

Tactic:
rw [PartialHomeomorph.subtypeRestr_def, PartialHomeomorph.trans_refl]

Result:
case intro
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : PartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : PartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
⊢ e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ t.partialHomeomorphSubtypeCoe this ∈ maximalAtlas (↥s) G