awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
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
⊢ Finsupp.cons k
      ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
        (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p'.leadingCoeff)) ∈
    p.support
have rwa₆ : AddMonoidAlgebra.leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) pₖ ≠ 0
Tactic: rwa [← mem_support_coeff_finSuccEquiv, mem_support_iff, ← hp', hk,
                ← Polynomial.leadingCoeff, ← hpₖ, ← leadingCoeff_toLex,
                AddMonoidAlgebra.leadingCoeff_ne_zero toLex.injective]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (hypothesis)
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
⊢ k ≤ degreeOf 0 p
have this : 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
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)}) ≤
    degreeOf 0 p
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
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
⊢ #({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
have S₂ : k ≤ 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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
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
⊢ (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)
have 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))
Tactic: rw [Finset.sup_add (support_nonempty.mpr hpₖ₀)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
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
⊢ 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))
have 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)
Tactic: apply Finset.sup_le
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
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)
have 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)
Tactic: refine le_sup_of_le (mem_support_coeff_finSuccEquiv.mp hi) ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
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) ≤
    ∑ i_1 : Fin (n + 1),
      HDiv.hDiv (α := ℚ≥0) (↑((Finsupp.cons p'.natDegree i : (a : Fin (n + 1)) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1)) : ℚ≥0)
have 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)
Tactic: rw [Fin.sum_univ_succ, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
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
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
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
⊢ 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)
have calc_2 : degreeOf 0 p ≤ p'.natDegree
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
s : Fin n →₀ ℕ
hs : s ∈ p.support
⊢ LE.le (α := ℚ≥0) (∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#(S i)) : ℚ≥0))
    (∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑(degreeOf i p) : ℚ≥0) (↑(#(S i)) : ℚ≥0))
have h : ∀ (i : Fin n), Membership.mem (γ := Finset (Fin n)) univ i → (s : (a : Fin n) → ℕ) i ≤ degreeOf i p
Tactic: gcongr with i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
⊢ (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(#S) : ℚ≥0)
have inl : (p.support.sup fun (s : Fin n →₀ ℕ) ↦
    ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(Finset.card.{u_1} (α := R) ∅) : ℚ≥0)) =
  HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(Finset.card.{u_1} (α := R) ∅) : ℚ≥0)
Tactic: obtain rfl | hs := S.eq_empty_or_nonempty
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
inl :
  (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(Finset.card.{u_1} (α := R) ∅) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(Finset.card.{u_1} (α := R) ∅) : ℚ≥0)
⊢ (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(#S) : ℚ≥0)
have inr : ∀ (hs : S.Nonempty),
  (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(#S) : ℚ≥0)
Tactic: obtain rfl | hs := S.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
⊢ (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(Finset.card.{u_1} (α := R) ∅) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(Finset.card.{u_1} (α := R) ∅) : ℚ≥0)
have inl : Eq (α := ℚ≥0) (p.support.sup fun (s : Fin n →₀ ℕ) ↦ 0) 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(#S) : ℚ≥0)
have inr : (p.support.sup fun (s : Fin n →₀ ℕ) ↦
    ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
  HDiv.hDiv (α := ℚ≥0) (p.support.sup fun (i : Fin n →₀ ℕ) ↦ (↑(i.sum fun (x : Fin n) (e : ℕ) ↦ e) : ℚ≥0)) (↑(#S) : ℚ≥0)
Tactic: simp_rw [totalDegree, Nat.cast_finsetSup]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.SchwartzZippel (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (p.support.sup fun (i : Fin n →₀ ℕ) ↦ (↑(i.sum fun (x : Fin n) (e : ℕ) ↦ e) : ℚ≥0))
      (↑(#S) : ℚ≥0)
have inr : Eq (α := ℚ≥0)
  (p.support.sup fun (s : Fin n →₀ ℕ) ↦
    ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0))
  (p.support.sup fun (i : Fin n →₀ ℕ) ↦ HDiv.hDiv (α := ℚ≥0) (↑(i.sum fun (x : Fin n) (e : ℕ) ↦ e) : ℚ≥0) (↑(#S) : ℚ≥0))
Tactic: rw [sup_div₀ (by positivity)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
⊢ Eq (α := Subalgebra R (MvPolynomial σ R)) (supported R s)
    (AlgHom.range (A := MvPolynomial.{u_1, u} { x : σ // x ∈ s } R) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))))
have rw : Eq (α := Subalgebra R (MvPolynomial σ R))
  (AlgHom.range (A := MvPolynomial.{u_1, u} (↑s : Type u_1) R) (aeval fun (x : (↑s : Type u_1)) ↦ X (↑x : σ)))
  (AlgHom.range (A := MvPolynomial.{u_1, u} { x : σ // x ∈ s } R) (aeval (X ∘ Subtype.val (p := fun (x : σ) ↦ x ∈ s))))
Tactic: rw [supported, Set.image_eq_range, adjoin_range_eq_range_aeval, rename]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
x : R
⊢ Eq (α := ↥(supported R s))
    ((AlgEquiv.symm (supportedEquivMvPolynomial s) : (a : MvPolynomial (↑s : Type u_1) R) → ↥(supported R s))
        ((C : (a : R) → MvPolynomial (↑s : Type u_1) R) x) :
      ↥(supported R s))
    ((algebraMap R ↥(supported R s) : (a : R) → ↥(supported R s)) x : ↥(supported R s))
have a : Eq (α := MvPolynomial σ R)
  (↑((AlgEquiv.symm (supportedEquivMvPolynomial s) : (a : MvPolynomial (↑s : Type u_1) R) → ↥(supported R s))
        ((C : (a : R) → MvPolynomial (↑s : Type u_1) R) x)) :
    MvPolynomial σ R)
  (↑((algebraMap R ↥(supported R s) : (a : R) → ↥(supported R s)) x) : MvPolynomial σ R)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R s) p ↔ (↑p.vars : Set σ) ⊆ s
have rw : (∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x =
      p) ↔
  (↑p.vars : Set σ) ⊆ s
Tactic: rw [supported_eq_range_rename, AlgHom.mem_range]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ (∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x =
        p) ↔
    (↑p.vars : Set σ) ⊆ s
have mp : (∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x =
      p) →
  (↑p.vars : Set σ) ⊆ s
Tactic: constructor