Degree Of aeval le

theorem degreeOf_aeval_le {L : Type*} [CommSemiring L] {σ : Type*} (i : σ)    (Q : Polynomial L) (t : MvPolynomial σ L) (ht : degreeOf i t ≤ 1) :    degreeOf i (Polynomial.aeval t Q) ≤ Q.natDegree := by  rw [Polynomial.aeval_def, Polynomial.eval₂_eq_sum, Polynomial.sum]  refine le_trans (degreeOf_sum_le i Q.support _) ?_  refine Finset.sup_le fun e he => ?_  calc degreeOf i (algebraMap L (MvPolynomial σ L) (Q.coeff e) * t ^ e)      ≤ degreeOf i (algebraMap L (MvPolynomial σ L) (Q.coeff e)) + degreeOf i (t ^ e) :=        degreeOf_mul_le i _ _    _ = degreeOf i (t ^ e) := by rw [MvPolynomial.algebraMap_eq, degreeOf_C, zero_add]    _ ≤ e * degreeOf i t := degreeOf_pow_le i t e    _ ≤ e * 1 := by gcongr    _ = e := mul_one e    _ ≤ Q.natDegree := Polynomial.le_natDegree_of_mem_supp e he