-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) :=
  (finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p
hp' : p' = (finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
S₁ :
  HDiv.hDiv (α := ℚ≥0)
      (↑(Finset.card.{u_1} (α := Fin (n + 1) → R)
            ({x ∈ piFinset (δ := fun (a : Fin (n + 1)) ↦ R) fun (i : Fin (n + 1)) ↦ S i |
              Eq (α := R) ((eval x : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R) ∧
                Eq (α := R) ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) x) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
                  (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0)) ≤
    HDiv.hDiv (α := ℚ≥0)
      (↑(Finset.card.{u_1} (α := (i : Fin (n + 1)) → R)
            ({x ∈ piFinset (δ := fun (i : Fin (n + 1)) ↦ R) fun (i : Fin (n + 1)) ↦ S i |
              Eq (α := R) ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) x) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
                (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0))
S₂ :
  HDiv.hDiv (α := ℚ≥0)
      (↑(Finset.card.{u_1} (α := (i : Fin (n + 1)) → R)
            ({x ∈ piFinset (δ := fun (i : Fin (n + 1)) ↦ R) fun (i : Fin (n + 1)) ↦ S i |
              Eq (α := R) ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) x) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
                (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0)) =
    HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0)
        (↑(Finset.card.{u_1} (α := Fin n → R)
              ({xₜ ∈
                  piFinset (δ := fun (a : Fin n) ↦ R) fun (i : Fin n) ↦
                    tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i |
                Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})) :
          ℚ≥0) /
      HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0) (∏ i : Fin n, (↑(#(S i.succ)) : ℚ≥0))
⊢ HDiv.hDiv (α := ℚ≥0)
      (↑(Finset.card.{u_1} (α := Fin (n + 1) → R)
            ({x ∈ piFinset (δ := fun (a : Fin (n + 1)) ↦ R) fun (i : Fin (n + 1)) ↦ S i |
              Eq (α := R) ((eval x : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R) ∧
                Eq (α := R) ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) x) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
                  (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0)) ≤
    pₖ.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#(S i.succ)) : ℚ≥0)

Tactic:
calc
          #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0)
            ≤ #{x ∈ S ^^ (n + 1) | eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0) := by
            gcongr with x; exact And.right
          _ = #(S 0) * #{xₜ ∈ tail S ^^ n | eval xₜ pₖ = 0}
              / (#(S 0) * (∏ i, #(S (.succ i)) : ℚ≥0)) := by
            rw [card_consEquiv_filter_piFinset S fun x ↦ eval x pₖ = 0, prod_univ_succ, tail_def]
            norm_cast
          _ ≤ #{xₜ ∈ tail S ^^ n | eval xₜ pₖ = 0} / ∏ i, (#(S (.succ i)) : ℚ≥0) :=
            mul_div_mul_left_le (by positivity)
          _ ≤ (pₖ.support.sup fun s ↦ ∑ i, (s i / #(S (.succ i)) : ℚ≥0)) :=
            schwartz_zippel_sup_sum hpₖ₀ _

Premises used: HMul.hMul, Finset.univ, Fin.succ, mul_div_mul_left_le, HDiv.hDiv, Nat.cast, MvPolynomial.support, Finset.prod, HAdd.hAdd, Finset.card, Finset.sup, OfNat.ofNat, Fin.tail, DFunLike.coe, Finset.sum