-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem isLocalStructomorphWithinAt_localInvariantProp [ClosedUnderRestriction G] :
    LocalInvariantProp G G (IsLocalStructomorphWithinAt G) :=
  { is_local

Proof state:
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : PartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : ↑e' x ∈ ↑e'.symm ⁻¹' s
⊢ ∃ e ∈ G, EqOn (f ∘ ↑e'.symm) (↑e.toPartialEquiv) (↑e'.symm ⁻¹' s ∩ e.source) ∧ ↑e' x ∈ e.source

Tactic:
have hxs : x ∈ s := by simpa only [e'.left_inv he'x, mfld_simps] using hx

Result:
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : PartialHomeomorph H H
he'G : e' ∈ G
he'x : x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : ↑e' x ∈ ↑e'.symm ⁻¹' s
hxs : x ∈ s
⊢ ∃ e ∈ G, EqOn (f ∘ ↑e'.symm) (↑e.toPartialEquiv) (↑e'.symm ⁻¹' s ∩ e.source) ∧ ↑e' x ∈ e.source

Proof state:
case intro.intro.intro.refine_1
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : PartialHomeomorph H H
he'G : e' ∈ G
a✝ : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : PartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
y : H
hy : y ∈ s ∧ y ∈ e.source ∧ ↑e y ∈ e'.source
⊢ (↑e' ∘ f) y = ↑(e ≫ₕ e').toPartialEquiv y

Tactic:
simp only [hef ⟨hy.1, hy.2.1⟩, mfld_simps]

Result:
no goals

Proof state:
case mp
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv) (s ∩ u ∩ e.source) ∧ x ∈ e.source

Tactic:
rcases h hx.1 with ⟨e, heG, hef, hex⟩

Result:
case mp.intro.intro.intro
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
e : PartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv) (s ∩ u ∩ e.source) ∧ x ∈ e.source

Proof state:
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen u
hux : x ∈ u
⊢ G.IsLocalStructomorphWithinAt f s x ↔ G.IsLocalStructomorphWithinAt f (s ∩ u) x

Tactic:
constructor

Result:
case mp
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen u
hux : x ∈ u
⊢ G.IsLocalStructomorphWithinAt f s x → G.IsLocalStructomorphWithinAt f (s ∩ u) x

case mpr
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen u
hux : x ∈ u
⊢ G.IsLocalStructomorphWithinAt f (s ∩ u) x → G.IsLocalStructomorphWithinAt f s x

Proof state:
case intro.intro.intro
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f g : H → H
hfgs : ∀ y ∈ s, f y = g y
a✝ : f x = g x
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : PartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn g (↑e.toPartialEquiv) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
refine ⟨e, heG, ?_, hex⟩

Result:
case intro.intro.intro
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f g : H → H
hfgs : ∀ y ∈ s, f y = g y
a✝ : f x = g x
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : PartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
⊢ EqOn g (↑e.toPartialEquiv) (s ∩ e.source)

Proof state:
case intro.intro.intro
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : PartialHomeomorph H H
he'G : e' ∈ G
a✝ : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : PartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn (↑e' ∘ f) (↑e.toPartialEquiv) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
refine ⟨e.trans e', G.trans heG he'G, ?_, ?_⟩

Result:
case intro.intro.intro.refine_1
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : PartialHomeomorph H H
he'G : e' ∈ G
a✝ : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : PartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
⊢ EqOn (↑e' ∘ f) (↑(e ≫ₕ e').toPartialEquiv) (s ∩ (e ≫ₕ e').source)

case intro.intro.intro.refine_2
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
f : H → H
e' : PartialHomeomorph H H
he'G : e' ∈ G
a✝ : s ⊆ f ⁻¹' e'.source
hfx : f x ∈ e'.source
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s
e : PartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
⊢ x ∈ (e ≫ₕ e').source