case mk
α : Type u
β : Type v
γ : Type w
δ : Type x
toFun✝ : α → Option β
invFun✝ : β → Option α
inv✝ : ∀ (a : α) (b : β), a ∈ invFun✝ b ↔ b ∈ toFun✝ a
⊢ PEquiv.symm (PEquiv.symm { toFun := toFun✝, invFun := invFun✝, inv := inv✝ }) =
    { toFun := toFun✝, invFun := invFun✝, inv := inv✝ }
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.symm (PEquiv.symm f) = f
cases f
no goals
case mk
α : Type u
β : Type v
γ : Type w
δ : Type x
toFun✝ : α → Option β
invFun✝ : β → Option α
inv✝ : ∀ (a : α) (b : β), a ∈ invFun✝ b ↔ b ∈ toFun✝ a
⊢ PEquiv.symm (PEquiv.symm { toFun := toFun✝, invFun := invFun✝, inv := inv✝ }) =
    { toFun := toFun✝, invFun := invFun✝, inv := inv✝ }
rfl