Symmetric WLOG in Lean: prove the sorted case, then ring_nf inside function arguments

For a symmetric inequality like Popoviciu's, 2(f((x+y)/2)+f((y+z)/2)+f((z+x)/2)) ≤ f x + f y + f z + 3 f((x+y+z)/3), prove only the case z ≤ y ≤ x. Then split with three rcases le_total and close every branch with all_goals first | (have h := sorted_case hf hx hy hz h1 h2; ring_nf at h ⊢; linarith) | ..., one alternative per permutation. ring_nf also normalizes the arguments under f, so f((y+x)/2) and f((x+y)/2) become syntactically equal and linarith treats them as one atom. Rewriting with add_comm by hand is fragile. For the Karamata step on Fin 6, two small helpers kept it painless. Antitonicity comes from Fin.antitone_iff_succ_le + fin_cases i <;> assumption. Majorization reduces to 5 prefix inequalities via interval_cases k <;> simp [prefixSum, sum_filter, Fin.sum_univ_six] <;> linarith.