Prob schwartz zippel mv polynomial

lemma prob_schwartz_zippel_mv_polynomial {R : Type} [CommRing R] [IsDomain R] [Fintype R]    {n : ℕ}    (P : MvPolynomial (Fin n) R) (h_nonzero : P ≠ 0) (h_deg : P.totalDegree ≤ n) :    Pr_{ let r ←$ᵖ (Fin n → R) }[ MvPolynomial.eval r P = 0 ] ≤      (n : ℝ≥0) / (Fintype.card R : ℝ≥0) := by  classical  rw [prob_uniform_eq_card_filter_div_card]  push_cast  have sz_bound := MvPolynomial.schwartz_zippel_totalDegree (R := R) (n := n)    (p := P) (hp := h_nonzero) (S := Finset.univ)  simp only [Fintype.piFinset_univ, card_univ] at sz_bound  have sz_bound_le_n_div_card_R : ((#{f | (MvPolynomial.eval f) P = 0}) : ℚ≥0)    / ((Fintype.card R ^ n)) ≤ (n : ℚ≥0) / ((#(Finset.univ : Finset R)) : ℚ≥0) := by    calc      _ ≤ (P.totalDegree : ℚ≥0) / ((#(Finset.univ : Finset R)) : ℚ≥0) := sz_bound      _ ≤ _ := by        simp only [card_univ]        apply div_le_of_le_mul₀ (hb := by simp only [zero_le]) (hc := by simp only [zero_le])        -- ⊢ ↑P.totalDegree ≤ ↑n / ↑(Fintype.card R) * ↑(Fintype.card R)        rw [div_mul_cancel₀ (h := by simp only [ne_eq, Nat.cast_eq_zero, Fintype.card_ne_zero,          not_false_eq_true])]        exact Nat.cast_le.mpr h_deg  have sz_bound_ENNReal : ((#{f | (MvPolynomial.eval f) P = 0}) : ENNReal)    / ((Fintype.card R ^ n) : ℕ) ≤ (n : ENNReal) / (Fintype.card R : ENNReal) := by    simp_rw [ENNReal.coe_Nat_coe_NNRat]    conv_lhs => rw [ENNReal.coe_div_of_NNRat (hb := by      simp only [Nat.cast_pow, ne_eq, pow_eq_zero_iff', Nat.cast_eq_zero, Fintype.card_ne_zero,        false_and, not_false_eq_true])]    conv_rhs => rw [ENNReal.coe_div_of_NNRat (hb := by simp only [ne_eq, Nat.cast_eq_zero,      Fintype.card_ne_zero, not_false_eq_true])]    rw [ENNReal.coe_le_of_NNRat]    simp only [Nat.cast_pow]    exact sz_bound_le_n_div_card_R  simp only [Fintype.card_pi, prod_const, card_univ, Fintype.card_fin, Nat.cast_pow, ge_iff_le]  rw [Nat.cast_pow] at sz_bound_ENNReal  exact sz_bound_ENNReal