awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
⊢ pₓ.natDegree = k

Tactic:
have hpₓdeg : pₓ.natDegree = k := by
          rw [hpₓ, hk, Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ (mem_filter.1 hxₜ).2]
-- 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
h : pₓ = 0
rw : Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) p'.leadingCoeff : R) (0 : R)
rw₁ : Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) (p'.coeff p'.natDegree) : R) (0 : R)
rw₂ : Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) (p'.coeff k) : R) (0 : R)
rw₃ : Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) (p'.coeff pₓ.natDegree) : R) (0 : R)
rw₄ :
  Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) (p'.coeff (Polynomial.natDegree.{u_1} (R := R) 0)) : R)
    (0 : R)
rw₅ : Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) (p'.coeff 0) : R) (0 : R)
rw₆ : (Polynomial.map (eval xₜ) p').coeff 0 = 0
rw₇ : pₓ.coeff 0 = 0
rw₈ : Eq.{u_1 + 1} (α := R) (Polynomial.coeff 0 0) 0
rw₉ rw₁₀ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)

Tactic:
rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]

Premises used: Polynomial.coeff_map, Polynomial.leadingCoeff, Polynomial.natDegree_zero, Polynomial.coeff_zero
-- 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
⊢ pₓ ≠ 0

Tactic:
have hpₓ₀ : pₓ ≠ 0 := fun h ↦ (mem_filter.1 hxₜ).2 <| by
          rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]
-- 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
a :
  {x₀ ∈ S 0 |
      Eq (α := R)
        ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ xₜ) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
        (0 : R)} ⊆
    pₓ.roots.toFinset
⊢ #({x₀ ∈ S 0 |
        Eq (α := R)
          ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ xₜ) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
          (0 : R)}) ≤
    #pₓ.roots.toFinset

Tactic:
gcongr
-- 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
⊢ {x₀ ∈ S 0 |
      Eq (α := R)
        ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ xₜ) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
        (0 : R)} ⊆
    pₓ.roots.toFinset

Tactic:
simp +contextual [subset_iff, eval_eq_eval_mv_eval', pₓ, hpₓ₀, p']

Premises used: MvPolynomial.eval_eq_eval_mv_eval', Finset.subset_iff
-- 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
⊢ #pₓ.roots.toFinset ≤ pₓ.roots.card

Tactic:
pₓ.roots.toFinset_card_le

Premises used: Polynomial.roots, Multiset.toFinset_card_le
-- 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
⊢ pₓ.roots.card ≤ pₓ.natDegree

Tactic:
pₓ.card_roots'

Premises used: Polynomial.card_roots'
-- 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
⊢ pₓ.natDegree = k

Tactic:
hpₓdeg
-- 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
⊢ Finsupp.cons k
      ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
        (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p'.leadingCoeff)) ∈
    p.support

Tactic:
have :
              (ofLex (AddMonoidAlgebra.supDegree toLex p'.leadingCoeff)).cons k ∈ p.support := by
              rwa [← mem_support_coeff_finSuccEquiv, mem_support_iff, ← hp', hk,
                ← Polynomial.leadingCoeff, ← hpₖ, ← leadingCoeff_toLex,
                AddMonoidAlgebra.leadingCoeff_ne_zero toLex.injective]
-- 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
this :
  Finsupp.cons k
      ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
        (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p'.leadingCoeff)) ∈
    p.support
⊢ k ≤ degreeOf 0 p

Tactic:
simpa using monomial_le_degreeOf 0 this

Premises used: MvPolynomial.monomial_le_degreeOf, OfNat.ofNat
-- 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
S₁ :
  #({x₀ ∈ S 0 |
        Eq (α := R)
          ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ xₜ) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
          (0 : R)}) ≤
    #pₓ.roots.toFinset
S₂ : k ≤ degreeOf 0 p
⊢ #({x₀ ∈ S 0 |
        Eq (α := R)
          ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ xₜ) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
          (0 : R)}) ≤
    degreeOf 0 p

Tactic:
calc
          #{x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0} ≤ #pₓ.roots.toFinset := by
            gcongr
            simp +contextual [subset_iff, eval_eq_eval_mv_eval', pₓ, hpₓ₀, p']
          _ ≤ Multiset.card pₓ.roots := pₓ.roots.toFinset_card_le
          _ ≤ pₓ.natDegree := pₓ.card_roots'
          _ = k := hpₓdeg
          _ ≤ p.degreeOf 0 := by
            have :
              (ofLex (AddMonoidAlgebra.supDegree toLex p'.leadingCoeff)).cons k ∈ p.support := by
              rwa [← mem_support_coeff_finSuccEquiv, mem_support_iff, ← hp', hk,
                ← Polynomial.leadingCoeff, ← hpₖ, ← leadingCoeff_toLex,
                AddMonoidAlgebra.leadingCoeff_ne_zero toLex.injective]
            simpa using monomial_le_degreeOf 0 this

Premises used: Multiset.toFinset, Polynomial.roots, Multiset.toFinset_card_le, Polynomial.card_roots', Multiset.card, Polynomial.natDegree, OfNat.ofNat, MvPolynomial.degreeOf
-- 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_2 :
  LE.le (α := ℚ≥0)
    (pₖ.support.sup fun (i : Fin n →₀ ℕ) ↦
      ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.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))
⊢ (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)

Tactic:
rw [Finset.sup_add (support_nonempty.mpr hpₖ₀)]

Premises used: Iff.mpr, MvPolynomial.support_nonempty, Finset.sup_add
-- 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_2 :
  ∀ b ∈ pₖ.support,
    ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((b : (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)
⊢ LE.le (α := ℚ≥0)
    (pₖ.support.sup fun (i : Fin n →₀ ℕ) ↦
      ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.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))

Tactic:
apply Finset.sup_le

Premises used: Finset.sup_le
-- 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
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.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)

Tactic:
le_sup_of_le (mem_support_coeff_finSuccEquiv.mp hi) ?_

Premises used: Finset.le_sup_of_le, Iff.mp, MvPolynomial.mem_support_coeff_finSuccEquiv
-- 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
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
calc_2 :
  ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.succ)) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(#(S 0)) : ℚ≥0) ≤
    ∑ i_1 : Fin (n + 1),
      HDiv.hDiv (α := ℚ≥0) (↑((Finsupp.cons p'.natDegree i : (a : Fin (n + 1)) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1)) : ℚ≥0)
⊢ ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.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)

Tactic:
refine le_sup_of_le (mem_support_coeff_finSuccEquiv.mp hi) ?_

Premises used: Finset.le_sup_of_le, Iff.mp, MvPolynomial.mem_support_coeff_finSuccEquiv
-- 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
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
calc_2 :
  HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(#(S 0)) : ℚ≥0) +
      ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.succ)) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑((Finsupp.cons p'.natDegree i : (a : Fin (n + 1)) → ℕ) 0) : ℚ≥0) (↑(#(S 0)) : ℚ≥0) +
      ∑ i_1 : Fin n,
        HDiv.hDiv (α := ℚ≥0) (↑((Finsupp.cons p'.natDegree i : (a : Fin (n + 1)) → ℕ) i_1.succ) : ℚ≥0)
          (↑(#(S i_1.succ)) : ℚ≥0)
⊢ ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.succ)) : ℚ≥0) +
      HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(#(S 0)) : ℚ≥0) ≤
    ∑ i_1 : Fin (n + 1),
      HDiv.hDiv (α := ℚ≥0) (↑((Finsupp.cons p'.natDegree i : (a : Fin (n + 1)) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1)) : ℚ≥0)

Tactic:
rw [Fin.sum_univ_succ, add_comm]

Premises used: add_comm, Fin.sum_univ_succ
-- 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
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
calc_2 :
  HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(#(S 0)) : ℚ≥0) +
      ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.succ)) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑p'.natDegree : ℚ≥0) (↑(#(S 0)) : ℚ≥0) +
      ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.succ)) : ℚ≥0)
⊢ HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(#(S 0)) : ℚ≥0) +
      ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.succ)) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑((Finsupp.cons p'.natDegree i : (a : Fin (n + 1)) → ℕ) 0) : ℚ≥0) (↑(#(S 0)) : ℚ≥0) +
      ∑ i_1 : Fin n,
        HDiv.hDiv (α := ℚ≥0) (↑((Finsupp.cons p'.natDegree i : (a : Fin (n + 1)) → ℕ) i_1.succ) : ℚ≥0)
          (↑(#(S i_1.succ)) : ℚ≥0)

Tactic:
dsimp