-- Mathlib/Topology/PartialHomeomorph.lean
theorem subtypeRestr_symm_eqOn_of_le {U V : Opens X} (hU : Nonempty U) (hV : Nonempty V)
    (hUV : U ≤ V) : EqOn (e.subtypeRestr hV).symm (Set.inclusion hUV ∘ (e.subtypeRestr hU).symm)
      (e.subtypeRestr hU).target

Proof state:
case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y) ∈ (V.partialHomeomorphSubtypeCoe hV).symm.target

Tactic:
apply PartialHomeomorph.map_source

Result:
case refine_1.h
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target
⊢ ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).symm.source

Proof state:
case refine_1.h
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target
⊢ ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target

Tactic:
exact hyV

Result:
no goals

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

Tactic:
set i := Set.inclusion hUV

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
⊢ EqOn (↑(e.subtypeRestr hV).symm) (i ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target

Proof state:
case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y) ∈ (V.partialHomeomorphSubtypeCoe hV).source

Tactic:
rw [← PartialHomeomorph.symm_target]

Result:
case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y) ∈ (V.partialHomeomorphSubtypeCoe hV).symm.target

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y) = i (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y))

Tactic:
refine (V.partialHomeomorphSubtypeCoe hV).injOn ?_ trivial ?_

Result:
case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y) ∈ (V.partialHomeomorphSubtypeCoe hV).source

case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.partialHomeomorphSubtypeCoe hV) (↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y)) =
    ↑(V.partialHomeomorphSubtypeCoe hV) (i (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))