Enumeration that respects a function

Stream: Is there code for X?

[Peter Nelson]

Is there an easy way to do this?

import Mathlib.Data.Set.Finite

/- For every function `r` from an infinite type `α` to `ℕ` with finite fibers,
  there is an enumeration of `α` with respect to which `r` is monotone. -/
theorem foo {α : Type*} [Infinite α] (r : α → ℕ) (hr : ∀ i, (r ⁻¹' {i}).Finite) :
    ∃ (e : ℕ ≃ α), Monotone (r ∘ e) := by
  sorry

It maybe should follow from stuff related to WellOrderExtension, but as far as I can see, a few pieces of the API are missing.