-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : 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' : PartialEquiv α β } :
          α → β)
        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' : PartialEquiv α β }.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' : PartialEquiv α β }.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' : PartialEquiv α β } :
      α → β) =
    (↑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' : PartialEquiv α β }.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' : PartialEquiv α β }.target
mk :
  ∀ (toFun_1 : α → β) (invFun_1 : β → α) (source_1 : Set α) (target_1 : Set β)
    (map_source'_1 : ∀ ⦃x : α⦄, x ∈ source_1 → toFun_1 x ∈ target_1)
    (map_target'_1 : ∀ ⦃x : β⦄, x ∈ target_1 → invFun_1 x ∈ source_1)
    (left_inv'_1 : ∀ ⦃x : α⦄, x ∈ source_1 → invFun_1 (toFun_1 x) = x)
    (right_inv'_1 : ∀ ⦃x : β⦄, x ∈ target_1 → toFun_1 (invFun_1 x) = x)
    (I' :
      (↑{ toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := map_source'_1,
                map_target' := map_target'_1, left_inv' := left_inv'_1, right_inv' := right_inv'_1 :
                PartialEquiv α β } :
            α → β) ''
          { toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := map_source'_1,
              map_target' := map_target'_1, left_inv' := left_inv'_1, right_inv' := right_inv'_1 :
              PartialEquiv α β }.source =
        { toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := map_source'_1,
            map_target' := map_target'_1, left_inv' := left_inv'_1, right_inv' := right_inv'_1 :
            PartialEquiv α β }.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' : PartialEquiv α β } :
              α → β)
            x =
          (↑{ toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1,
                  map_source' := map_source'_1, map_target' := map_target'_1, left_inv' := left_inv'_1,
                  right_inv' := right_inv'_1 : PartialEquiv α β } :
              α → β)
            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' :
                    PartialEquiv α β }.symm :
              β → α)
            x =
          (↑{ toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1,
                    map_source' := map_source'_1, map_target' := map_target'_1, left_inv' := left_inv'_1,
                    right_inv' := right_inv'_1 : PartialEquiv α β }.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' : PartialEquiv α β }.source =
        { toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := map_source'_1,
            map_target' := map_target'_1, left_inv' := left_inv'_1, right_inv' := right_inv'_1 :
            PartialEquiv α β }.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' : PartialEquiv α β } :
          α → β) =
        (↑{ toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := map_source'_1,
              map_target' := map_target'_1, left_inv' := left_inv'_1, right_inv' := right_inv'_1 } :
          α → β))
    (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' : PartialEquiv α β }.symm :
          β → α) =
        (↑{ toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := map_source'_1,
                map_target' := map_target'_1, left_inv' := left_inv'_1, right_inv' := right_inv'_1 }.symm :
          β → α))
    (I :
      { toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := map_source'_1,
            map_target' := map_target'_1, left_inv' := left_inv'_1, right_inv' := right_inv'_1 :
            PartialEquiv α β }.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' : PartialEquiv α β }.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' : PartialEquiv α β } =
      { toFun := toFun_1, invFun := invFun_1, source := source_1, target := target_1, map_source' := map_source'_1,
        map_target' := map_target'_1, left_inv' := left_inv'_1, right_inv' := right_inv'_1 }
⊢ { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
      map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β } =
    e'

Tactic:
cases e'