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
rw :
  Finset.card (α := R × ((i : Fin n) → R))
      ({r ∈ piFinset (δ := fun (i : Fin n) ↦ R) (tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S) |
            Ne (α := R) ((eval r : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)}.biUnion
        fun (a : (i : Fin n) → R) ↦
        filter
          ((fun (x : (i : Fin (n + 1)) → R) ↦
              Eq (α := R) ((eval x : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R)) ∘
            (⇑(Equiv.toEmbedding (consEquiv.{u_1} (n := n) fun (i : Fin (n + 1)) ↦ R) :
                  R × ((i : Fin n) → R) ↪ (i : Fin (n + 1)) → R) :
              (a : R × ((i : Fin n) → R)) → (i : Fin (n + 1)) → R))
          (image (fun (a_1 : R) ↦ (a_1, a)) (S 0))) =
    Finset.card.{u_1} (α := R × (Fin n → R))
      (Finset.biUnion
        ({xₜ ∈ piFinset (δ := fun (a : 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)})
        fun (xₜ : Fin n → R) ↦
        image (fun (x₀ : R) ↦ (x₀, xₜ))
          ({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)}))
⊢ Finset.card.{u_1} (α := (i : Fin (n + 1)) → R)
      ({x ∈ piFinset (δ := fun (i : Fin (n + 1)) ↦ R) fun (i : Fin (n + 1)) ↦ S i |
        Ne (α := R) ((eval (tail (α := fun (a : Fin (n + 1)) ↦ R) x) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
            (0 : R) ∧
          Eq (α := R) ((eval x : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R)}) =
    Finset.card.{u_1} (α := R × (Fin n → R))
      (Finset.biUnion
        ({xₜ ∈ piFinset (δ := fun (a : 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)})
        fun (xₜ : Fin n → R) ↦
        image (fun (x₀ : R) ↦ (x₀, xₜ))
          ({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)}))

Tactic:
rw [← filter_filter, filter_piFinset_eq_map_consEquiv S (fun r ↦ eval r pₖ ≠ 0),
              filter_map, card_map, product_eq_biUnion_right, filter_biUnion]

Premises used: Finset.filter_filter, Finset.card_map, Finset.filter_piFinset_eq_map_consEquiv, Ne, Finset.product_eq_biUnion_right, MvPolynomial.eval, Finset.filter_biUnion, OfNat.ofNat, DFunLike.coe, Finset.filter_map
-- 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
⊢ Finset.card (α := R × ((i : Fin n) → R))
      ({x ∈ piFinset (δ := fun (i : Fin n) ↦ R) (tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S) |
            ¬Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)}.biUnion
        fun (a : (i : Fin n) → R) ↦
        image (fun (a_1 : R) ↦ (a_1, a))
          ({a_1 ∈ S 0 |
            Eq (α := R)
              ((eval
                      (((consEquiv.{u_1} (n := n) fun (i : Fin (n + 1)) ↦ R :
                            R × ((i : Fin n) → R) ≃ ((i : Fin (n + 1)) → R)) :
                          (a : R × ((i : Fin n) → R)) → (i : Fin (n + 1)) → R)
                        (a_1, a)) :
                    (a : MvPolynomial (Fin (n + 1)) R) → R)
                  p :
                R)
              (0 : R)})) =
    Finset.card.{u_1} (α := R × (Fin n → R))
      (Finset.biUnion
        ({x ∈ piFinset (δ := fun (a : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i |
          ¬Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})
        fun (xₜ : Fin n → R) ↦
        image (fun (x₀ : R) ↦ (x₀, xₜ))
          ({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)}))

Tactic:
rfl
-- 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
⊢ Finset.card.{u_1} (α := R × (Fin n → R))
      (Finset.biUnion
        ({xₜ ∈ piFinset (δ := fun (a : 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)})
        fun (xₜ : Fin n → R) ↦
        image (fun (x₀ : R) ↦ (x₀, xₜ))
          ({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)})) ≤
    ∑ xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i with
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R),
      Finset.card (α := R × (Fin n → R))
        (image (fun (x₀ : R) ↦ (x₀, xₜ))
          ({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)}))

Tactic:
card_biUnion_le

Premises used: Finset.card_biUnion_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
h :
  ∀ (i : Fin n → R),
    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)})
        i →
      Finset.card (α := R × (Fin n → R))
          (image (fun (x₀ : R) ↦ (x₀, i))
            ({x₀ ∈ S 0 |
              Eq (α := R)
                ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ i) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
                (0 : R)})) ≤
        #({x₀ ∈ S 0 |
            Eq (α := R)
              ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ i) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
              (0 : R)})
⊢ LE.le (α := ℕ)
    (∑ xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i with
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R),
      Finset.card (α := R × (Fin n → R))
        (image (fun (x₀ : R) ↦ (x₀, xₜ))
          ({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)})))
    (∑ xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i with
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R),
      #({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)}))

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
i : Fin n → R
h :
  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)})
    i
⊢ Finset.card (α := R × (Fin n → R))
      (image (fun (x₀ : R) ↦ (x₀, i))
        ({x₀ ∈ S 0 |
          Eq (α := R)
            ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ i) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
            (0 : R)})) ≤
    #({x₀ ∈ S 0 |
        Eq (α := R)
          ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ i) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
          (0 : R)})

Tactic:
card_image_le

Premises used: Finset.card_image_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 → R
h :
  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)})
    i
⊢ Finset.card (α := R × (Fin n → R))
      (image (fun (x₀ : R) ↦ (x₀, i))
        ({x₀ ∈ S 0 |
          Eq (α := R)
            ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ i) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
            (0 : R)})) ≤
    #({x₀ ∈ S 0 |
        Eq (α := R)
          ((eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) x₀ i) : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R)
          (0 : R)})

Tactic:
exact card_image_le

Premises used: Finset.card_image_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
⊢ LE.le (α := ℕ)
    (∑ xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i with
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R),
      #({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)}))
    (∑ xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i with
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R), degreeOf 0 p)

Tactic:
?_
-- 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
h :
  Subset.{u_1} (α := 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)})
    (piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i)
⊢ LE.le (α := ℕ)
    (∑ xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i with
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R), degreeOf 0 p)
    (∑ _xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i,
      degreeOf 0 p)

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
⊢ Subset.{u_1} (α := 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)})
    (piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i)

Tactic:
filter_subset ..

Premises used: Finset.filter_subset
-- 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
⊢ Subset.{u_1} (α := 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)})
    (piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i)

Tactic:
exact filter_subset ..

Premises used: Finset.filter_subset
-- 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ₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i,
      degreeOf 0 p =
    degreeOf 0 p * ∏ i : Fin n, #(S i.succ)

Tactic:
simp [mul_comm, tail]

Premises used: mul_comm, Fin.tail
-- 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_1 :
  LE.le (α := ℕ)
    (∑ xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i with
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R),
      #({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)}))
    (∑ xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i with
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R), degreeOf 0 p)
⊢ Finset.card.{u_1} (α := Fin (n + 1) → R)
      ({x ∈ piFinset (δ := fun (a : Fin (n + 1)) ↦ R) fun (i : Fin (n + 1)) ↦ S i |
        Eq (α := R) ((eval x : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R) ∧
          Ne (α := R) ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) x) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
            (0 : R)}) ≤
    degreeOf 0 p * ∏ i : Fin n, #(S i.succ)

Tactic:
calc
          #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ ≠ 0}
            = #{x ∈ S ^^ (n + 1) | eval (tail x) pₖ ≠ 0 ∧ eval x p = 0} := by simp_rw [and_comm]
          _ = #({xₜ ∈ tail S ^^ n | eval xₜ pₖ ≠ 0}.biUnion fun xₜ ↦ image (fun x₀ ↦ (x₀, xₜ))
                {x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0}) := by
            rw [← filter_filter, filter_piFinset_eq_map_consEquiv S (fun r ↦ eval r pₖ ≠ 0),
              filter_map, card_map, product_eq_biUnion_right, filter_biUnion]
            simp [filter_image]
            rfl
          _ ≤ ∑ xₜ ∈ tail S ^^ n with eval xₜ pₖ ≠ 0,
                #(image (fun x₀ ↦ (x₀, xₜ)) {x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0}) :=
            card_biUnion_le
          _ ≤ ∑ xₜ ∈ tail S ^^ n with eval xₜ pₖ ≠ 0, #{x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0} := by
            gcongr; exact card_image_le
          _ ≤ ∑ xₜ ∈ tail S ^^ n with eval xₜ pₖ ≠ 0, p.degreeOf 0 := ?_
          _ ≤ ∑ _xₜ ∈ tail S ^^ n, p.degreeOf 0 := by gcongr; exact filter_subset ..
          _ = p.degreeOf 0 * ∏ i, #(S (.succ i)) := by simp [mul_comm, tail]

Premises used: Fin.cons, Prod.mk, Ne, Finset.biUnion, Fintype.piFinset, MvPolynomial.eval, HAdd.hAdd, Finset.card_biUnion_le, OfNat.ofNat, Finset.filter, Eq, Fin.tail, DFunLike.coe, Finset.image, 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_1 :
  ∀ (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ₜ),
    #({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
⊢ LE.le (α := ℕ)
    (∑ xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i with
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R),
      #({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)}))
    (∑ xₜ ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (i : Fin n) ↦ tail (α := fun (i : Fin (n + 1)) ↦ Finset R) S i with
      Ne (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R), degreeOf 0 p)

Tactic:
gcongr with xₜ hxₜ
-- 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ₜ
⊢ let pₓ := Polynomial.map (eval xₜ) p';
  pₓ = Polynomial.map (eval xₜ) p'

Tactic:
set pₓ := p'.map (eval xₜ) with hpₓ

Premises used: MvPolynomial.eval, Polynomial.map
-- 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'
rw : (Polynomial.map (eval xₜ) p').natDegree = k
rw₁ : (Polynomial.map (eval xₜ) p').natDegree = p'.natDegree
rw₂ rw₃ : p'.natDegree = p'.natDegree
⊢ pₓ.natDegree = k

Tactic:
rw [hpₓ, hk, Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ (mem_filter.1 hxₜ).2]

Premises used: And.right, Polynomial.natDegree_map_of_leadingCoeff_ne_zero, Iff.mp, Finset.mem_filter