awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
rw :
  Finset.image (Finsupp.mapDomain f)
      (support.{u_4, u_1} (R := R) ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p)) ⊆
    p.support
rw₁ : Finset.image (Finsupp.mapDomain f) (p.support.preimage (Finsupp.mapDomain f) ⋯) ⊆ p.support
⊢ support.{u_4, u_2} (R := R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p)) ⊆
    p.support
have rw₂ : {x ∈ p.support | Membership.mem (γ := Set (τ →₀ ℕ)) (range (Finsupp.mapDomain f)) x} ⊆ p.support
Tactic: classical
  rw [MvPolynomial.support_rename_of_injective hf, support_killCompl, Finset.image_preimage]
  exact Finset.filter_subset ..
-- 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
p : MvPolynomial (Fin 0) R
hp : p ≠ 0
S : Fin 0 → Finset R
⊢ HDiv.hDiv (α := ℚ≥0)
      (↑(Finset.card.{u_1} (α := Fin 0 → R)
            ({x ∈ piFinset (δ := fun (a : Fin 0) ↦ R) fun (i : Fin 0) ↦ S i |
              Eq (α := R) ((eval x : (a : MvPolynomial (Fin 0) R) → R) p : R) (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin 0, (↑(#(S i)) : ℚ≥0)) ≤
    p.support.sup fun (s : Fin 0 →₀ ℕ) ↦
      ∑ i : Fin 0, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin 0) → ℕ) i) : ℚ≥0) (↑(#(S i)) : ℚ≥0)
have rw : ∀
  (hp :
    Ne (α := MvPolynomial (Fin 0) R) ((C : (a : R) → MvPolynomial (Fin 0) R) (coeff 0 p) : MvPolynomial (Fin 0) R)
      (0 : MvPolynomial (Fin 0) R))
  (S : Fin 0 → Finset R),
  HDiv.hDiv (α := ℚ≥0)
      (↑(Finset.card.{u_1} (α := Fin 0 → R)
            ({x ∈ piFinset (δ := fun (a : Fin 0) ↦ R) fun (i : Fin 0) ↦ S i |
              Eq (α := R)
                ((eval x : (a : MvPolynomial (Fin 0) R) → R)
                    ((C : (a : R) → MvPolynomial (Fin 0) R) (coeff 0 p) : MvPolynomial (Fin 0) R) :
                  R)
                (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin 0, (↑(#(S i)) : ℚ≥0)) ≤
    sup (support.{u_1, 0} (R := R) ((C : (a : R) → MvPolynomial (Fin 0) R) (coeff 0 p))) fun (s : Fin 0 →₀ ℕ) ↦
      ∑ i : Fin 0, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin 0) → ℕ) i) : ℚ≥0) (↑(#(S i)) : ℚ≥0)
Tactic: rw [p.eq_C_of_isEmpty] at *
Cleared hypotheses: hp, S
-- 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
⊢ 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)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥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 hp' : let p' : Polynomial (MvPolynomial (Fin n) R) :=
  (finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p;
p' = (finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p
Tactic: set p' : Polynomial (MvPolynomial (Fin n) R) := finSuccEquiv R n p with hp'
-- 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
⊢ 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)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥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 hk : let k := p'.natDegree;
k = p'.natDegree
Tactic: set k := p'.natDegree with hk
-- 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
⊢ 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)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥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 hpₖ : let pₖ := p'.leadingCoeff;
pₖ = p'.leadingCoeff
Tactic: set pₖ := p'.leadingCoeff with hpₖ
-- 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
⊢ 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)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥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 hp'₀ : p' ≠ 0
Tactic: have hp'₀ : p' ≠ 0 := EmbeddingLike.map_ne_zero_iff.2 hp
-- 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
⊢ 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)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥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 hpₖ₀ : pₖ ≠ 0
Tactic: have hpₖ₀ : pₖ ≠ 0 := by simpa [pₖ, k]
-- 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)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥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_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) ∧
                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} (α := 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)) ≤
  (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)
Tactic: calc
      -- We split the set of possible zeros into a union of two cases.
      #{x ∈ S ^^ (n + 1) | eval x p = 0} / ∏ i, (#(S i) : ℚ≥0)
          -- In the first case, `pₖ` evaluates to `0`.
        = #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0)
          -- In the second case, `pₖ` does not evaluate to `0`.
          + #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ ≠ 0} / ∏ i, (#(S i) : ℚ≥0) := by
        rw [← add_div, ← Nat.cast_add, ← card_union_add_card_inter, filter_union_right,
          ← filter_and]
        simp [← and_or_left, em, and_and_and_comm]
      _ ≤ (pₖ.support.sup fun s ↦ ∑ i, (s i / #(S i.succ) : ℚ≥0)) + p.degreeOf 0 / #(S 0) := ?_
      _ ≤ p.support.sup fun s ↦ ∑ i, (s i / #(S i) : ℚ≥0) := ?_
-- 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)) +
      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)) ≤
    (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)
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) ∧
              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)
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
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) ∧
                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)
⊢ 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} (α := 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)) ≤
    (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)
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) : ℚ≥0) (↑(#(S 0)) : ℚ≥0)
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
⊢ 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))
have hab : ∀ (x : Fin (n + 1) → R),
  Membership.mem (γ := Finset (Fin (n + 1) → R)) (piFinset (δ := fun (a : Fin (n + 1)) ↦ R) fun (i : Fin (n + 1)) ↦ S i)
      x →
    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) →
      Eq (α := R) ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) x) : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)
Tactic: gcongr with x
-- 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} (α := (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)) =
    HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0)
        (↑(Finset.card.{u_1} (α := Fin n → R)
              ({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)})) :
          ℚ≥0) /
      HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0) (∏ i : Fin n, (↑(#(S i.succ)) : ℚ≥0))
have rw : (↑(#(S 0) *
          Finset.card.{u_1} (α := (i : Fin n) → R)
            ({r ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (k : Fin n) ↦ S k.succ |
              Eq (α := R) ((eval r : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})) :
      ℚ≥0) /
    HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0) (∏ i : Fin n, (↑(#(S i.succ)) : ℚ≥0)) =
  HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0)
      (↑(Finset.card.{u_1} (α := Fin n → R)
            ({xₜ ∈ piFinset (δ := fun (a : Fin n) ↦ R) fun (i : Fin n) ↦ (fun (k : Fin n) ↦ S k.succ) i |
              Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})) :
        ℚ≥0) /
    HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0) (∏ i : Fin n, (↑(#(S i.succ)) : ℚ≥0))
Tactic: rw [card_consEquiv_filter_piFinset S fun x ↦ eval x pₖ = 0, prod_univ_succ, tail_def]
-- 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
⊢ (↑(#(S 0) *
            Finset.card.{u_1} (α := (i : Fin n) → R)
              ({r ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (k : Fin n) ↦ S k.succ |
                Eq (α := R) ((eval r : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})) :
        ℚ≥0) /
      HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0) (∏ i : Fin n, (↑(#(S i.succ)) : ℚ≥0)) =
    HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0)
        (↑(Finset.card.{u_1} (α := Fin n → R)
              ({xₜ ∈ piFinset (δ := fun (a : Fin n) ↦ R) fun (i : Fin n) ↦ (fun (k : Fin n) ↦ S k.succ) i |
                Eq (α := R) ((eval xₜ : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})) :
          ℚ≥0) /
      HMul.hMul (α := ℚ≥0) (↑(#(S 0)) : ℚ≥0) (∏ i : Fin n, (↑(#(S i.succ)) : ℚ≥0))
have norm_cast : HDiv.hDiv (α := ℚ≥0)
    (↑(#(S 0) *
          Finset.card.{u_1} (α := (i : Fin n) → R)
            ({x ∈ piFinset (δ := fun (i : Fin n) ↦ R) fun (k : Fin n) ↦ S k.succ |
              Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})) :
      ℚ≥0)
    (↑(#(S 0) * ∏ i : Fin n, #(S i.succ)) : ℚ≥0) =
  HDiv.hDiv (α := ℚ≥0)
    (↑(#(S 0) *
          Finset.card.{u_1} (α := Fin n → R)
            ({x ∈ piFinset (δ := fun (a : Fin n) ↦ R) fun (i : Fin n) ↦ (fun (k : Fin n) ↦ S k.succ) i |
              Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) pₖ : R) (0 : R)})) :
      ℚ≥0)
    (↑(#(S 0) * ∏ i : Fin n, #(S i.succ)) : ℚ≥0)
Tactic: norm_cast