awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
norm_cast : g.natDegree ≤ g.natDegree + (q - f /ₘ g).natDegree
⊢ (↑g.natDegree : WithBot ℕ) ≤
    HAdd.hAdd (α := WithBot ℕ) (↑g.natDegree : WithBot ℕ) (↑(q - f /ₘ g).natDegree : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.natDegree ≤ g.natDegree + (q - f /ₘ g).natDegree

Tactic:
Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.natDegree ≤ g.natDegree + (q - f /ₘ g).natDegree

Tactic:
exact Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
rw : g.leadingCoeff * (q - f /ₘ g).leadingCoeff ≠ 0
⊢ g.degree + (q - f /ₘ g).degree = (r - f %ₘ g).degree

Tactic:
rw [h₂, degree_mul']

Premises used: Polynomial.degree_mul'
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.leadingCoeff * (q - f /ₘ g).leadingCoeff ≠ 0

Tactic:
simpa [Monic.def.1 hg]

Premises used: Iff.mp, Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
⊢ q - f /ₘ g = 0

Tactic:
have h₅ : q - f /ₘ g = 0 :=
    _root_.by_contradiction fun hqf =>
      not_le_of_gt h₄ <|
        calc
          degree g ≤ degree g + degree (q - f /ₘ g) := by
            rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]
            norm_cast
            exact Nat.le_add_right _ _
          _ = degree (r - f %ₘ g) := by rw [h₂, degree_mul']; simpa [Monic.def.1 hg]
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
h₅ : q - f /ₘ g = 0
⊢ r - f %ₘ g = 0

Tactic:
simpa [h₅] using h₁
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
h₅ : q - f /ₘ g = 0
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
exact ⟨Eq.symm <| eq_of_sub_eq_zero h₅, Eq.symm <| eq_of_sub_eq_zero <| by simpa [h₅] using h₁⟩
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
⊢ Nontrivial R

Tactic:
haveI : Nontrivial R := f.domain_nontrivial
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this : Nontrivial R
rw : map f p = map f (p %ₘ q) + map f (q * (p /ₘ q))
rw₁ : map f p = map f (p %ₘ q + q * (p /ₘ q))
rw₂ rw₃ : map f p = map f p
⊢ map f p = map f (p %ₘ q) + map f q * map f (p /ₘ q)

Tactic:
rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div]

Premises used: Polynomial.map_mul, Polynomial.map_add, Polynomial.modByMonic_add_div
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this : Nontrivial R
rw : Ne.{v + 1} (α := S) 1 0
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) q.leadingCoeff : S) (0 : S)

Tactic:
rw [Monic.def.1 hq, f.map_one]

Premises used: RingHom.map_one, Iff.mp, Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this : Nontrivial R
⊢ Ne.{v + 1} (α := S) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this : Nontrivial R
⊢ Ne.{v + 1} (α := S) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this : Nontrivial R
⊢ map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q)

Tactic:
have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q) :=
    div_modByMonic_unique ((p /ₘ q).map f) _ (hq.map f)
      ⟨Eq.symm <| by rw [← Polynomial.map_mul, ← Polynomial.map_add, modByMonic_add_div],
        calc
          _ ≤ degree (p %ₘ q) := degree_map_le
          _ < degree q := degree_modByMonic_lt _ hq
          _ = _ :=
            Eq.symm <|
              degree_map_eq_of_leadingCoeff_ne_zero _
                (by rw [Monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this_1 : Nontrivial R
this : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q)
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q

Tactic:
⟨this.1.symm, this.2.symm⟩

Premises used: And.right, And.left, And.intro, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
h : Nontrivial S
this_1 : Nontrivial R
this : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q)
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q

Tactic:
exact ⟨this.1.symm, this.2.symm⟩
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
⊢ map f (p /ₘ q) = map f p /ₘ map f q

Tactic:
(map_mod_divByMonic f hq).1

Premises used: And.left, Polynomial.map_mod_divByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
p q : R[X]
inst_1 : Ring S
f : R →+* S
hq : q.Monic
⊢ map f (p %ₘ q) = map f p %ₘ map f q

Tactic:
(map_mod_divByMonic f hq).2

Premises used: And.right, Polynomial.map_mod_divByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
rw : q ∣ q * (p /ₘ q)
⊢ q ∣ p

Tactic:
rw [← modByMonic_add_div p q, h, zero_add]

Premises used: zero_add, Polynomial.modByMonic_add_div
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
⊢ q ∣ q * (p /ₘ q)

Tactic:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
⊢ q ∣ q * (p /ₘ q)

Tactic:
exact dvd_mul_right _ _

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

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

Tactic:
obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h

Premises used: exists_eq_mul_right_of_dvd
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
by_contra : ∀ (hpq0 : ¬p %ₘ q = 0), False
⊢ p %ₘ q = 0

Tactic:
by_contra hpq0
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
rw : p - q * (p /ₘ q) = q * (r - p /ₘ q)
rw₁ : p - q * (p /ₘ q) = q * r - q * (p /ₘ q)
rw₂ rw₃ : p - q * (p /ₘ q) = p - q * (p /ₘ q)
⊢ p %ₘ q = q * (r - p /ₘ q)

Tactic:
rw [modByMonic_eq_sub_mul_div, mul_sub, ← hr]

Premises used: mul_sub, Polynomial.modByMonic_eq_sub_mul_div
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ p %ₘ q = q * (r - p /ₘ q)

Tactic:
have hmod : p %ₘ q = q * (r - p /ₘ q) := by rw [modByMonic_eq_sub_mul_div, mul_sub, ← hr]
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
⊢ (q * (r - p /ₘ q)).degree < q.degree

Tactic:
have : degree (q * (r - p /ₘ q)) < degree q := hmod ▸ degree_modByMonic_lt _ hq
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h_1 : q ∣ p
h_2 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
rw : (q * (r - p /ₘ q)).leadingCoeff = 0
rw₁ : (q * 0).leadingCoeff = 0
rw₂ : Eq.{u + 1} (α := R) (leadingCoeff 0) 0
rw₃ rw₄ : Eq.{u + 1} (α := R) 0 0
⊢ (p %ₘ q).leadingCoeff = 0

Tactic:
rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero]

Premises used: Polynomial.leadingCoeff_zero, MulZeroClass.mul_zero, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
⊢ (r - p /ₘ q).leadingCoeff ≠ 0

Tactic:
have hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0 := fun h =>
      hpq0 <|
        leadingCoeff_eq_zero.1
          (by rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero])
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
rwa : 1 * (r - p /ₘ q).leadingCoeff ≠ 0
rwa₁ rwa₂ rwa₃ rwa₄ : (r - p /ₘ q).leadingCoeff ≠ 0
⊢ q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0

Tactic:
rwa [Monic.def.1 hq, one_mul]

Premises used: Iff.mp, Polynomial.Monic.def, one_mul
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
⊢ q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0

Tactic:
have hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0 := by rwa [Monic.def.1 hq, one_mul]
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
⊢ HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(r - p /ₘ q).natDegree : WithBot ℕ) <
    (↑q.natDegree : WithBot ℕ)

Tactic:
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero,
      degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)] at this

Premises used: Iff.mpr, Polynomial.degree_eq_natDegree, mt, Polynomial.degree_mul', Polynomial.leadingCoeff_eq_zero, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
this₁ :
  HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(r - p /ₘ q).natDegree : WithBot ℕ) <
    (↑q.natDegree : WithBot ℕ)
⊢ (r - p /ₘ q).leadingCoeff ≠ 0

Tactic:
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero,
      degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)] at this

Premises used: Iff.mpr, Polynomial.degree_eq_natDegree, mt, Polynomial.degree_mul', Polynomial.leadingCoeff_eq_zero, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
this₁ :
  HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(r - p /ₘ q).natDegree : WithBot ℕ) <
    (↑q.natDegree : WithBot ℕ)
hrpq0₁ : (r - p /ₘ q).leadingCoeff ≠ 0
⊢ q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0

Tactic:
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero,
      degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)] at this

Premises used: Iff.mpr, Polynomial.degree_eq_natDegree, mt, Polynomial.degree_mul', Polynomial.leadingCoeff_eq_zero, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this :
  HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(r - p /ₘ q).natDegree : WithBot ℕ) <
    (↑q.natDegree : WithBot ℕ)
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False

Tactic:
not_lt_of_ge (Nat.le_add_right _ _) (WithBot.coe_lt_coe.1 this)

Premises used: Nat.le_add_right, WithBot.coe_lt_coe, Iff.mp, not_lt_of_ge
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
h_1 : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this :
  HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(r - p /ₘ q).natDegree : WithBot ℕ) <
    (↑q.natDegree : WithBot ℕ)
hrpq0 : (r - p /ₘ q).leadingCoeff ≠ 0
hlc : q.leadingCoeff * (r - p /ₘ q).leadingCoeff ≠ 0
⊢ False

Tactic:
exact not_lt_of_ge (Nat.le_add_right _ _) (WithBot.coe_lt_coe.1 this)

Premises used: Nat.le_add_right, WithBot.coe_lt_coe, Iff.mp, not_lt_of_ge
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
rw : q ∣ q * p
⊢ q * p %ₘ 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 : Ring R
p q : R[X]
hq : q.Monic
⊢ q ∣ q * p

Tactic:
dvd_mul_right q p

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

Tactic:
exact dvd_mul_right q p

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R[X]
hx : x.Monic
rw : map f (y %ₘ x) = 0 ↔ y %ₘ x = 0
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
rw [← modByMonic_eq_zero_iff_dvd hx, ← modByMonic_eq_zero_iff_dvd (hx.map f), ←
    map_modByMonic f hx]

Premises used: Polynomial.map_modByMonic, Polynomial.modByMonic_eq_zero_iff_dvd, Polynomial.Monic.map
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R[X]
hx : x.Monic
H : map f (y %ₘ x) = 0
rw : 0 = map f 0
rw₁ rw₂ : Eq.{v + 1} (α := S[X]) 0 0
⊢ map f (y %ₘ x) = map f 0

Tactic:
rw [H, Polynomial.map_zero]

Premises used: Polynomial.map_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R[X]
hx : x.Monic
H : y %ₘ x = 0
rw : map f 0 = 0
rw₁ rw₂ : Eq.{v + 1} (α := S[X]) 0 0
⊢ map f (y %ₘ x) = 0

Tactic:
rw [H, Polynomial.map_zero]

Premises used: Polynomial.map_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R[X]
hx : x.Monic
⊢ map f (y %ₘ x) = 0 ↔ y %ₘ x = 0

Tactic:
exact
    ⟨fun H => map_injective f hf <| by rw [H, Polynomial.map_zero], fun H => by
      rw [H, Polynomial.map_zero]⟩
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ Monic.{u} (R := R) 1

Tactic:
monic_one (R := R)

Premises used: Polynomial.monic_one
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ Monic.{u} (R := R) 1

Tactic:
convert! monic_one (R := R)

Premises used: Polynomial.monic_one
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
rw : p %ₘ 1 + 1 * (p /ₘ 1)
| p

Tactic:
rw [← modByMonic_add_div p 1]

Premises used: Polynomial.modByMonic_add_div, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
simp : p /ₘ 1
| p %ₘ 1 + 1 * (p /ₘ 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
rw : p /ₘ 1
| p

Tactic:
rw [← modByMonic_add_div p 1]; simp

Premises used: Polynomial.modByMonic_add_div, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
conv_rhs : p /ₘ 1 = p
conv_rhs₁ : p /ₘ 1 = p /ₘ 1
⊢ p /ₘ 1 = p

Tactic:
conv_rhs => rw [← modByMonic_add_div p 1]; simp

Premises used: Polynomial.modByMonic_add_div, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ (↑n : WithBot ℕ)
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ (↑n : WithBot ℕ)
h : Nontrivial R
⊢ ∀ (i : ℕ), Eq.{u + 1} (α := R[X]) ((fun (i : ℕ) (c : R) ↦ ((monomial i : (a : R) → R[X]) c : R[X])) i 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ (↑n : WithBot ℕ)
h : Nontrivial R
⊢ ∑ i : Fin n, (monomial (↑i : ℕ) : (a : R) → R[X]) ((p %ₘ q).coeff (↑i : ℕ)) = p %ₘ q

Tactic:
exact
    (sum_fin (fun i c => monomial i c) (by simp) ((degree_modByMonic_lt _ hq).trans_le hn)).trans
      (sum_monomial_eq _)

Premises used: Polynomial.monomial, Polynomial.sum_monomial_eq, LT.lt.trans_le, Polynomial.degree_modByMonic_lt, Polynomial.sum_fin, DFunLike.coe, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmo : q.Monic
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmo : q.Monic
h : Nontrivial R
rw rw₁ : q * p = q * p
⊢ 0 + q * p = q * p

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmo : q.Monic
h : Nontrivial R
refine : degree.{u} (R := R) 0 < q.degree
⊢ q * p /ₘ q = p

Tactic:
refine (div_modByMonic_unique _ 0 hmo ⟨by rw [zero_add], ?_⟩).1

Premises used: Polynomial.div_modByMonic_unique, And.left, And.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmo : q.Monic
h : Nontrivial R
⊢ ⊥ < q.degree

Tactic:
Ne.bot_lt fun h => hmo.ne_zero (degree_eq_bot.1 h)

Premises used: Iff.mp, Polynomial.degree_eq_bot, Ne.bot_lt, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmo : q.Monic
h : Nontrivial R
⊢ ⊥ < q.degree

Tactic:
exact Ne.bot_lt fun h => hmo.ne_zero (degree_eq_bot.1 h)

Premises used: Iff.mp, Polynomial.degree_eq_bot, Ne.bot_lt, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : Nontrivial R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Monic

Tactic:
have := monic_X_sub_C a
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : Nontrivial R
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Monic
set :
  let q := p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]);
  q.coeff n = p.coeff (n + 1) + a * q.coeff (n + 1)
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
    p.coeff (n + 1) + a * (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1)

Tactic:
set q := p /ₘ (X - C a)

Premises used: Polynomial.C, HSub.hSub, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : Nontrivial R
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Monic
q : R[X] := p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])
rw :
  q.coeff n =
    (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]))).coeff
        (n + 1) +
      a * q.coeff (n + 1)
⊢ q.coeff n = p.coeff (n + 1) + a * q.coeff (n + 1)

Tactic:
rw [← p.modByMonic_add_div (X - C a)]

Premises used: Polynomial.C, HSub.hSub, Polynomial.modByMonic_add_div, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : Nontrivial R
this : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Monic
q : R[X] := 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])).degree < (↑(n + 1) : WithBot ℕ)

Tactic:
have : degree (p %ₘ (X - C a)) < ↑(n + 1) := degree_X_sub_C a ▸ p.degree_modByMonic_lt this
    |>.trans_le <| WithBot.coe_le_coe.mpr le_add_self
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : Nontrivial R
this_1 : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Monic
q : R[X] := p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])
this : (p %ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree < (↑(n + 1) : WithBot ℕ)
⊢ q.coeff n =
    (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]))).coeff
        (n + 1) +
      a * q.coeff (n + 1)

Tactic:
simp [q, sub_mul, add_sub, coeff_eq_zero_of_degree_lt this]

Premises used: add_sub, sub_mul, Polynomial.coeff_eq_zero_of_degree_lt