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
⊢ HDiv.hDiv (α := ℚ≥0)
      (↑(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) ∧
                Eq (α := R) ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) x) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
                  (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(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)
have S₁ : HDiv.hDiv (α := ℚ≥0)
    (↑(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) ∧
              Eq (α := R) ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) x) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
                (0 : R)})) :
      ℚ≥0)
    (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0)) ≤
  HDiv.hDiv (α := ℚ≥0)
    (↑(Finset.card.{u_1} (α := (i : Fin (n + 1)) → R)
          ({x ∈ piFinset (δ := fun (i : Fin (n + 1)) ↦ R) fun (i : Fin (n + 1)) ↦ S i |
            Eq (α := R) ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) x) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
              (0 : R)})) :
      ℚ≥0)
    (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0))
Tactic: calc
          #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0)
            ≤ #{x ∈ S ^^ (n + 1) | eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0) := by
            gcongr with x; exact And.right
          _ = #(S 0) * #{xₜ ∈ tail S ^^ n | eval xₜ pₖ = 0}
              / (#(S 0) * (∏ i, #(S (.succ i)) : ℚ≥0)) := by
            rw [card_consEquiv_filter_piFinset S fun x ↦ eval x pₖ = 0, prod_univ_succ, tail_def]
            norm_cast
          _ ≤ #{xₜ ∈ tail S ^^ n | eval xₜ pₖ = 0} / ∏ i, (#(S (.succ i)) : ℚ≥0) :=
            mul_div_mul_left_le (by positivity)
          _ ≤ (pₖ.support.sup fun s ↦ ∑ i, (s i / #(S (.succ i)) : ℚ≥0)) :=
            schwartz_zippel_sup_sum 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
⊢ HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0)) =
    HMul.hMul (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(∏ i : Fin n, #(S i.succ)) : ℚ≥0) /
      HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0) (↑(∏ i : Fin n, #(S i.succ)) : ℚ≥0)
have norm_cast : HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) (↑(∏ i : Fin (n + 1), #(S i)) : ℚ≥0) =
  HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) (↑(#(S 0) * ∏ i : Fin n, #(S i.succ)) : ℚ≥0)
Tactic: norm_cast
-- 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
⊢ HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) (↑(∏ i : Fin (n + 1), #(S i)) : ℚ≥0) =
    HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) (↑(#(S 0) * ∏ i : Fin n, #(S i.succ)) : ℚ≥0)
have rw : HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) (↑(#(S 0) * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) =
  HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) (↑(#(S 0) * ∏ i : Fin n, #(S i.succ)) : ℚ≥0)
Tactic: rw [prod_univ_succ]
-- 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
⊢ HDiv.hDiv (α := ℚ≥0)
      (↑(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)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0)) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(#(S 0)) : ℚ≥0)
have calc_1 : HDiv.hDiv (α := ℚ≥0)
    (↑(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)})) :
      ℚ≥0)
    (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0)) ≤
  HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0))
Tactic: calc
          #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ ≠ 0} / ∏ i, (#(S i) : ℚ≥0)
            ≤ ↑(p.degreeOf 0 * ∏ i, #(S (.succ i))) / ∏ i, (#(S i) : ℚ≥0) := ?_
          _ = p.degreeOf 0 * (∏ i, #(S (.succ i))) / (#(S 0) * ∏ i, #(S (.succ i))) := by
            norm_cast; rw [prod_univ_succ]
          _ ≤ (p.degreeOf 0 / #(S 0) : ℚ≥0) := mul_div_mul_right_le (by positivity)
-- 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
⊢ HDiv.hDiv (α := ℚ≥0)
      (↑(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)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0)) ≤
    HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0))
have calc_1 : 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: 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
⊢ 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)}))
have 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)}))
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]
-- 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
⊢ 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)}))
have simp : 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: simp [filter_image]
-- 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 (α := ℕ)
    (∑ 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)}))
have 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)})
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
⊢ 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)
have 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)
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
⊢ 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)
have 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)
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]
-- 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 (α := ℕ)
    (∑ 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)
have 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
Tactic: gcongr with xₜ hxₜ
-- 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ₜ
⊢ #({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ₓ : let pₓ := Polynomial.map (eval xₜ) p';
pₓ = Polynomial.map (eval xₜ) p'
Tactic: set pₓ := p'.map (eval xₜ) with hpₓ