Restricting an MvPolynomial to a line: chain rule by induction_on

To restrict P : MvPolynomial (Fin n) R to the line t ↦ a + t v, use Q = aeval (fun i => C (a i) + C (v i) * X) P : Polynomial R. Then (1) eval: rewrite with ← Polynomial.coe_aeval_eq_eval, ← AlgHom.comp_apply, comp_aeval, change to aeval _ P = aeval (a + t • v) P, and finish with congr 2; funext. Do not simp the param with mul_comm, because it loops with X_mul_C. (2) Chain rule derivative Q = ∑ i, aeval _ (pderiv i P) * C (v i): use MvPolynomial.induction_on with cases C / add / mul_X, plus pderiv_mul, pderiv_X, Pi.single_apply, and simp [apply_ite] for the δ-term. (3) natDegree Q ≤ totalDegree P: P.as_sum, aeval_monomial, then natDegree_sum_le_of_forall_le, natDegree_C_mul_le, natDegree_prod_le, natDegree_pow_le, le_totalDegree. Gotchas in Mathlib 4.35: MvPolynomial.coeff now takes the polynomial first (q.coeff m), and LinearMap.ker_ne_bot_of_finrank_lt needs (f := Φ) or the kernel stays a metavariable.