awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
inr :
  (if Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r)) =
    0
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0

Tactic:
rw [rootMultiplicity_eq_multiplicity]

Premises used: Polynomial.rootMultiplicity_eq_multiplicity
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
pos : ∀ (hr : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])), Eq (α := ℕ) 0 0
neg :
  ∀ (hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])),
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r) = 0
⊢ (if Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r)) =
    0

Tactic:
split_ifs with hr
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
hr : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) r) <
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) r) <
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree

Tactic:
have h : natDegree (C r) < natDegree (X - C a) := by simp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
r a : R
h_1 : Nontrivial R
hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])
h :
  natDegree.{u} (R := R) ((C : (a : R) → R[X]) r) <
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree
⊢ multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r) = 0

Tactic:
simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]

Premises used: Iff.mpr, Polynomial.monic_X_sub_C, multiplicity_eq_zero, Polynomial.Monic.not_dvd_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
r a : R
h : Nontrivial R
inr inr₁ inr₂ :
  (if Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r)) =
    0
pos : ∀ (hr : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])), Eq (α := ℕ) 0 0
neg neg₁ :
  ∀ (hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])),
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r) = 0
neg₂ :
  ∀ (hr : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]))
    (h :
      natDegree.{u} (R := R) ((C : (a : R) → R[X]) r) <
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree),
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ((C : (a : R) → R[X]) r) = 0
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0

Tactic:
classical
  rw [rootMultiplicity_eq_multiplicity]
  split_ifs with hr
  · rfl
  have h : natDegree (C r) < natDegree (X - C a) := by simp
  simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]

Premises used: Polynomial.rootMultiplicity_eq_multiplicity
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : p = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p ∣ p

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
rw :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
      multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p ∣
    p
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p ∣ p

Tactic:
rw [rootMultiplicity_eq_multiplicity, if_neg h]

Premises used: Polynomial.rootMultiplicity_eq_multiplicity, if_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
      multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p ∣
    p

Tactic:
apply pow_multiplicity_dvd

Premises used: pow_multiplicity_dvd
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
rw :
  (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
      if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p) ∣
    p
rw₁ rw₂ rw₃ rw₄ :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
      multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p ∣
    p
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p ∣ p

Tactic:
classical
    rw [rootMultiplicity_eq_multiplicity, if_neg h]; apply pow_multiplicity_dvd

Premises used: pow_multiplicity_dvd, Polynomial.rootMultiplicity_eq_multiplicity, if_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).Monic

Tactic:
have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).Monic
rw :
  0 +
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p)
| p

Tactic:
rw [← modByMonic_add_div p, (modByMonic_eq_zero_iff_dvd this).2 (pow_rootMultiplicity_dvd _ _)]

Premises used: Iff.mpr, Polynomial.pow_rootMultiplicity_dvd, Polynomial.modByMonic_eq_zero_iff_dvd, Polynomial.modByMonic_add_div
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).Monic
conv_rhs :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) =
    0 +
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p)
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) =
    p

Tactic:
conv_rhs =>
    rw [← modByMonic_add_div p, (modByMonic_eq_zero_iff_dvd this).2 (pow_rootMultiplicity_dvd _ _)]

Premises used: Iff.mpr, Polynomial.pow_rootMultiplicity_dvd, Polynomial.modByMonic_eq_zero_iff_dvd, Polynomial.modByMonic_add_div
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p).Monic
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) =
    0 +
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
hp : p ≠ 0
a : R
rw :
  ∃ (q : R[X]),
    p =
        HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
            multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p *
          q ∧
      ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
⊢ ∃ (q : R[X]),
    p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q ∧
      ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q

Tactic:
rw [rootMultiplicity_eq_multiplicity, if_neg hp]

Premises used: Polynomial.rootMultiplicity_eq_multiplicity, if_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ (q : R[X]),
    p =
        HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
            multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p *
          q ∧
      ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q

Tactic:
apply (finiteMultiplicity_X_sub_C a hp).exists_eq_pow_mul_and_not_dvd

Premises used: FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd, Polynomial.finiteMultiplicity_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
hp : p ≠ 0
a : R
rw :
  ∃ (q : R[X]),
    p =
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
            if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p) *
          q ∧
      ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
rw₁ rw₂ rw₃ :
  ∃ (q : R[X]),
    p =
        HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
            multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p *
          q ∧
      ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q
⊢ ∃ (q : R[X]),
    p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p * q ∧
      ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ q

Tactic:
classical
  rw [rootMultiplicity_eq_multiplicity, if_neg hp]
  apply (finiteMultiplicity_X_sub_C a hp).exists_eq_pow_mul_and_not_dvd

Premises used: FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd, Polynomial.rootMultiplicity_eq_multiplicity, Polynomial.finiteMultiplicity_X_sub_C, if_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h : Nontrivial R
rw :
  eval a
      (p -
        HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))) =
    eval a p
rw₁ :
  eval a p -
      eval a
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))) =
    eval a p
rw₂ :
  eval a p -
      eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) *
        eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    eval a p
rw₃ :
  eval a p -
      (eval a X - eval a ((C : (a : R) → R[X]) a)) *
        eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    eval a p
rw₄ :
  eval a p -
      (a - eval a ((C : (a : R) → R[X]) a)) *
        eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    eval a p
rw₅ : eval a p - (a - a) * eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
rw₆ : eval a p - 0 * eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
rw₇ : eval a p - 0 = eval a p
rw₈ rw₉ : eval a p = eval a p
⊢ eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p

Tactic:
rw [modByMonic_eq_sub_mul_div, eval_sub, eval_mul, eval_sub, eval_X,
      eval_C, sub_self, zero_mul, sub_zero]

Premises used: Polynomial.eval_C, sub_self, sub_zero, Polynomial.eval_X, MulZeroClass.zero_mul, Polynomial.modByMonic_eq_sub_mul_div, Polynomial.eval_mul, Polynomial.eval_sub
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h : Nontrivial R
⊢ eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p

Tactic:
have h : (p %ₘ (X - C a)).eval a = p.eval a := by
    rw [modByMonic_eq_sub_mul_div, eval_sub, eval_mul, eval_sub, eval_X,
      eval_C, sub_self, zero_mul, sub_zero]
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
⊢ (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1

Tactic:
have : degree (p %ₘ (X - C a)) < 1 :=
    degree_X_sub_C a ▸ degree_modByMonic_lt p (monic_X_sub_C a)
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
this : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1
revert :
  ∀ (this : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1),
    (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ 0
⊢ (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ 0

Tactic:
revert this
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
bot : ∀ (this : LT.lt (α := WithBot ℕ) ⊥ 1), LE.le (α := WithBot ℕ) ⊥ 0
coe : ∀ (a : ℕ) (this : (↑a : WithBot ℕ) < 1), (↑a : WithBot ℕ) ≤ 0
⊢ ∀ (this : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1),
    (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ 0

Tactic:
cases degree (p %ₘ (X - C a))

Premises used: Polynomial.C, HSub.hSub, Polynomial.degree, Polynomial.modByMonic, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
⊢ ∀ (this : LT.lt (α := WithBot ℕ) ⊥ 1), LE.le (α := WithBot ℕ) ⊥ 0

Tactic:
fun _ => bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
⊢ ∀ (this : LT.lt (α := WithBot ℕ) ⊥ 1), LE.le (α := WithBot ℕ) ⊥ 0

Tactic:
exact fun _ => bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
a_1 : ℕ
⊢ ∀ (this : (↑a_1 : WithBot ℕ) < 1), (↑a_1 : WithBot ℕ) ≤ 0

Tactic:
fun h => WithBot.coe_le_coe.2 (Nat.le_of_lt_succ (WithBot.coe_lt_coe.1 h))

Premises used: Iff.mpr, WithBot.coe_le_coe, WithBot.coe_lt_coe, Nat.le_of_lt_succ, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
a_1 : ℕ
⊢ ∀ (this : (↑a_1 : WithBot ℕ) < 1), (↑a_1 : WithBot ℕ) ≤ 0

Tactic:
exact fun h => WithBot.coe_le_coe.2 (Nat.le_of_lt_succ (WithBot.coe_lt_coe.1 h))

Premises used: Iff.mpr, WithBot.coe_le_coe, WithBot.coe_lt_coe, Nat.le_of_lt_succ, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
this : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1
⊢ (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ 0

Tactic:
have : degree (p %ₘ (X - C a)) ≤ 0 := by
    revert this
    cases degree (p %ₘ (X - C a))
    · exact fun _ => bot_le
    · exact fun h => WithBot.coe_le_coe.2 (Nat.le_of_lt_succ (WithBot.coe_lt_coe.1 h))
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
this_1 : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1
this : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ 0
⊢ (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff 0 = eval a p

Tactic:
rw [eq_C_of_degree_le_zero this, eval_C] at h

Premises used: Polynomial.eval_C, Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
this_1 : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1
this : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ 0
h₁ : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff 0 = eval a p
⊢ (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1

Tactic:
rw [eq_C_of_degree_le_zero this, eval_C] at h

Premises used: Polynomial.eval_C, Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : eval a (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = eval a p
this_1 : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1
this : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ 0
h₁ : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff 0 = eval a p
this₁ : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1
⊢ (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ 0

Tactic:
rw [eq_C_of_degree_le_zero this, eval_C] at h

Premises used: Polynomial.eval_C, Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
h_1 : Nontrivial R
h : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff 0 = eval a p
this_1 : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < 1
this : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree ≤ 0
rw :
  Eq (α := R[X])
    ((C : (a : R) → R[X]) ((p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff 0) : R[X])
    ((C : (a : R) → R[X]) (eval a p) : R[X])
rw₁ rw₂ : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval a p) : R[X]) ((C : (a : R) → R[X]) (eval a p) : R[X])
⊢ p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = (C : (a : R) → R[X]) (eval a p)

Tactic:
rw [eq_C_of_degree_le_zero this, h]

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    p
rw :
  eval a
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))) =
    0
rw₁ :
  eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) *
      eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    0
rw₂ :
  (eval a X - eval a ((C : (a : R) → R[X]) a)) *
      eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    0
rw₃ :
  (a - eval a ((C : (a : R) → R[X]) a)) *
      eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    0
rw₄ : (a - a) * eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0
rw₅ : 0 * eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) = 0
rw₆ rw₇ : Eq.{u + 1} (α := R) 0 0
⊢ eval a p = 0

Tactic:
rw [← h, eval_mul, eval_sub, eval_X, eval_C, sub_self, zero_mul]

Premises used: Polynomial.eval_C, sub_self, Polynomial.eval_X, MulZeroClass.zero_mul, Polynomial.eval_mul, Polynomial.eval_sub
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : eval a p = 0
rw :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
| p

Tactic:
rw [← modByMonic_add_div p, modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]

Premises used: Polynomial.C_0, zero_add, Polynomial.modByMonic_X_sub_C_eq_C_eval, Polynomial.modByMonic_add_div
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : eval a p = 0
conv_rhs :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    p
conv_rhs₁ :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    p

Tactic:
conv_rhs => rw [← modByMonic_add_div p, modByMonic_X_sub_C_eq_C_eval, h, C_0, zero_add]

Premises used: Polynomial.C_0, zero_add, Polynomial.modByMonic_X_sub_C_eq_C_eval, Polynomial.modByMonic_add_div
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
rwa : ∀ (h : p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 0), p.IsRoot a
rwa₁ : ∀ (h : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval a p) : R[X]) (0 : R[X])), p.IsRoot a
rwa₂ : ∀ (h : Eq (α := R[X]) ((C : (a : R) → R[X]) (eval a p) : R[X]) ((C : (a : R) → R[X]) 0 : R[X])), p.IsRoot a
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : eval a p = 0), p.IsRoot a
⊢ p.IsRoot a

Tactic:
rwa [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval, ← C_0,
      C_inj] at h

Premises used: Polynomial.monic_X_sub_C, Polynomial.C_inj, Polynomial.C_0, Polynomial.modByMonic_eq_zero_iff_dvd, Polynomial.modByMonic_X_sub_C_eq_C_eval
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
h : p.IsRoot a
rw rw₁ : p = p
⊢ p =
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))

Tactic:
rw [mul_divByMonic_eq_iff_isRoot.2 h]

Premises used: Iff.mpr, Polynomial.mul_divByMonic_eq_iff_isRoot