-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : 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_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:
simp_all