-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem _root_.PartialHomeomorph.isLocalStructomorphWithinAt_iff {G : StructureGroupoid H}
    [ClosedUnderRestriction G] (f : PartialHomeomorph H H) {s : Set H} {x : H}
    (hx : x ∈ f.source ∪ sᶜ) :
    G.IsLocalStructomorphWithinAt (⇑f) s x ↔
      x ∈ s → ∃ e : PartialHomeomorph H H,
      e ∈ G ∧ e.source ⊆ f.source ∧ EqOn f (⇑e) (s ∩ e.source) ∧ x ∈ e.source

Proof state:
case mp
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : PartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
obtain ⟨e, he, hfe, hxe⟩ := hf h2x

Result:
case mp.intro.intro.intro
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : PartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : PartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source

Proof state:
case mp.intro.intro.intro
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : PartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : PartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
refine ⟨e.restr f.source, closedUnderRestriction' he f.open_source, ?_, ?_, hxe, ?_⟩

Result:
case mp.intro.intro.intro.refine_1
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : PartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : PartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ (e.restr f.source).source ⊆ f.source

case mp.intro.intro.intro.refine_2
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : PartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : PartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ EqOn (↑f) (↑(e.restr f.source)) (s ∩ (e.restr f.source).source)

case mp.intro.intro.intro.refine_3
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : PartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
e : PartialHomeomorph H H
he : e ∈ G
hfe : EqOn (↑f) (↑e.toPartialEquiv) (s ∩ e.source)
hxe : x ∈ e.source
⊢ x ∈ interior f.source

Proof state:
case mp
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : PartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
⊢ G.IsLocalStructomorphWithinAt (↑f) s x →
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
intro hf h2x

Result:
case mp
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : PartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
hf : G.IsLocalStructomorphWithinAt (↑f) s x
h2x : x ∈ s
⊢ ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source