exists re-ordering of coordinates to make monotone?

Stream: Is there code for X?

[David Renshaw]

I'm struggling to find a nice way to prove this:

import Mathlib.Tactic

lemma can_sort (n : ℕ) (a : Fin n → ℤ) :
    ∃ p : Fin n ↪ Fin n,
        ∀ i j, i ≤ j → a (p i) ≤ a (p j) := by
  sorry

[Michael Stoll]

docs#Tuple.sort (and API)?

[David Renshaw]

nice!

[David Renshaw]

This works:

lemma can_sort (n : ℕ) (a : Fin n → ℤ) :
    ∃ p : Fin n ↪ Fin n,
        ∀ i j, i ≤ j → a (p i) ≤ a (p j) :=
  ⟨Tuple.sort a, fun _ _ hij ↦ Tuple.monotone_sort a hij⟩

[David Renshaw]

... and suggests that perhaps I should be reformulating my problem to use Equiv.Perm instead of Function.Embedding