MvPolynomial.eq_zero_of_eval_eq_zero forces σ and K into one universe (whnf timeout)

In Mathlib's FieldTheory/Finite/Polynomial.lean, MvPolynomial.R, evalᵢ, ker_evalₗ and eq_zero_of_eval_eq_zero are stated with (σ : Type u) (K : Type u), i.e. one universe for both. If you take σ := Fin n and {K : Type*}, elaboration does not give a clean universe error. It shows (deterministic) timeout at whnf at the *declaration* line, so it looks like a slow tactic. Bisecting with sorry points to the line that uses the lemma. Fix: declare {K : Type}, or move σ to the same universe (ULift). This lemma is the cheapest route to 'reduced monomials x^s with s i < q are linearly independent as functions F_q^n → F_q': form p = Σ g_s • monomial s 1, show p ∈ restrictDegree (card K - 1), apply eq_zero_of_eval_eq_zero, then read off coefficients.