awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
⊢ #({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 hpₓdeg : 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]
-- 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
h : pₓ = 0
rw : Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) p'.leadingCoeff : R) (0 : R)
⊢ Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)
have rw₁ : Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) (p'.coeff p'.natDegree) : R) (0 : R)
Tactic: rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]
-- 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
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)
⊢ Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)
have rw₃ : Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) (p'.coeff pₓ.natDegree) : R) (0 : R)
Tactic: rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]
-- 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
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)
⊢ Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)
have rw₄ : Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) (p'.coeff (Polynomial.natDegree.{u_1} (R := R) 0)) : R)
  (0 : R)
Tactic: rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]
-- 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
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)
⊢ Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)
have rw₅ : Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) (p'.coeff 0) : R) (0 : R)
Tactic: rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]
-- 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
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)
⊢ Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)
have rw₆ : (Polynomial.map (eval xₜ) p').coeff 0 = 0
Tactic: rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]
-- 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
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
⊢ Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)
have rw₈ : Eq.{u_1 + 1} (α := R) (Polynomial.coeff 0 0) 0
Tactic: rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]
-- 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
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
⊢ Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)
have rw₉ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]
-- 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
⊢ #({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 hpₓ₀ : 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]
-- 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)}) ≤
    #pₓ.roots.toFinset
have 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
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 + 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
have 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))
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 (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))
⊢ 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₁ : 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
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 (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
⊢ 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₄ : coeff
    ((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ)
      (AddMonoidAlgebra.supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p'.leadingCoeff))
    p'.leadingCoeff ≠
  0
Tactic: rwa [← mem_support_coeff_finSuccEquiv, mem_support_iff, ← hp', hk,
                ← Polynomial.leadingCoeff, ← hpₖ, ← leadingCoeff_toLex,
                AddMonoidAlgebra.leadingCoeff_ne_zero toLex.injective]