-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem ext {e e' : PartialEquiv α β} (h : ∀ x, e x = e' x)
    (hsymm : ∀ x, e.symm x = e'.symm x) (hs : e.source = e'.source) : e = e'

Proof state:
case mk
α : Type u_1
β : Type u_2
e' : PartialEquiv α β
I' : ↑e' '' e'.source = e'.target
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
h :
  ∀ (x : α),
    ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
        x =
      ↑e' x
hsymm :
  ∀ (x : β),
    ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm
        x =
      ↑e'.symm x
hs :
  { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source =
    e'.source
A :
  ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ } =
    ↑e'
B :
  ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm =
    ↑e'.symm
I :
  e'.target =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target
⊢ { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
      map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ } =
    e'

Tactic:
cases e'

Result:
case mk.mk
α : Type u_1
β : Type u_2
toFun✝¹ : α → β
invFun✝¹ : β → α
source✝¹ : Set α
target✝¹ : Set β
map_source'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → toFun✝¹ x ∈ target✝¹
map_target'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → invFun✝¹ x ∈ source✝¹
left_inv'✝¹ : ∀ ⦃x : α⦄, x ∈ source✝¹ → invFun✝¹ (toFun✝¹ x) = x
right_inv'✝¹ : ∀ ⦃x : β⦄, x ∈ target✝¹ → toFun✝¹ (invFun✝¹ x) = x
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
I' :
  ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ } ''
      { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target
h :
  ∀ (x : α),
    ↑{ toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
            map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }
        x =
      ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
        x
hsymm :
  ∀ (x : β),
    ↑{ toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
              map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }.symm
        x =
      ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm
        x
hs :
  { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
        map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }.source =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source
A :
  ↑{ toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
        map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ } =
    ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
B :
  ↑{ toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
          map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }.symm =
    ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm
I :
  { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target =
    { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
        map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ }.target
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, source := source✝¹, target := target✝¹, map_source' := map_source'✝¹,
      map_target' := map_target'✝¹, left_inv' := left_inv'✝¹, right_inv' := right_inv'✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
      map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
⊢ e = e'

Tactic:
have B : (e.symm : β → α) = e'.symm := by
  ext x
  exact hsymm x

Result:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑e.symm = ↑e'.symm
⊢ e = e'

Proof state:
case h
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
x : β
⊢ ↑e.symm x = ↑e'.symm x

Tactic:
exact hsymm x

Result:
no goals