-- 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
calc_1 :
  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} (α := 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) ∧
                  Ne (α := 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)) +
      HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(#(S 0)) : ℚ≥0)
calc_2 :
  (pₖ.support.sup fun (s : Fin n →₀ ℕ) ↦
        ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#(S i.succ)) : ℚ≥0)) +
      HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(#(S 0)) : ℚ≥0) ≤
    p.support.sup fun (s : Fin (n + 1) →₀ ℕ) ↦
      ∑ i : Fin (n + 1), HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin (n + 1)) → ℕ) i) : ℚ≥0) (↑(#(S i)) : ℚ≥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)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0)) ≤
    p.support.sup fun (s : Fin (n + 1) →₀ ℕ) ↦
      ∑ i : Fin (n + 1), HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin (n + 1)) → ℕ) i) : ℚ≥0) (↑(#(S i)) : ℚ≥0)

Tactic:
calc
      -- We split the set of possible zeros into a union of two cases.
      #{x ∈ S ^^ (n + 1) | eval x p = 0} / ∏ i, (#(S i) : ℚ≥0)
          -- In the first case, `pₖ` evaluates to `0`.
        = #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0)
          -- In the second case, `pₖ` does not evaluate to `0`.
          + #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ ≠ 0} / ∏ i, (#(S i) : ℚ≥0) := by
        rw [← add_div, ← Nat.cast_add, ← card_union_add_card_inter, filter_union_right,
          ← filter_and]
        simp [← and_or_left, em, and_and_and_comm]
      _ ≤ (pₖ.support.sup fun s ↦ ∑ i, (s i / #(S i.succ) : ℚ≥0)) + p.degreeOf 0 / #(S 0) := ?_
      _ ≤ p.support.sup fun s ↦ ∑ i, (s i / #(S i) : ℚ≥0) := ?_

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