Dvd eval of root Multiplicity zero

lemma dvd_eval_of_rootMultiplicity_zero (Q : F[X][Y]) (P : F[X]) (m : ℕ)    (hQ : ∀ i j, i + j < m → Bivariate.coeff Q i j = 0) (hP : P.coeff 0 = 0) :    X ^ m ∣ Q.eval P := by  have h_div_Pj : ∀ j : ℕ, X ^ j ∣ P ^ j := fun j ↦ pow_dvd_pow_of_dvd (X_dvd_iff.mpr hP) j  have h_div_term_all : ∀ i j : ℕ, (Q.coeff j).coeff i ≠ 0 →      X ^ m ∣ Polynomial.monomial i ((Q.coeff j).coeff i) * P ^ j := by    intros i j hij    have h_div_term : X ^ (i + j) ∣ Polynomial.monomial i ((Q.coeff j).coeff i) * P ^ j := by      simp only [pow_add]      exact mul_dvd_mul (by simp [← C_mul_X_pow_eq_monomial]) (h_div_Pj j)    exact dvd_trans (pow_dvd_pow _ (Nat.le_of_not_lt fun h ↦ hij <| by solve_by_elim)) h_div_term  simp only [eval_eq_sum, sum_def]  refine Finset.dvd_sum fun n hn ↦ ?_  rw [(Q.coeff n).as_sum_range_C_mul_X_pow]  simp only [Finset.sum_mul, C_mul_X_pow_eq_monomial]  classical  exact Finset.dvd_sum fun i hi ↦    if hi0 : (Q.coeff n).coeff i = 0 then by simp [hi0]    else h_div_term_all i n hi0