-- 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
xₜ : Fin n → R
hxₜ :
  Membership.mem (γ := Finset (Fin n → R))
    ({xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i |
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})
    xₜ
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
hpₓ₀ : pₓ ≠ 0
rwa :
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
    (support.{u_1, 0} (R := R)
      (Polynomial.coeff
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p) k))
    ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
      (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p'.leadingCoeff))
rwa₁ :
  Ne.{u_1 + 1} (α := R)
    (coeff (σ := Fin n)
      ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
        (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p'.leadingCoeff))
      (Polynomial.coeff
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p) k))
    0
rwa₂ :
  coeff
      ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
        (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p'.leadingCoeff))
      (p'.coeff k) ≠
    0
rwa₃ :
  coeff
      ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
        (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p'.leadingCoeff))
      (p'.coeff p'.natDegree) ≠
    0
rwa₄ :
  coeff
      ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
        (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p'.leadingCoeff))
      p'.leadingCoeff ≠
    0
rwa₅ :
  coeff
      ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
        (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) pₖ))
      pₖ ≠
    0
rwa₆ : AddMonoidAlgebra.leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) pₖ ≠ 0
rwa₇ rwa₈ rwa₉ rwa₁₀ : pₖ ≠ 0
⊢ Finsupp.cons k
      ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
        (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p'.leadingCoeff)) ∈
    p.support

Tactic:
rwa [← mem_support_coeff_finSuccEquiv, mem_support_iff, ← hp', hk,
                ← Polynomial.leadingCoeff, ← hpₖ, ← leadingCoeff_toLex,
                AddMonoidAlgebra.leadingCoeff_ne_zero toLex.injective]

Premises used: AddMonoidAlgebra.leadingCoeff_ne_zero, MvPolynomial.mem_support_iff, Polynomial.leadingCoeff, MvPolynomial.mem_support_coeff_finSuccEquiv, Equiv.injective, MvPolynomial.leadingCoeff_toLex, toLex