-- Mathlib/Topology/PartialHomeomorph.lean
theorem replaceEquiv_eq_self (e' : PartialEquiv X Y)
    (h : e.toPartialEquiv = e') : e.replaceEquiv e' h = e

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
e' : PartialEquiv X Y
h : e.toPartialEquiv = e'
⊢ e.replaceEquiv e' h = e

Tactic:
cases e

Result:
case mk
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e' toPartialEquiv✝ : PartialEquiv X Y
open_source✝ : IsOpen toPartialEquiv✝.source
open_target✝ : IsOpen toPartialEquiv✝.target
continuousOn_toFun✝ : ContinuousOn (↑toPartialEquiv✝) toPartialEquiv✝.source
continuousOn_invFun✝ : ContinuousOn toPartialEquiv✝.invFun toPartialEquiv✝.target
h :
  { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }.toPartialEquiv =
    e'
⊢ { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
          continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }.replaceEquiv
      e' h =
    { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
      continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }

Proof state:
case mk
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
toPartialEquiv✝ : PartialEquiv X Y
open_source✝ : IsOpen toPartialEquiv✝.source
open_target✝ : IsOpen toPartialEquiv✝.target
continuousOn_toFun✝ : ContinuousOn (↑toPartialEquiv✝) toPartialEquiv✝.source
continuousOn_invFun✝ : ContinuousOn toPartialEquiv✝.invFun toPartialEquiv✝.target
⊢ { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
          continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }.replaceEquiv
      { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
          continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }.toPartialEquiv
      ⋯ =
    { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
      continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }

Tactic:
rfl

Result:
no goals

Proof state:
case mk
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e' toPartialEquiv✝ : PartialEquiv X Y
open_source✝ : IsOpen toPartialEquiv✝.source
open_target✝ : IsOpen toPartialEquiv✝.target
continuousOn_toFun✝ : ContinuousOn (↑toPartialEquiv✝) toPartialEquiv✝.source
continuousOn_invFun✝ : ContinuousOn toPartialEquiv✝.invFun toPartialEquiv✝.target
h :
  { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
        continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }.toPartialEquiv =
    e'
⊢ { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
          continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }.replaceEquiv
      e' h =
    { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
      continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }

Tactic:
subst e'

Result:
case mk
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
toPartialEquiv✝ : PartialEquiv X Y
open_source✝ : IsOpen toPartialEquiv✝.source
open_target✝ : IsOpen toPartialEquiv✝.target
continuousOn_toFun✝ : ContinuousOn (↑toPartialEquiv✝) toPartialEquiv✝.source
continuousOn_invFun✝ : ContinuousOn toPartialEquiv✝.invFun toPartialEquiv✝.target
⊢ { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
          continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }.replaceEquiv
      { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
          continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }.toPartialEquiv
      ⋯ =
    { toPartialEquiv := toPartialEquiv✝, open_source := open_source✝, open_target := open_target✝,
      continuousOn_toFun := continuousOn_toFun✝, continuousOn_invFun := continuousOn_invFun✝ }