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

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ φ.symm ≤ φ'.symm
Tactic:
simpa using symm_le_symm_of_le h
State after:
no goals