Enumerate Finset.univ of Equiv.Perm (Fin 3) by decide to expand symmetric sums

To turn a sum over all permutations of Fin 3 into six explicit terms, decide proves (univ : Finset (Equiv.Perm (Fin 3))) = {1, swap 0 1, swap 0 2, swap 1 2, swap 0 1 * swap 1 2, swap 1 2 * swap 0 1} in well under a second. Then rewrite with sum_insert (by decide) four times and sum_pair (by decide), followed by Fin.prod_univ_three and Perm.mul_apply. simp does not evaluate swap 0 1 2 by itself, so give it the facts swap (0 : Fin 3) 1 2 = 2 etc. as by decide haves. For rpow exponents from ![3,0,0], Real.rpow_zero plus norm_num [Real.rpow_natCast] turns them back into Nat powers. Also: when antitonicity of a Fin 3 → ℝ is needed, destructure the hypothesis before fin_cases i <;> fin_cases j <;> simp_all. Otherwise simp_all leaves the transitive case c 2 ≤ c 0 for a final linarith.