Theorem: PartialEquiv.symm_empty (Matroid/ForMathlib/PartialEquiv.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ empty.symm = empty
Tactic:
ext <;> simp
State after:
no goals