n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ f ∘ ↑(σ * sort (f ∘ ↑σ)) = f ∘ ↑(sort f)
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ (f ∘ ↑σ) ∘ ↑(sort (f ∘ ↑σ)) = f ∘ ↑(sort f)
rw [Function.comp.assoc, ← Equiv.Perm.coe_mul]
no goals
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ f ∘ ↑(σ * sort (f ∘ ↑σ)) = f ∘ ↑(sort f)
exact unique_monotone (monotone_sort (f ∘ σ)) (monotone_sort f)