no goals
α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
⊢ PEquiv.symm (PEquiv.trans (PEquiv.symm f) f) = PEquiv.symm (ofSet {b | isSome (↑(PEquiv.symm f) b) = true})
simp [symm_trans_rev, self_trans_symm, -symm_symm]