-- 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
rw :
  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)) =
    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) ∨
                  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)}) +
            Finset.card.{u_1} (α := Fin (n + 1) → R)
              ({a ∈ piFinset (δ := fun (a : Fin (n + 1)) ↦ R) fun (i : Fin (n + 1)) ↦ S i |
                (Eq (α := R) ((eval a : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R) ∧
                    Eq (α := R)
                      ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) a) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
                      (0 : R)) ∧
                  Eq (α := R) ((eval a : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R) ∧
                    Ne (α := R)
                      ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) a) : (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)})) :
        ℚ≥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) ∧
                  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))

Tactic:
rw [← add_div, ← Nat.cast_add, ← card_union_add_card_inter, filter_union_right,
          ← filter_and]

Premises used: Finset.filter_union_right, Finset.card_union_add_card_inter, Nat.cast_add, Finset.filter_and, add_div