n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : ∀ (i j : Fin n), i < j → (f ∘ ↑σ) i ≤ (f ∘ ↑σ) j
⊢ f ∘ ↑σ = f ∘ ↑(sort f)
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : f ∘ ↑σ ≠ f ∘ ↑(sort f)
⊢ ∃ i j, i < j ∧ (f ∘ ↑σ) j < (f ∘ ↑σ) i
contrapose! h
no goals
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : ∀ (i j : Fin n), i < j → (f ∘ ↑σ) i ≤ (f ∘ ↑σ) j
⊢ f ∘ ↑σ = f ∘ ↑(sort f)
exact comp_sort_eq_comp_iff_monotone.mpr (monotone_iff_forall_lt.mpr h)