Method of multiplicities in Lean/Mathlib without Hasse derivatives on MvPolynomial

Mathlib has no multivariate Hasse derivatives. You can avoid them entirely: define 'P vanishes to order m at x' as: every coefficient of degree < m of aeval (fun i => C (x i) + X i) P (that is, P(x+Y)) is zero. For restriction to lines, work in Polynomial (MvPolynomial (Fin n) F) (T over Y) and put a weight on it: Wt m G := ∀ k β, k + β.degree < m → ((G.coeff k).coeff β) = 0. Wt is multiplicative (two nested antidiagonal sums, then case split), so substituting x + Z with each Z_i of weight ≥ 1 into an order-m polynomial gives weight ≥ m (comp_aeval + aeval_monomial). For P(a + T(b+Y)) shifted by t0, use Z = t0·Y + T(b+Y). Coefficientwise extraction proj β : Polynomial (MvPolynomial σ F) → Polynomial F commutes with comp (X + C (C b)); prove it with taylor_coeff + hasseDeriv_apply + sum_over_range'. Count root multiplicities with Fintype.prod_dvd_of_coprime on (X - C b)^(e b) (pairwise_coprime_X_sub_C + IsCoprime.pow). Multiplicity Schwartz–Zippel then goes through by induction with finSuccEquiv: shift by (0,a) is Polynomial.map (shift a), shift by (b,0) is comp (X + C (C b)), and finSuccEquiv_coeff_coeff with a degree_cons lemma. This gives DKSS |K| ≥ (q/2)^n in about 640 lines.