Theorem Order.le_lift_cof_iff

feat: `cof α = cof β` given a strictly monotonic function `f : α → β` with cofinal range (#36703) …