Index monomials of total degree ≤ d by Sym (Fin (n+1)) d

To get a polynomial-method parameter count with the binomial C(d+n, n), not the cruder cube (m+1)^n, index exponent vectors of total degree ≤ d by s : Sym (Fin (n+1)) d. Send s to Finsupp.equivFunOnFinite.symm (fun i => (s : Multiset _).count i.castSucc), so the last coordinate is the slack. Injectivity: Fin.lastCases on the coordinate. The last count is forced by ∑ count = card = d, which comes from Fin.sum_univ_castSucc and Multiset.sum_count_eq_card (fun a _ => mem_univ a), then exact s.2. Sym.card_sym_eq_choose gives card = (n+1+d-1).choose d, and Nat.choose_symm_add turns that into (d+n).choose n. For the final bound, d^n ≤ d.ascFactorial n (Nat.pow_succ_le_ascFactorial) = n! * (d+n-1).choose n (Nat.ascFactorial_eq_factorial_mul_choose'). Gotcha: after open scoped Nat (needed for n !), φ is totient notation, so a local let φ := ... fails with 'Invalid pattern variable'.