-- 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:
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
⊢ ↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y) = i (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y))

Tactic:
have hyV : e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target := by
  rw [Opens.partialHomeomorphSubtypeCoe_target] at hy ⊢
  exact hUV hy.2

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
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))

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.subtypeRestr hU).target
⊢ ↑(e.subtypeRestr hV).symm y = (i ∘ ↑(e.subtypeRestr hU).symm) y

Tactic:
dsimp [PartialHomeomorph.subtypeRestr_def] at hy ⊢

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
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target
⊢ ↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y) = i (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y))

Proof state:
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
⊢ ↑e.symm y = ↑(V.partialHomeomorphSubtypeCoe hV) (i (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))

Tactic:
show _ = U.partialHomeomorphSubtypeCoe hU _

Result:
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
⊢ ↑e.symm y = ↑(U.partialHomeomorphSubtypeCoe hU) (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y))

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
⊢ ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target

Tactic:
rw [Opens.partialHomeomorphSubtypeCoe_target] at hy ⊢

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
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' ↑U
⊢ ↑e.symm y ∈ ↑V

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).symm.source

Tactic:
rw [PartialHomeomorph.symm_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).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
⊢ EqOn (↑(e.subtypeRestr hV).symm) (i ∘ ↑(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 V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ (e.subtypeRestr hU).target
⊢ ↑(e.subtypeRestr hV).symm y = (i ∘ ↑(e.subtypeRestr hU).symm) y

Proof state:
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)))

Tactic:
rw [(V.partialHomeomorphSubtypeCoe hV).right_inv hyV]

Result:
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
⊢ ↑e.symm y = ↑(V.partialHomeomorphSubtypeCoe hV) (i (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))

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
⊢ ↑e.symm y ∈ ↑V

Tactic:
exact hUV hy.2

Result:
no goals

Proof state:
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
⊢ ↑e.symm y = ↑(U.partialHomeomorphSubtypeCoe hU) (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y))

Tactic:
rw [(U.partialHomeomorphSubtypeCoe hU).right_inv hy.2]

Result:
no goals