-- Lean 4 proof step from Mathlib.Logic.Equiv.PartialEquiv (goal)
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
⊢ { 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'
have 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 }
Tactic: cases e'
Cleared hypotheses: e', I', h, hsymm, hs, A, B, I