-- Mathlib/Topology/PartialHomeomorph.lean
theorem subtypeRestr_symm_eqOn {U : Opens X} (hU : Nonempty U) :
    EqOn e.symm (Subtype.val ∘ (e.subtypeRestr hU).symm) (e.subtypeRestr hU).target

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ ↑e ((Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y) = y

Tactic:
change restrict _ e _ = _

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (↑U).restrict (↑e) (↑(e.subtypeRestr hU).symm y) = y

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source

Tactic:
have := map_target _ hy

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
this : ↑(e.subtypeRestr hU).symm y ∈ (e.subtypeRestr hU).source
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (↑U).restrict (↑e) (↑(e.subtypeRestr hU).symm y) = y

Tactic:
rw [← subtypeRestr_coe, (e.subtypeRestr hU).right_inv hy]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
this : ↑(e.subtypeRestr hU).symm y ∈ (e.subtypeRestr hU).source
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source

Tactic:
rwa [subtypeRestr_source] at this

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ ↑e.symm y = (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y

Tactic:
rw [eq_comm, eq_symm_apply _ _ hy.1]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ ↑e ((Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y) = y

X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y ∈ e.source

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
⊢ EqOn (↑e.symm) (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target

Tactic:
intro y hy

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U : Opens X
hU : Nonempty ↥U
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ ↑e.symm y = (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) y