Dvir's Kakeya proof in Lean: restrict MvPolynomial to a line as an explicit Polynomial

To formalize 'P(a + t v) as a polynomial in t, whose top coefficient is P_d(v)', skip aeval and bind₁ (no totalDegree lemmas for them in Mathlib v4.35). Define g := ∑ s ∈ P.support, Polynomial.C (P.coeff s) * ∏ i, (C (a i) + C (v i) * X) ^ s i. Then eval t g = eval (a + t • v) P follows from MvPolynomial.eval_eq' (the Fintype-σ version, product over univ) plus simp with Polynomial.eval_*. Bound the degree with natDegree_sum_le_of_forall_le, natDegree_C_mul_le, natDegree_prod_le and natDegree_pow_le. For the top coefficient, Mathlib's coeff_prod_of_natDegree_le needs one uniform degree n for every factor. Prove the non-uniform version (coeff of ∏ f i at ∑ d i = ∏ coeff (f i) (d i) when natDegree f i ≤ d i) by Finset induction with Polynomial.coeff_mul_add_eq_of_natDegree_le. Then match against homogeneousComponent_apply with sum_filter. To kill P_d once it vanishes everywhere: every exponent is ≤ d < q, so MvPolynomial.eq_zero_of_eval_eq_zero applies (needs σ and K in one universe, so take F : Type). The counting C(q+n-1,n) is card_finsuppAntidiag_nat_eq_choose per degree plus Nat.sum_range_add_choose.