awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hdp : d ≤ rootMultiplicity 1 p
hp : ¬p = 0
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
neg :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p).hilbertPoly
      d =
    0
neg₁ :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p).hilbertPoly
      (0 + d) =
    0
neg₂ :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p - d + d) *
          HSub.hSub (α := F[X]) 1 X ^ (rootMultiplicity 1 p - d + d)).hilbertPoly
      (0 + d) =
    0
neg₃ :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p - d + d) *
          (HSub.hSub (α := F[X]) 1 X ^ (rootMultiplicity 1 p - d) * HSub.hSub (α := F[X]) 1 X ^ d)).hilbertPoly
      (0 + d) =
    0
neg₄ :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p - d + d) *
            HSub.hSub (α := F[X]) 1 X ^ (rootMultiplicity 1 p - d) *
          HSub.hSub (α := F[X]) 1 X ^ d).hilbertPoly
      (0 + d) =
    0
neg₅ :
  (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p - d + d) *
          HSub.hSub (α := F[X]) 1 X ^ (rootMultiplicity 1 p - d)).hilbertPoly
      0 =
    0
neg₆ neg₇ : Eq.{u_1 + 1} (α := F[X]) 0 0
⊢ p.hilbertPoly d = 0

Tactic:
rw [heq, ← zero_add d, ← Nat.sub_add_cancel hdp, pow_add (1 - X), ← mul_assoc,
      hilbertPoly_mul_one_sub_pow_add, hilbertPoly]

Premises used: mul_assoc, HSub.hSub, pow_add, zero_add, Polynomial.hilbertPoly, Nat.sub_add_cancel, Polynomial.hilbertPoly_mul_one_sub_pow_add, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
rcases :
  ∀ (q : F[X]) (hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q)
    (hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q),
    (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
rcases exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp 1 with ⟨q, hq1, hq2⟩

Premises used: Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
simp : p = q * HSub.hSub (α := F[X]) X 1 ^ rootMultiplicity 1 p
⊢ p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p

Tactic:
simp only [mul_assoc, ← mul_pow, neg_mul, one_mul, neg_sub]

Premises used: neg_sub, mul_assoc, neg_mul, mul_pow, one_mul
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
⊢ p = q * HSub.hSub (α := F[X]) X 1 ^ rootMultiplicity 1 p

Tactic:
hq1.trans (mul_comm _ _)

Premises used: mul_comm, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
⊢ p = q * HSub.hSub (α := F[X]) X 1 ^ rootMultiplicity 1 p

Tactic:
exact hq1.trans (mul_comm _ _)

Premises used: mul_comm, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
⊢ p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p

Tactic:
have heq : p = q * (-1) ^ p.rootMultiplicity 1 * (1 - X) ^ p.rootMultiplicity 1 := by
    simp only [mul_assoc, ← mul_pow, neg_mul, one_mul, neg_sub]
    exact hq1.trans (mul_comm _ _)
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
nth_rw :
  ((q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).hilbertPoly (d - rootMultiplicity 1 p - 1 + 1)).natDegree =
    d - rootMultiplicity 1 p - 1
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
nth_rw 1 [heq, ← Nat.sub_add_cancel (le_of_lt hpd), hilbertPoly_mul_one_sub_pow_add,
    ← Nat.sub_add_cancel (Nat.le_sub_of_add_le' <| add_one_le_of_lt hpd)]

Premises used: le_of_lt, Nat.le_sub_of_add_le', Nat.add_one_le_of_lt, Nat.sub_add_cancel, Polynomial.hilbertPoly_mul_one_sub_pow_add
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
pn :
  natDegree.{u_1} (R := F)
      (match (motive := ℕ → F[X]) d - rootMultiplicity 1 p - 1 + 1 with
      | 0 => 0
      | d.succ =>
        ∑ i ∈ (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).support,
          HSMul.hSMul (β := F[X]) ((q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).coeff i)
            (preHilbertPoly F d i)) ≤
    d - rootMultiplicity 1 p - 1
p1 :
  Ne.{u_1 + 1} (α := F)
    (coeff
      (match (motive := ℕ → F[X]) d - rootMultiplicity 1 p - 1 + 1 with
      | 0 => 0
      | d.succ =>
        ∑ i ∈ (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).support,
          HSMul.hSMul (β := F[X]) ((q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).coeff i)
            (preHilbertPoly F d i))
      (d - rootMultiplicity 1 p - 1))
    0
⊢ natDegree.{u_1} (R := F)
      (match (motive := ℕ → F[X]) d - rootMultiplicity 1 p - 1 + 1 with
      | 0 => 0
      | d.succ =>
        ∑ i ∈ (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).support,
          HSMul.hSMul (β := F[X]) ((q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).coeff i)
            (preHilbertPoly F d i)) =
    d - rootMultiplicity 1 p - 1

Tactic:
apply natDegree_eq_of_le_of_coeff_ne_zero

Premises used: Polynomial.natDegree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
apply :
  ∀ x ∈ (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).support,
    (HSMul.hSMul (β := F[X]) ((q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).coeff x)
          (preHilbertPoly F (d - rootMultiplicity 1 p - 1) x)).natDegree ≤
      d - rootMultiplicity 1 p - 1
⊢ natDegree.{u_1} (R := F)
      (match (motive := ℕ → F[X]) d - rootMultiplicity 1 p - 1 + 1 with
      | 0 => 0
      | d.succ =>
        ∑ i ∈ (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).support,
          HSMul.hSMul (β := F[X]) ((q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).coeff i)
            (preHilbertPoly F d i)) ≤
    d - rootMultiplicity 1 p - 1

Tactic:
apply natDegree_sum_le_of_forall_le _ _ <| fun _ _ => ?_

Premises used: Polynomial.natDegree_sum_le_of_forall_le
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
x : ℕ
h : x ∈ (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).support
apply : natDegree (preHilbertPoly F (d - rootMultiplicity 1 p - 1) x) ≤ d - rootMultiplicity 1 p - 1
⊢ (HSMul.hSMul (β := F[X]) ((q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).coeff x)
        (preHilbertPoly F (d - rootMultiplicity 1 p - 1) x)).natDegree ≤
    d - rootMultiplicity 1 p - 1

Tactic:
apply le_trans (natDegree_smul_le _ _)

Premises used: Polynomial.natDegree_smul_le, le_trans
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
x : ℕ
h : x ∈ (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).support
rw rw₁ : d - rootMultiplicity 1 p - 1 ≤ d - rootMultiplicity 1 p - 1
⊢ natDegree (preHilbertPoly F (d - rootMultiplicity 1 p - 1) x) ≤ d - rootMultiplicity 1 p - 1

Tactic:
rw [natDegree_preHilbertPoly]

Premises used: Polynomial.natDegree_preHilbertPoly
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
⊢ Eq.{u_1 + 1} (α := (x : ℕ) → (a : F) → F) (fun (x : ℕ) (a : F) ↦ a) fun (x : ℕ) (a : F) ↦ a * HPow.hPow (α := F) 1 x

Tactic:
simp only [one_pow, mul_one]

Premises used: one_pow, mul_one
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
⊢ Eq.{u_1 + 1} (α := (x : ℕ) → (a : F) → F) (fun (x : ℕ) (a : F) ↦ a) fun (x : ℕ) (a : F) ↦ a * HPow.hPow (α := F) 1 x

Tactic:
have : (fun (x : ℕ) (a : F) => a) = fun x a => a * 1 ^ x := by simp only [one_pow, mul_one]
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
this :
  Eq.{u_1 + 1} (α := (x : ℕ) → (a : F) → F) (fun (x : ℕ) (a : F) ↦ a) fun (x : ℕ) (a : F) ↦ a * HPow.hPow (α := F) 1 x
p1 : ¬eval 1 q = 0 ∧ ¬(d - rootMultiplicity 1 p - 1)! = 0
⊢ Ne.{u_1 + 1} (α := F)
    (coeff
      (match (motive := ℕ → F[X]) d - rootMultiplicity 1 p - 1 + 1 with
      | 0 => 0
      | d.succ =>
        ∑ i ∈ (q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).support,
          HSMul.hSMul (β := F[X]) ((q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p)).coeff i)
            (preHilbertPoly F d i))
      (d - rootMultiplicity 1 p - 1))
    0

Tactic:
simp only [finsetSum_coeff, coeff_smul, smul_eq_mul, coeff_preHilbertPoly_self,
      ← Finset.sum_mul, ← sum_def _ (fun _ a => a), this, ← eval_eq_sum, eval_mul, eval_pow,
      eval_neg, eval_one, _root_.mul_eq_zero, pow_eq_zero_iff', neg_eq_zero, one_ne_zero, ne_eq,
      false_and, or_false, inv_eq_zero, cast_eq_zero, not_or]

Premises used: inv_eq_zero, Polynomial.eval_pow, false_and, pow_eq_zero_iff', neg_eq_zero, Polynomial.finsetSum_coeff, Polynomial.eval_mul, mul_eq_zero, ne_eq, not_or, Polynomial.coeff_smul, Nat.cast_eq_zero, Polynomial.sum_def, Polynomial.eval_eq_sum, Polynomial.eval_one, Polynomial.eval_neg, or_false, smul_eq_mul, one_ne_zero, Polynomial.coeff_preHilbertPoly_self, Finset.sum_mul
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
this :
  Eq.{u_1 + 1} (α := (x : ℕ) → (a : F) → F) (fun (x : ℕ) (a : F) ↦ a) fun (x : ℕ) (a : F) ↦ a * HPow.hPow (α := F) 1 x
⊢ ¬eval 1 q = 0 ∧ ¬(d - rootMultiplicity 1 p - 1)! = 0

Tactic:
⟨(not_iff_not.2 dvd_iff_isRoot).1 hq2, factorial_ne_zero _⟩

Premises used: not_iff_not, Iff.mpr, Nat.factorial_ne_zero, And.intro, Iff.mp, Polynomial.dvd_iff_isRoot
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ^ rootMultiplicity 1 p * q
hq2 : ¬HSub.hSub (α := F[X]) X ((C : (a : F) → F[X]) 1) ∣ q
heq : p = q * HPow.hPow (α := F[X]) (-1) (rootMultiplicity 1 p) * HSub.hSub (α := F[X]) 1 X ^ rootMultiplicity 1 p
this :
  Eq.{u_1 + 1} (α := (x : ℕ) → (a : F) → F) (fun (x : ℕ) (a : F) ↦ a) fun (x : ℕ) (a : F) ↦ a * HPow.hPow (α := F) 1 x
⊢ ¬eval 1 q = 0 ∧ ¬(d - rootMultiplicity 1 p - 1)! = 0

Tactic:
exact ⟨(not_iff_not.2 dvd_iff_isRoot).1 hq2, factorial_ne_zero _⟩
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
h : p = 0
⊢ Ne.{u_1 + 1} (α := F[X]) (hilbertPoly 0 d) 0

Tactic:
rw [h] at hh
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
h : p = 0
hh₁ : Ne.{u_1 + 1} (α := F[X]) (hilbertPoly 0 d) 0
⊢ p = 0

Tactic:
rw [h] at hh
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : Ne.{u_1 + 1} (α := F[X]) (hilbertPoly 0 d) 0
h : p = 0
⊢ False

Tactic:
hh (hilbertPoly_zero_left d)

Premises used: Polynomial.hilbertPoly_zero_left
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : Ne.{u_1 + 1} (α := F[X]) (hilbertPoly 0 d) 0
h : p = 0
⊢ False

Tactic:
exact hh (hilbertPoly_zero_left d)

Premises used: Polynomial.hilbertPoly_zero_left
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
⊢ p ≠ 0

Tactic:
have hp : p ≠ 0 := by
    intro h
    rw [h] at hh
    exact hh (hilbertPoly_zero_left d)
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
by_contra : ∀ (h : ¬rootMultiplicity 1 p < d), False
⊢ rootMultiplicity 1 p < d

Tactic:
by_contra h
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
h : ¬rootMultiplicity 1 p < d
⊢ False

Tactic:
hh (hilbertPoly_eq_zero_of_le_rootMultiplicity_one <| not_lt.1 h)

Premises used: Polynomial.hilbertPoly_eq_zero_of_le_rootMultiplicity_one, not_lt, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
h : ¬rootMultiplicity 1 p < d
⊢ False

Tactic:
exact hh (hilbertPoly_eq_zero_of_le_rootMultiplicity_one <| not_lt.1 h)

Premises used: Polynomial.hilbertPoly_eq_zero_of_le_rootMultiplicity_one, not_lt, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
⊢ rootMultiplicity 1 p < d

Tactic:
have hpd : p.rootMultiplicity 1 < d := by
    by_contra h
    exact hh (hilbertPoly_eq_zero_of_le_rootMultiplicity_one <| not_lt.1 h)
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt hp hpd

Premises used: Polynomial.natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt
-- Module: Mathlib.RingTheory.Polynomial.HilbertPoly
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
⊢ (p.hilbertPoly d).natDegree = d - rootMultiplicity 1 p - 1

Tactic:
exact natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt hp hpd

Premises used: Polynomial.natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
a : R
b : R[X]
P : R[X][X]
rw :
  (∃ (a_1 : R[X][X]) (b_1 : R[X][X]),
      HMul.hMul (β := R[X][X]) a_1
            ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) :
              R[X][X]) +
          b_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
        P) ↔
    eval a (eval b P) = 0
⊢ Membership.mem (γ := Ideal R[X][X])
      (Ideal.span
        (insert (α := R[X][X])
          ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X])
          {HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X])}))
      P ↔
    eval a (eval b P) = 0

Tactic:
rw [Ideal.mem_span_pair]

Premises used: Ideal.mem_span_pair
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
a : R
b : R[X]
P : R[X][X]
mp :
  (∃ (a_1 : R[X][X]) (b_1 : R[X][X]),
      HMul.hMul (β := R[X][X]) a_1
            ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) :
              R[X][X]) +
          b_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
        P) →
    eval a (eval b P) = 0
mpr :
  eval a (eval b P) = 0 →
    ∃ (a_2 : R[X][X]) (b_1 : R[X][X]),
      HMul.hMul (β := R[X][X]) a_2
            ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) :
              R[X][X]) +
          b_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
        P
⊢ (∃ (a_1 : R[X][X]) (b_1 : R[X][X]),
      HMul.hMul (β := R[X][X]) a_1
            ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) :
              R[X][X]) +
          b_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
        P) ↔
    eval a (eval b P) = 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
a : R
b : R[X]
P : R[X][X]
h :
  ∃ (a_1 : R[X][X]) (b_1 : R[X][X]),
    HMul.hMul (β := R[X][X]) a_1
          ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X]) +
        b_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
      P
mp :
  ∀ (w w_1 : R[X][X]),
    eval a
        (eval b
          (HMul.hMul (β := R[X][X]) w
              ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) :
                R[X][X]) +
            w_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]))) =
      0
⊢ eval a (eval b P) = 0

Tactic:
rcases h with ⟨_, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
a : R
b : R[X]
w w_1 : R[X][X]
⊢ eval a
      (eval b
        (HMul.hMul (β := R[X][X]) w
            ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) :
              R[X][X]) +
          w_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]))) =
    0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
mpr :
  ∀ (p : R[X]) (hp : eval b P = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * p),
    ∃ (a_1 : R[X][X]) (b_1 : R[X][X]),
      HMul.hMul (β := R[X][X]) a_1
            ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) :
              R[X][X]) +
          b_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
        P
⊢ ∃ (a_1 : R[X][X]) (b_1 : R[X][X]),
    HMul.hMul (β := R[X][X]) a_1
          ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X]) +
        b_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
      P

Tactic:
rcases dvd_iff_isRoot.mpr h with ⟨p, hp⟩

Premises used: Iff.mpr, Polynomial.dvd_iff_isRoot
-- Module: Mathlib.RingTheory.Polynomial.Ideal
Goal:
R : Type u_1
inst : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * p
mpr :
  ∀ (q : R[X][X])
    (hq :
      HSub.hSub (β := R[X][X]) P ((C : (a : R[X]) → R[X][X]) (eval b P) : R[X][X]) =
        HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) * q),
    ∃ (a_1 : R[X][X]) (b_1 : R[X][X]),
      HMul.hMul (β := R[X][X]) a_1
            ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) :
              R[X][X]) +
          b_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
        P
⊢ ∃ (a_1 : R[X][X]) (b_1 : R[X][X]),
    HMul.hMul (β := R[X][X]) a_1
          ((C : (a : R[X]) → R[X][X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) : R[X][X]) +
        b_1 * HSub.hSub (α := R[X][X]) (β := R[X][X]) X ((C : (a : R[X]) → R[X][X]) b : R[X][X]) =
      P

Tactic:
rcases @X_sub_C_dvd_sub_C_eval _ b _ P with ⟨q, hq⟩

Premises used: Polynomial.X_sub_C_dvd_sub_C_eval