awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw :
  (if p * q = 0 then 0
    else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q)) =
    rootMultiplicity x p + rootMultiplicity x q
rw₁ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    rootMultiplicity x p + rootMultiplicity x q
rw₂ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    (if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p) +
      rootMultiplicity x q
rw₃ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p + rootMultiplicity x q
rw₄ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
      if q = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q
rw₅ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (p * q) =
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
      multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q
rw₆ rw₇ :
  multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
      multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q =
    multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p +
      multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) q
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]

Premises used: HMul.hMul, Polynomial.prime_X_sub_C, Polynomial.rootMultiplicity_eq_multiplicity, multiplicity_mul, Polynomial.finiteMultiplicity_X_sub_C, if_neg
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p q : R[X]
x : R
hpq : p * q ≠ 0
have have₁ have₂ : ∀ (hp : p ≠ 0), rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
have₃ : ∀ (hp : p ≠ 0) (hq : q ≠ 0), rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q
⊢ rootMultiplicity x (p * q) = rootMultiplicity x p + rootMultiplicity x q

Tactic:
classical
  have hp : p ≠ 0 := left_ne_zero_of_mul hpq
  have hq : q ≠ 0 := right_ne_zero_of_mul hpq
  rw [rootMultiplicity_eq_multiplicity (p * q), if_neg hpq, rootMultiplicity_eq_multiplicity p,
    if_neg hp, rootMultiplicity_eq_multiplicity q, if_neg hq,
    multiplicity_mul (prime_X_sub_C x) (finiteMultiplicity_X_sub_C _ hpq)]

Premises used: Polynomial.prime_X_sub_C, multiplicity_mul, Polynomial.finiteMultiplicity_X_sub_C, if_neg
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h_1 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) = 0
⊢ Ne.{u + 1} (α := R[X]) 0 0

Tactic:
rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp

Premises used: Iff.mpr, Polynomial.mul_divByMonic_eq_iff_isRoot, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h_1 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) = 0
hp₁ : Ne.{u + 1} (α := R[X]) 0 0
⊢ p.IsRoot x

Tactic:
rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp

Premises used: Iff.mpr, Polynomial.mul_divByMonic_eq_iff_isRoot, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h_1 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) = 0
hp₁ : Ne.{u + 1} (α := R[X]) 0 0
hx₁ : p.IsRoot x
⊢ 0 < p.degree

Tactic:
rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp

Premises used: Iff.mpr, Polynomial.mul_divByMonic_eq_iff_isRoot, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h_1 : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) = 0
hp₁ : Ne.{u + 1} (α := R[X]) 0 0
hx₁ : p.IsRoot x
hpd₁ : 0 < p.degree
⊢ p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) = 0

Tactic:
rw [← mul_divByMonic_eq_iff_isRoot.2 hx, h, mul_zero] at hp

Premises used: Iff.mpr, Polynomial.mul_divByMonic_eq_iff_isRoot, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
this : Decidable (∃ (x : R), p.IsRoot x)
h_1 : ∃ (x : R), p.IsRoot x
x : R
hp : Ne.{u + 1} (α := R[X]) 0 0
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) = 0
⊢ False

Tactic:
hp rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
this : Decidable (∃ (x : R), p.IsRoot x)
h_1 : ∃ (x : R), p.IsRoot x
x : R
hp : Ne.{u + 1} (α := R[X]) 0 0
hx : p.IsRoot x
hpd : 0 < p.degree
h : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) = 0
⊢ False

Tactic:
exact hp rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
⊢ LT.lt (α := WithBot ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree

Tactic:
simpa using Nat.WithBot.one_le_iff_zero_lt.mpr hpd

Premises used: Iff.mpr, Nat.WithBot.one_le_iff_zero_lt
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
e_a : (x ::ₘ t).card = Add.add (↑t.card : ℕ) 1
⊢ (↑(x ::ₘ t).card : WithBot ℕ) = HAdd.hAdd (α := WithBot ℕ) (↑t.card : WithBot ℕ) 1

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
⊢ (x ::ₘ t).card = Add.add (↑t.card : ℕ) 1

Tactic:
mod_cast Multiset.card_cons _ _

Premises used: cast, Multiset.cons, Add.add, Nat.cast, Multiset.card_cons, Multiset.card, Eq.refl, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
⊢ (x ::ₘ t).card = Add.add (↑t.card : ℕ) 1

Tactic:
exact mod_cast Multiset.card_cons _ _

Premises used: Multiset.card_cons
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
rw :
  HAdd.hAdd (α := WithBot ℕ) 1 (↑t.card : WithBot ℕ) ≤
    1 + (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
⊢ HAdd.hAdd (α := WithBot ℕ) (↑t.card : WithBot ℕ) 1 ≤ p.degree

Tactic:
rw [← degree_add_divByMonic (monic_X_sub_C x) hdeg, degree_X_sub_C, add_comm]

Premises used: Polynomial.monic_X_sub_C, Polynomial.degree_X_sub_C, add_comm, Polynomial.degree_add_divByMonic
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
⊢ HAdd.hAdd (α := WithBot ℕ) 1 (↑t.card : WithBot ℕ) ≤
    1 + (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree

Tactic:
add_le_add (le_refl (1 : WithBot ℕ)) htd

Premises used: le_refl, add_le_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
⊢ HAdd.hAdd (α := WithBot ℕ) 1 (↑t.card : WithBot ℕ) ≤
    1 + (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree

Tactic:
exact add_le_add (le_refl (1 : WithBot ℕ)) htd

Premises used: le_refl, add_le_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
rw :
  rootMultiplicity a
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
| rootMultiplicity a p

Tactic:
rw [← mul_divByMonic_eq_iff_isRoot.mpr hx]

Premises used: Iff.mpr, Polynomial.mul_divByMonic_eq_iff_isRoot
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
conv_rhs :
  count a (x ::ₘ t) =
    rootMultiplicity a
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
⊢ count a (x ::ₘ t) = rootMultiplicity a p

Tactic:
conv_rhs => rw [← mul_divByMonic_eq_iff_isRoot.mpr hx]

Premises used: Iff.mpr, Polynomial.mul_divByMonic_eq_iff_isRoot
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
rw : count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t
⊢ count a (x ::ₘ t) =
    rootMultiplicity a
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))

Tactic:
rw [rootMultiplicity_mul (mul_ne_zero (X_sub_C_ne_zero x) hdiv0),
            rootMultiplicity_X_sub_C, ← htr a]

Premises used: Polynomial.rootMultiplicity_mul, Polynomial.rootMultiplicity_X_sub_C, mul_ne_zero, Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
pos : ∀ (ha : a = x), count a (x ::ₘ t) = 1 + count a t
neg : ∀ (ha : ¬a = x), count a (x ::ₘ t) = 0 + count a t
⊢ count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t

Tactic:
split_ifs with ha
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
ha : a = x
pos : count x (x ::ₘ t) = 1 + count x t
pos₁ : count x t + 1 = 1 + count x t
pos₂ pos₃ : 1 + count x t = 1 + count x t
⊢ count a (x ::ₘ t) = 1 + count a t

Tactic:
rw [ha, count_cons_self, add_comm]

Premises used: add_comm, Multiset.count_cons_self
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
t : Multiset R
htd : (↑t.card : WithBot ℕ) ≤ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree
htr :
  ∀ (a : R), count a t = rootMultiplicity a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
hdeg : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree ≤ p.degree
hdiv0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
a : R
ha : ¬a = x
neg : count a t = 0 + count a t
neg₁ neg₂ : count a t = count a t
⊢ count a (x ::ₘ t) = 0 + count a t

Tactic:
rw [count_cons_of_ne ha, zero_add]

Premises used: zero_add, Multiset.count_cons_of_ne
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ (x : R), p.IsRoot x)
h : ¬∃ (x : R), p.IsRoot x
a : R
rw : 0 = rootMultiplicity a p
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ count a 0 = rootMultiplicity a p

Tactic:
rw [count_zero, rootMultiplicity_eq_zero (not_exists.mp h a)]

Premises used: not_exists, Multiset.count_zero, Iff.mp, Polynomial.rootMultiplicity_eq_zero
-- Module: Mathlib.Algebra.Polynomial.RingDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
_x : (p : R[X]) ×' p ≠ 0
h_1 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y _x →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p_1 : R[X]
h_2 : p_1 ≠ 0
h_3 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p_1 h_2) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
p : R[X]
hp : p ≠ 0
h_4 :
  ∀ (y : (p : R[X]) ×' p ≠ 0),
    InvImage (fun (x1 x2 : ℕ) ↦ x1 < x2)
        (fun (x : (p : R[X]) ×' p ≠ 0) ↦
          PSigma.casesOn (β := fun (p : R[X]) ↦ p ≠ 0) (motive := fun (_x : (p : R[X]) ×' p ≠ 0) ↦ ℕ) x
            fun (p : R[X]) (x : p ≠ 0) ↦ p.natDegree)
        y (PSigma.mk (β := fun (x : R[X]) ↦ x ≠ 0) p hp) →
      ∃ (s : Multiset R),
        (↑s.card : WithBot ℕ) ≤ degree.{u} (R := R) y.1 ∧ ∀ (a : R), count a s = rootMultiplicity a y.1
h : ∃ (x : R), p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0
wf : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree < p.degree
apply :
  LT.lt (α := WithBot ℕ)
    (↑(p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree : WithBot ℕ)
    (↑p.natDegree : WithBot ℕ)
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree < p.natDegree

Tactic:
apply (Nat.cast_lt (α := WithBot ℕ)).mp

Premises used: Iff.mp, Nat.cast_lt