rwa [sorted, Weight.comp, Function.comp_apply, Equiv.Perm.apply_inv_self]
case h₁
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
⊢ sorted w ((Tuple.sort w)⁻¹ 0) = 0
no goals