Exists permutation, which makes the function monotone

Stream: general

[Mantas Baksys]

I'm pretty sure we don't have the following lemma (or smth similar) and I am not too sure where to start.

import order.monotone
import data.finset.basic

lemma exists_perm_comp_monotone_on  {ι α : Type*} [preorder ι] [linear_order α] {f : ι → α} (s : finset ι) :
  ∃ σ : equiv.perm ι, {x | σ x ≠ x} ⊆ s ∧ monotone_on (f ∘ σ) s :=
begin
  sorry
end

My first thought was to use finset.sort in some way but I can't currently see how. Thanks for the help!

[Yaël Dillies]

Just noting that there is a more general version using docs#monovary and that the proof of the above should translate directly to a proof of the monovary version.

[Patrick Massot]

I don't think you should use finset.sort. I would do an induction on s

[Patrick Massot]

I mean starting with

  classical,
  apply s.induction_on,

[Eric Wieser]

I think there is probably a short and constructive way to get what you want here using docs#finset.sort

[Eric Wieser]

Not to say that it's easier than induction!

[David Wärn]

Here's a similar result proved using docs#mono_equiv_of_fin: https://github.com/leanprover-community/mathlib/blob/deuber/src/combinatorics/to_mathlib.lean#L15-L40. I'm still not sure about the best way to phrase the lemma

[Yaël Dillies]

David, if you have other statements in mind, do you think we should change the statement of docs#monovary_on.sum_smul_comp_perm_le_sum_smul?