-- Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean
/-- The **Schwartz-Zippel lemma**

For a nonzero multivariable polynomial `p` over an integral domain, the probability that `p`
evaluates to zero at points drawn at random from a product of finite subsets `S i` of the integral
domain is bounded by the supremum of `∑ i, degᵢ s / #(S i)` ranging over monomials `s` of `p`. -/
lemma schwartz_zippel_sup_sum :
    ∀ {n} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0) (S : Fin n → Finset R),
      #{x ∈ S ^^ n | eval x p = 0} / ∏ i, (#(S i) : ℚ≥0) ≤
        p.support.sup fun s ↦ ∑ i, (s i / #(S i) : ℚ≥0)
  | 0, p, hp, S => by
    -- Because `p` is a polynomial over zero variables, it is constant.
    rw [p.eq_C_of_isEmpty] at *
    simp [C_ne_zero.mp hp]
    -- Now, assume that the theorem holds for all polynomials in `n` variables.
  | n + 1, p, hp, S => by
    -- We can consider `p` to be a polynomial over multivariable polynomials in one fewer variables.
    set p' : Polynomial (MvPolynomial (Fin n) R) := finSuccEquiv R n p with hp'
    -- Since `p` is not identically zero, there is some `k` such that `pₖ` is not identically zero.
    -- WLOG `k` is the largest such.
    set k := p'.natDegree with hk
    set pₖ := p'.leadingCoeff with hpₖ
    have hp'₀ : p' ≠ 0 := EmbeddingLike.map_ne_zero_iff.2 hp
    have hpₖ₀ : pₖ ≠ 0

Proof state:
case calc_1.h₂.hab.h.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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) p
hp' : p' = (finSuccEquiv R n) 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
xₜ : Fin n → R
hxₜ : xₜ ∈ filter (fun xₜ => (eval xₜ) pₖ ≠ 0) (piFinset fun i => tail S i)
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
⊢ #(filter (fun x₀ => (eval (Fin.cons x₀ xₜ)) p = 0) (S 0)) ≤ degreeOf 0 p

Tactic:
have hpₓdeg : pₓ.natDegree = k := by
  rw [hpₓ, hk, Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ (mem_filter.1 hxₜ).2]

Result:
case calc_1.h₂.hab.h.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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) p
hp' : p' = (finSuccEquiv R n) 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
xₜ : Fin n → R
hxₜ : xₜ ∈ filter (fun xₜ => (eval xₜ) pₖ ≠ 0) (piFinset fun i => tail S i)
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
⊢ #(filter (fun x₀ => (eval (Fin.cons x₀ xₜ)) p = 0) (S 0)) ≤ degreeOf 0 p

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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) p
hp' : p' = (finSuccEquiv R n) 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
⊢ #((filter (fun r => (eval r) pₖ ≠ 0) (piFinset (tail S))).biUnion fun a =>
        filter ((fun x => (eval x) p = 0) ∘ ⇑(consEquiv fun i => R).toEmbedding) (image (fun a_1 => (a_1, a)) (S 0))) =
    #((filter (fun xₜ => (eval xₜ) pₖ ≠ 0) (piFinset fun i => tail S i)).biUnion fun xₜ =>
        image (fun x₀ => (x₀, xₜ)) (filter (fun x₀ => (eval (Fin.cons x₀ xₜ)) p = 0) (S 0)))

Tactic:
simp [Function.comp_def, filter_image, filter_filter]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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) p
hp' : p' = (finSuccEquiv R n) 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
⊢ #((filter (fun r => ¬(eval r) pₖ = 0) (piFinset (tail S))).biUnion fun a =>
        image (fun a_1 => (a_1, a)) (filter (fun a_1 => (eval ((consEquiv fun i => R) (a_1, a))) p = 0) (S 0))) =
    #((filter (fun xₜ => ¬(eval xₜ) pₖ = 0) (piFinset fun i => tail S i)).biUnion fun xₜ =>
        image (fun x₀ => (x₀, xₜ)) (filter (fun x₀ => (eval (Fin.cons x₀ xₜ)) p = 0) (S 0)))

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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) p
hp' : p' = (finSuccEquiv R n) 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
⊢ ↑(#(filter (fun x => (eval x) p = 0) (piFinset fun i => S i))) / ∏ i : Fin (n + 1), ↑(#(S i)) =
    ↑(#(filter (fun x => (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0) (piFinset fun i => S i))) /
        ∏ i : Fin (n + 1), ↑(#(S i)) +
      ↑(#(filter (fun x => (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0) (piFinset fun i => S i))) /
        ∏ i : Fin (n + 1), ↑(#(S i))

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

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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) p
hp' : p' = (finSuccEquiv R n) 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
⊢ ↑(#(filter (fun x => (eval x) p = 0) (piFinset fun i => S i))) / ∏ i : Fin (n + 1), ↑(#(S i)) =
    ↑(#(filter (fun x => (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0 ∨ (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0)
              (piFinset fun i => S i)) +
          #(filter (fun a => ((eval a) p = 0 ∧ (eval (tail a)) pₖ = 0) ∧ (eval a) p = 0 ∧ (eval (tail a)) pₖ ≠ 0)
              (piFinset fun i => S i))) /
      ∏ i : Fin (n + 1), ↑(#(S i))

Proof state:
case calc_1.h₂
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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) p
hp' : p' = (finSuccEquiv R n) 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
⊢ ↑(#(filter (fun x => (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0) (piFinset fun i => S i))) /
      ∏ i : Fin (n + 1), ↑(#(S i)) ≤
    ↑(degreeOf 0 p) / ↑(#(S 0))

Tactic:
calc
  #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ ≠ 0} / ∏ i, (#(S i) : ℚ≥0)
    ≤ ↑(p.degreeOf 0 * ∏ i, #(S (.succ i))) / ∏ i, (#(S i) : ℚ≥0) := ?_
  _ = p.degreeOf 0 * (∏ i, #(S (.succ i))) / (#(S 0) * ∏ i, #(S (.succ i))) := by
    norm_cast; rw [prod_univ_succ]
  _ ≤ (p.degreeOf 0 / #(S 0) : ℚ≥0) := mul_div_mul_right_le (by positivity)

Result:
case calc_1.h₂
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : 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) p
hp' : p' = (finSuccEquiv R n) 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
⊢ ↑(#(filter (fun x => (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0) (piFinset fun i => S i))) /
      ∏ i : Fin (n + 1), ↑(#(S i)) ≤
    ↑(degreeOf 0 p * ∏ i : Fin n, #(S i.succ)) / ∏ i : Fin (n + 1), ↑(#(S i))