awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
a : R
inst : CommRing R
p : R[X]
rw : (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])).IsRoot a
rw₁ : eval a (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])) = 0
rw₂ : eval a p - eval a ((C : (a : R) → R[X]) (eval a p)) = 0
rw₃ : eval a p - eval a p = 0
rw₄ rw₅ : Eq.{u + 1} (α := R) 0 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
    HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval a p) : R[X])

Tactic:
rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]

Premises used: Polynomial.eval_C, sub_self, Polynomial.IsRoot, Polynomial.dvd_iff_isRoot, Polynomial.eval_sub
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
rw : p %ₘ X = p %ₘ HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0)
rw₁ : p %ₘ X = p %ₘ HSub.hSub (α := R[X]) X 0
rw₂ rw₃ : p %ₘ X = p %ₘ X
⊢ p %ₘ X = (C : (a : R) → R[X]) (eval 0 p)

Tactic:
rw [← modByMonic_X_sub_C_eq_C_eval, C_0, sub_zero]

Premises used: sub_zero, Polynomial.C_0, Polynomial.modByMonic_X_sub_C_eq_C_eval
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
rw : eval₂ f x (p - q * (p /ₘ q)) = eval₂ f x p
rw₁ : eval₂ f x p - eval₂ f x (q * (p /ₘ q)) = eval₂ f x p
rw₂ : eval₂ f x p - eval₂ f x q * eval₂ f x (p /ₘ q) = eval₂ f x p
rw₃ : eval₂ f x p - 0 * eval₂ f x (p /ₘ q) = eval₂ f x p
rw₄ : eval₂ f x p - 0 = eval₂ f x p
rw₅ rw₆ : eval₂ f x p = eval₂ f x p
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p

Tactic:
rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]

Premises used: sub_zero, MulZeroClass.zero_mul, Polynomial.eval₂_sub, Polynomial.modByMonic_eq_sub_mul_div, Polynomial.eval₂_mul
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
a b : R
p : R[X]
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]) ∣
    HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval b p) : R[X])
⊢ a - b ∣ eval a p - eval b p

Tactic:
simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C]
      using (_root_.map_dvd (evalRingHom a)) this

Premises used: Polynomial.eval_C, Polynomial.eval_X, map_dvd, Polynomial.evalRingHom, Polynomial.eval_sub, Polynomial.coe_evalRingHom
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
a b : R
p : R[X]
suffices :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]) ∣
    HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval b p) : R[X])
⊢ a - b ∣ eval a p - eval b p

Tactic:
suffices X - C b ∣ p - C (p.eval b) by
    simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C]
      using (_root_.map_dvd (evalRingHom a)) this
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
a b : R
p : R[X]
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]) ∣
    HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (eval b p) : R[X])

Tactic:
simp [dvd_iff_isRoot]

Premises used: Polynomial.dvd_iff_isRoot
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
h : p.IsRoot x
⊢ x ∣ p.coeff 0

Tactic:
simpa [h.eq_zero, coeff_zero_eq_eval_zero] using sub_dvd_eval_sub 0 x p

Premises used: Polynomial.coeff_zero_eq_eval_zero, Polynomial.sub_dvd_eval_sub, Polynomial.IsRoot.eq_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
⊢ rootMultiplicity x p = 0 ↔ p.IsRoot x → p = 0

Tactic:
simp only [rootMultiplicity_eq_multiplicity, ite_eq_left_iff, multiplicity_eq_zero,
    dvd_iff_isRoot, not_imp_not]

Premises used: multiplicity_eq_zero, ite_eq_left_iff, Polynomial.rootMultiplicity_eq_multiplicity, Polynomial.dvd_iff_isRoot, not_imp_not
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
⊢ rootMultiplicity x p = 0 ↔ p.IsRoot x → p = 0

Tactic:
classical
  simp only [rootMultiplicity_eq_multiplicity, ite_eq_left_iff, multiplicity_eq_zero,
    dvd_iff_isRoot, not_imp_not]

Premises used: multiplicity_eq_zero, ite_eq_left_iff, Polynomial.rootMultiplicity_eq_multiplicity, Polynomial.dvd_iff_isRoot, not_imp_not
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
h : ¬p.IsRoot x
⊢ rootMultiplicity x p = 0

Tactic:
rootMultiplicity_eq_zero_iff.2 fun h' => (h h').elim

Premises used: Iff.mpr, Polynomial.rootMultiplicity_eq_zero_iff, False.elim
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
rw : rootMultiplicity x p ≠ 0 ↔ p ≠ 0 ∧ p.IsRoot x
rw₁ : ¬rootMultiplicity x p = 0 ↔ p ≠ 0 ∧ p.IsRoot x
rw₂ : ¬(p.IsRoot x → p = 0) ↔ p ≠ 0 ∧ p.IsRoot x
rw₃ : p.IsRoot x ∧ ¬p = 0 ↔ p ≠ 0 ∧ p.IsRoot x
rw₄ rw₅ : ¬p = 0 ∧ p.IsRoot x ↔ p ≠ 0 ∧ p.IsRoot x
⊢ 0 < rootMultiplicity x p ↔ p ≠ 0 ∧ p.IsRoot x

Tactic:
rw [pos_iff_ne_zero, Ne, rootMultiplicity_eq_zero_iff, Classical.not_imp, and_comm]

Premises used: Polynomial.rootMultiplicity_eq_zero_iff, Ne, and_comm, Classical.not_imp, pos_iff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
hp : p ≠ 0
x : R
⊢ 0 < rootMultiplicity x p ↔ p.IsRoot x

Tactic:
rootMultiplicity_pos'.trans (and_iff_right hp)

Premises used: and_iff_right, Iff.trans, Polynomial.rootMultiplicity_pos'
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
⊢ Nontrivial R

Tactic:
haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
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]) ^ rootMultiplicity a p
⊢ eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0

Tactic:
rw [Ne, ← IsRoot, ← dvd_iff_isRoot]

Premises used: Polynomial.IsRoot, Ne, Polynomial.dvd_iff_isRoot
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
q : R[X]
hq :
  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]) * q
⊢ 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:
have := pow_mul_divByMonic_rootMultiplicity_eq p a
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this_1 : Nontrivial R
q : R[X]
hq :
  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]) * q
this :
  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
⊢ 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 + 1) *
      q =
    p

Tactic:
rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this

Premises used: pow_succ, mul_assoc, Polynomial.rootMultiplicity_eq_multiplicity, if_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this_1 : Nontrivial R
q : R[X]
hq :
  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]) * q
this :
  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 + 1) *
      q =
    p
rw : LT.lt (α := WithBot ℕ) 0 1
⊢ 0 < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree

Tactic:
rw [degree_X_sub_C]

Premises used: Polynomial.degree_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this_1 : Nontrivial R
q : R[X]
hq :
  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]) * q
this :
  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 + 1) *
      q =
    p
⊢ LT.lt (α := WithBot ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this_1 : Nontrivial R
q : R[X]
hq :
  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]) * q
this :
  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 + 1) *
      q =
    p
⊢ False

Tactic:
exact
    (finiteMultiplicity_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
      (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
      (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)

Premises used: Polynomial.monic_X_sub_C, dvd_of_mul_right_eq, Nat.lt_succ_self, Polynomial.finiteMultiplicity_of_degree_pos_of_monic, FiniteMultiplicity.not_pow_dvd_of_multiplicity_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
a : R
hp : p ≠ 0
haveI haveI₁ haveI₂ :
  ∀ (this : Nontrivial R),
    eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0
haveI₃ :
  ∀ (this : Nontrivial R),
    ¬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]) ^ rootMultiplicity a p
haveI₄ :
  ∀ (this : Nontrivial R) (q : R[X])
    (hq :
      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]) * q),
    False
haveI₅ :
  ∀ (this : Nontrivial R) (q : R[X])
    (hq :
      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]) * q)
    (this :
      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),
    False
haveI₆ :
  ∀ (this : Nontrivial R) (q : R[X])
    (hq :
      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]) * q)
    (this :
      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 + 1) *
          q =
        p),
    False
⊢ eval a (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ rootMultiplicity a p) ≠ 0

Tactic:
classical
  haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
  rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
  rintro ⟨q, hq⟩
  have := pow_mul_divByMonic_rootMultiplicity_eq p a
  rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
  exact
    (finiteMultiplicity_of_degree_pos_of_monic
      (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
      (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
      (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)

Premises used: pow_succ, Polynomial.IsRoot, mul_assoc, Ne, Polynomial.rootMultiplicity_eq_multiplicity, Polynomial.dvd_iff_isRoot, if_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hq : q.Monic
rw : q ∣ p * q
⊢ p * q %ₘ q = 0

Tactic:
rw [modByMonic_eq_zero_iff_dvd hq]

Premises used: Polynomial.modByMonic_eq_zero_iff_dvd
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hq : q.Monic
⊢ q ∣ p * q

Tactic:
dvd_mul_left q p

Premises used: dvd_mul_left
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hq : q.Monic
⊢ q ∣ p * q

Tactic:
exact dvd_mul_left q p

Premises used: dvd_mul_left
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : q ∣ p₁ - p₂
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : q ∣ p₁ - p₂
h_1 : Nontrivial R
obtain : ∀ (f : R[X]) (sub_eq : p₁ - p₂ = q * f), p₁ %ₘ q = p₂ %ₘ q
⊢ p₁ %ₘ q = p₂ %ₘ q

Tactic:
obtain ⟨f, sub_eq⟩ := h
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
⊢ p₁ %ₘ q = p₂ %ₘ q

Tactic:
(div_modByMonic_unique (p₂ /ₘ q + f) _ hq ⟨?_, degree_modByMonic_lt _ hq⟩).2

Premises used: Polynomial.divByMonic, Polynomial.div_modByMonic_unique, And.right, HAdd.hAdd, And.intro, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
refine : p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁
⊢ p₁ %ₘ q = p₂ %ₘ q

Tactic:
refine (div_modByMonic_unique (p₂ /ₘ q + f) _ hq ⟨?_, degree_modByMonic_lt _ hq⟩).2

Premises used: Polynomial.divByMonic, Polynomial.div_modByMonic_unique, And.right, HAdd.hAdd, And.intro, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
hq : q.Monic
h : Nontrivial R
f : R[X]
sub_eq : p₁ - p₂ = q * f
rw : p₂ %ₘ q + q * (p₂ /ₘ q + f) = q * f + p₂
rw₁ : p₂ %ₘ q + (q * (p₂ /ₘ q) + q * f) = q * f + p₂
rw₂ : p₂ %ₘ q + q * (p₂ /ₘ q) + q * f = q * f + p₂
rw₃ : p₂ + q * f = q * f + p₂
rw₄ rw₅ : q * f + p₂ = q * f + p₂
⊢ p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁

Tactic:
rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div, add_comm]

Premises used: add_assoc, add_comm, sub_eq_iff_eq_add, Polynomial.modByMonic_add_div, Iff.mp, mul_add
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
pos : ∀ (hq : q.Monic), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
neg : ∀ (hq : ¬q.Monic), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
by_cases hq : q.Monic

Premises used: Polynomial.Monic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
pos : ∀ (hR : Subsingleton R), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
pos₁ : ∀ (hR : Nontrivial R), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
rw : p₁ %ₘ q + p₂ %ₘ q + (q * (p₁ /ₘ q) + q * (p₂ /ₘ q)) = p₁ + p₂
rw₁ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂ %ₘ q + q * (p₂ /ₘ q)) = p₁ + p₂
rw₂ : q * (p₁ /ₘ q) + (p₁ %ₘ q + (p₂ %ₘ q + q * (p₂ /ₘ q))) = p₁ + p₂
rw₃ : q * (p₁ /ₘ q) + (p₁ %ₘ q + p₂) = p₁ + p₂
rw₄ : q * (p₁ /ₘ q) + p₁ %ₘ q + p₂ = p₁ + p₂
rw₅ : p₁ %ₘ q + q * (p₁ /ₘ q) + p₂ = p₁ + p₂
rw₆ rw₇ : p₁ + p₂ = p₁ + p₂
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂

Tactic:
rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div]

Premises used: HMul.hMul, add_left_comm, add_assoc, add_comm, Polynomial.modByMonic_add_div, mul_add
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
exact
      (div_modByMonic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
          ⟨by
            rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div],
            (degree_add_le _ _).trans_lt
              (max_lt (degree_modByMonic_lt _ hq) (degree_modByMonic_lt _ hq))⟩).2

Premises used: Polynomial.divByMonic, max_lt, Polynomial.div_modByMonic_unique, And.right, HAdd.hAdd, And.intro, Polynomial.degree_modByMonic_lt, Polynomial.degree_add_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
q p₁ p₂ : R[X]
hq : ¬q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
simp_rw [modByMonic_eq_of_not_monic _ hq]

Premises used: Polynomial.modByMonic_eq_of_not_monic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
rw : -p %ₘ q + p %ₘ q = 0
rw₁ : (-p + p) %ₘ q = 0
rw₂ : 0 %ₘ q = 0
rw₃ rw₄ : Eq.{u + 1} (α := R[X]) 0 0
⊢ -p %ₘ q = -(p %ₘ q)

Tactic:
rw [eq_neg_iff_add_eq_zero, ← add_modByMonic, neg_add_cancel, zero_modByMonic]

Premises used: neg_add_cancel, eq_neg_iff_add_eq_zero, Polynomial.add_modByMonic, Polynomial.zero_modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
⊢ (p₁ - p₂) %ₘ q = p₁ %ₘ q - p₂ %ₘ q

Tactic:
simp [sub_eq_add_neg, add_modByMonic, neg_modByMonic]

Premises used: sub_eq_add_neg, Polynomial.neg_modByMonic, Polynomial.add_modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
pos : ∀ (h : ¬q.Monic), p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
neg : ∀ (h : q.Monic), p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

Tactic:
by_cases! h : ¬ q.Monic

Premises used: Polynomial.Monic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : ¬q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

Tactic:
simp [Polynomial.modByMonic_eq_of_not_monic _ h]

Premises used: Polynomial.modByMonic_eq_of_not_monic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
neg : q ∣ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q)
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

Tactic:
apply Polynomial.modByMonic_eq_of_dvd_sub h

Premises used: Polynomial.modByMonic_eq_of_dvd_sub
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)

Tactic:
ring
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)

Tactic:
have : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = (p₁ %ₘ q) * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q) := by ring
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
neg : q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q)

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
neg : q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q)
neg₁ : q ∣ p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)

Tactic:
apply dvd_add

Premises used: dvd_add
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
neg : q ∣ p₂ - p₂ %ₘ q
⊢ q ∣ p₁ %ₘ q * (p₂ - p₂ %ₘ q)

Tactic:
apply dvd_mul_of_dvd_right

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₂ - p₂ %ₘ q

Tactic:
simp [Polynomial.modByMonic_eq_sub_mul_div]

Premises used: Polynomial.modByMonic_eq_sub_mul_div
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
neg : q ∣ p₁ - p₁ %ₘ q
⊢ q ∣ p₂ * (p₁ - p₁ %ₘ q)

Tactic:
apply dvd_mul_of_dvd_right

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
this : p₁ * p₂ - p₁ %ₘ q * (p₂ %ₘ q) = p₁ %ₘ q * (p₂ - p₂ %ₘ q) + p₂ * (p₁ - p₁ %ₘ q)
⊢ q ∣ p₁ - p₁ %ₘ q

Tactic:
simp [Polynomial.modByMonic_eq_sub_mul_div]

Premises used: Polynomial.modByMonic_eq_sub_mul_div
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
inl :
  eval t (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t 0) =
    (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inr :
  ∀ (hp : p ≠ 0),
    eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
      (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
⊢ eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff

Tactic:
obtain rfl | hp := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
t : R
inl : eval t 0 = (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inl₁ : 0 = (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
inl₂ : Eq.{u + 1} (α := R) 0 (trailingCoeff 0)
inl₃ inl₄ : Eq.{u + 1} (α := R) 0 0
⊢ eval t (0 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t 0) =
    (comp 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff

Tactic:
rw [zero_divByMonic, eval_zero, zero_comp, trailingCoeff_zero]

Premises used: Polynomial.zero_comp, Polynomial.zero_divByMonic, Polynomial.eval_zero, Polynomial.trailingCoeff_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hp : p ≠ 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    p

Tactic:
have mul_eq := p.pow_mul_divByMonic_rootMultiplicity_eq t
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hp : p ≠ 0
mul_eq :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    p
inr :
  let m := rootMultiplicity t p;
  ∀
    (mul_eq :
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) =
        p),
    eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) =
      (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
⊢ eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff

Tactic:
set m := p.rootMultiplicity t

Premises used: Polynomial.rootMultiplicity