awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
rw : coeff d (Finsupp.mapDomain (Finsupp.mapDomain f) φ) = 0
rw₁ rw₂ rw₃ : d ∉ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
rw₄ : ∀ (H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)), False
rw₅ : ∀ (H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support), False
rw₆ : ∀ (H : ∃ a ∈ φ.support, Finsupp.mapDomain f a = d), False
rw₇ :
  ∀ (u : σ →₀ ℕ) (hu : u ∈ φ.support)
    (h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0), False
rw₈ : ∀ (u : σ →₀ ℕ) (hu : u ∈ φ.support) (h : coeff u φ = 0), False
rw₉ : ∀ (u : σ →₀ ℕ) (hu : Ne.{u_4 + 1} (α := R) ((φ : (a : σ →₀ ℕ) → R) u : R) (0 : R)) (h : coeff u φ = 0), False
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0

Tactic:
classical
  rw [rename_eq, ← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction

Premises used: Finsupp.mem_support_iff, MvPolynomial.notMem_support_iff, Finset.mem_image, rfl, MvPolynomial.rename_eq
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : Ne.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
contrapose! :
  ∀ (h : ∀ (u : σ →₀ ℕ) (_ : Finsupp.mapDomain f u = d), coeff u φ = 0),
    Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
⊢ ∃ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d ∧ coeff u φ ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ) (_ : Finsupp.mapDomain f u = d), coeff u φ = 0
⊢ Eq.{u_4 + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0

Tactic:
apply coeff_rename_eq_zero _ _ _ h

Premises used: MvPolynomial.coeff_rename_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq.{u_4 + 1} (α := R)
      ((constantCoeff : (a : MvPolynomial τ R) → R)
          ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
            MvPolynomial τ R) :
        R)
      ((constantCoeff : (a : MvPolynomial σ R) → R)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) :
        R)
add :
  ∀ (p q : MvPolynomial σ R),
    Eq.{u_4 + 1} (α := R)
        ((constantCoeff : (a : MvPolynomial τ R) → R)
            ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R) :
          R)
        ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) →
      Eq.{u_4 + 1} (α := R)
          ((constantCoeff : (a : MvPolynomial τ R) → R)
              ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) q : MvPolynomial τ R) :
            R)
          ((constantCoeff : (a : MvPolynomial σ R) → R) q : R) →
        Eq.{u_4 + 1} (α := R)
          ((constantCoeff : (a : MvPolynomial τ R) → R)
              ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q) : MvPolynomial τ R) :
            R)
          ((constantCoeff : (a : MvPolynomial σ R) → R) (p + q) : R)
mul_X :
  ∀ (p : MvPolynomial σ R) (n : σ),
    Eq.{u_4 + 1} (α := R)
        ((constantCoeff : (a : MvPolynomial τ R) → R)
            ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R) :
          R)
        ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) →
      Eq.{u_4 + 1} (α := R)
        ((constantCoeff : (a : MvPolynomial τ R) → R)
            ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X n) : MvPolynomial τ R) :
          R)
        ((constantCoeff : (a : MvPolynomial σ R) → R) (p * X n) : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) φ : R)

Tactic:
apply φ.induction_on

Premises used: MvPolynomial.induction_on
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
a : R
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) a) :
          MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : R)

Tactic:
simp only [constantCoeff_C, rename_C]

Premises used: MvPolynomial.constantCoeff_C, MvPolynomial.rename_C
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
τ : Type u_6
f : σ → τ
φ p q : MvPolynomial σ R
hp :
  Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) p : R)
hq :
  Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) q : MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) q : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q) : MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) (p + q) : R)

Tactic:
simp only [hp, hq, map_add]

Premises used: map_add
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
R : Type u_4
inst : CommSemiring R
τ : Type u_6
f : σ → τ
φ p : MvPolynomial σ R
n : σ
hp :
  Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) p : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((constantCoeff : (a : MvPolynomial τ R) → R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X n) : MvPolynomial τ R) :
      R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) (p * X n) : R)

Tactic:
simp only [hp, rename_X, constantCoeff_X, map_mul]

Premises used: MvPolynomial.constantCoeff_X, map_mul, MvPolynomial.rename_X
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
inst_1 : DecidableEq τ
h : Injective f
rw : support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) p.support
⊢ support.{u_4, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p) =
    Finset.image (Finsupp.mapDomain f) p.support

Tactic:
rw [rename_eq]

Premises used: MvPolynomial.rename_eq
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
inst_1 : DecidableEq τ
h : Injective f
⊢ support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) p.support

Tactic:
Finsupp.mapDomain_support_of_injective (Finsupp.mapDomain_injective h) _

Premises used: Finsupp.mapDomain_support_of_injective, MvPolynomial.support, Finsupp.mapDomain_injective
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
inst_1 : DecidableEq τ
h : Injective f
⊢ support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) p.support

Tactic:
exact Finsupp.mapDomain_support_of_injective (Finsupp.mapDomain_injective h) _

Premises used: Finsupp.mapDomain_support_of_injective, Finsupp.mapDomain_injective
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
rw : {x ∈ p.support | Membership.mem (γ := Set (τ →₀ ℕ)) (range (Finsupp.mapDomain f)) x} ⊆ 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

Tactic:
rw [MvPolynomial.support_rename_of_injective hf, support_killCompl, Finset.image_preimage]

Premises used: MvPolynomial.support_killCompl, MvPolynomial.support_rename_of_injective, Finset.image_preimage
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ {x ∈ p.support | Membership.mem (γ := Set (τ →₀ ℕ)) (range (Finsupp.mapDomain f)) x} ⊆ p.support

Tactic:
Finset.filter_subset ..

Premises used: Set.Mem, setOf, Finset.filter_subset
-- Module: Mathlib.Algebra.MvPolynomial.Rename
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ {x ∈ p.support | Membership.mem (γ := Set (τ →₀ ℕ)) (range (Finsupp.mapDomain f)) x} ⊆ p.support

Tactic:
exact Finset.filter_subset ..

Premises used: Finset.filter_subset
-- Module: Mathlib.Algebra.MvPolynomial.Rename
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
rw₂ rw₃ rw₄ : {x ∈ p.support | Membership.mem (γ := Set (τ →₀ ℕ)) (range (Finsupp.mapDomain f)) x} ⊆ 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

Tactic:
classical
  rw [MvPolynomial.support_rename_of_injective hf, support_killCompl, Finset.image_preimage]
  exact Finset.filter_subset ..

Premises used: MvPolynomial.support_killCompl, Finset.filter_subset, Finset.image_preimage
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
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
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)
⊢ 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)

Tactic:
rw [p.eq_C_of_isEmpty] at *

Premises used: MvPolynomial.eq_C_of_isEmpty
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : MvPolynomial (Fin 0) R
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:
simp [C_ne_zero.mp hp]

Premises used: Iff.mp, MvPolynomial.C_ne_zero
-- 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
⊢ 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'

Premises used: MvPolynomial.finSuccEquiv, Polynomial, MvPolynomial, Fin, DFunLike.coe
-- 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
⊢ let k := p'.natDegree;
  k = p'.natDegree

Tactic:
set k := p'.natDegree with hk

Premises used: Polynomial.natDegree
-- 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
⊢ let pₖ := p'.leadingCoeff;
  pₖ = p'.leadingCoeff

Tactic:
set pₖ := p'.leadingCoeff with hpₖ

Premises used: Polynomial.leadingCoeff
-- 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
⊢ p' ≠ 0

Tactic:
have hp'₀ : p' ≠ 0 := EmbeddingLike.map_ne_zero_iff.2 hp
-- 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
⊢ pₖ ≠ 0

Tactic:
simpa [pₖ, k]
-- 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
⊢ pₖ ≠ 0

Tactic:
have hpₖ₀ : pₖ ≠ 0 := by simpa [pₖ, k]
-- 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
⊢ 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)) =
    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) ∨
                  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)}) +
            Finset.card.{u_1} (α := Fin (n + 1) → R)
              ({a ∈ piFinset (δ := fun (a : Fin (n + 1)) ↦ R) fun (i : Fin (n + 1)) ↦ S i |
                (Eq (α := R) ((eval a : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R) ∧
                    Eq (α := R)
                      ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) a) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
                      (0 : R)) ∧
                  Eq (α := R) ((eval a : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R) ∧
                    Ne (α := R)
                      ((eval (tail (α := fun (i : Fin (n + 1)) ↦ R) a) : (a : MvPolynomial (Fin n) R) → R) pₖ : R)
                      (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin (n + 1), (↑(#(S i)) : ℚ≥0))

Tactic:
simp [← and_or_left, em, and_and_and_comm]

Premises used: and_or_left, em, and_and_and_comm
-- 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
⊢ 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:
?_
-- 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
⊢ (pₖ.support.sup fun (s : Fin n →₀ ℕ) ↦
        ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#(S i.succ)) : ℚ≥0)) +
      HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(#(S 0)) : ℚ≥0) ≤
    p.support.sup fun (s : Fin (n + 1) →₀ ℕ) ↦
      ∑ i : Fin (n + 1), HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin (n + 1)) → ℕ) i) : ℚ≥0) (↑(#(S i)) : ℚ≥0)

Tactic:
?_