awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h1 : p ∣ q
h2 : q ≠ 0
obtain : ∀ (q : R[X]) (h2 : p * q ≠ 0), p.natDegree ≤ (p * q).natDegree
⊢ p.natDegree ≤ q.natDegree

Tactic:
obtain ⟨q, rfl⟩ := h1

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p ≠ 0 ∧ q ≠ 0

Tactic:
rw [mul_ne_zero_iff] at h2

Premises used: mul_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
rw : p.natDegree ≤ p.natDegree + q.natDegree
⊢ p.natDegree ≤ (p * q).natDegree

Tactic:
rw [natDegree_mul h2.1 h2.2]

Premises used: Polynomial.natDegree_mul, And.right, And.left
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ p.natDegree + q.natDegree

Tactic:
Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ p.natDegree + q.natDegree

Tactic:
exact Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h1 : p ∣ q
h2 : q ≠ 0
rcases : ∀ (q : R[X]) (h2 : p * q ≠ 0), p.degree ≤ (p * q).degree
⊢ p.degree ≤ q.degree

Tactic:
rcases h1 with ⟨q, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.degree ≤ (p * q).degree

Tactic:
degree_le_mul_left p h2.2

Premises used: Polynomial.degree_le_mul_left, And.right
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.degree ≤ (p * q).degree

Tactic:
exact degree_le_mul_left p h2.2

Premises used: Polynomial.degree_le_mul_left, And.right
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.degree < p.degree
by_contra : ∀ (hc : ¬q = 0), False
⊢ q = 0

Tactic:
by_contra hc
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.degree < p.degree
hc : ¬q = 0
⊢ False

Tactic:
lt_iff_not_ge.mp h₂ (degree_le_of_dvd h₁ hc)

Premises used: lt_iff_not_ge, Polynomial.degree_le_of_dvd, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.degree < p.degree
hc : ¬q = 0
⊢ False

Tactic:
exact lt_iff_not_ge.mp h₂ (degree_le_of_dvd h₁ hc)

Premises used: lt_iff_not_ge, Polynomial.degree_le_of_dvd, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
by_contra : ∀ (hc : ¬q = 0), False
⊢ q = 0

Tactic:
by_contra hc
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
hc : ¬q = 0
⊢ False

Tactic:
lt_iff_not_ge.mp h₂ (natDegree_le_of_dvd h₁ hc)

Premises used: lt_iff_not_ge, Polynomial.natDegree_le_of_dvd, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
hc : ¬q = 0
⊢ False

Tactic:
exact lt_iff_not_ge.mp h₂ (natDegree_le_of_dvd h₁ hc)

Premises used: lt_iff_not_ge, Polynomial.natDegree_le_of_dvd, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.degree < p.degree
by_contra : ∀ (hcontra : p ∣ q), False
⊢ ¬p ∣ q

Tactic:
by_contra hcontra
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.degree < p.degree
hcontra : p ∣ q
⊢ False

Tactic:
h0 (eq_zero_of_dvd_of_degree_lt hcontra hl)

Premises used: Polynomial.eq_zero_of_dvd_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.degree < p.degree
hcontra : p ∣ q
⊢ False

Tactic:
exact h0 (eq_zero_of_dvd_of_degree_lt hcontra hl)

Premises used: Polynomial.eq_zero_of_dvd_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
by_contra : ∀ (hcontra : p ∣ q), False
⊢ ¬p ∣ q

Tactic:
by_contra hcontra
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
hcontra : p ∣ q
⊢ False

Tactic:
h0 (eq_zero_of_dvd_of_natDegree_lt hcontra hl)

Premises used: Polynomial.eq_zero_of_dvd_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
hcontra : p ∣ q
⊢ False

Tactic:
exact h0 (eq_zero_of_dvd_of_natDegree_lt hcontra hl)

Premises used: Polynomial.eq_zero_of_dvd_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
rw :
  HAdd.hAdd (α := ℤ) (↑p₁.natDegree : ℤ) (↑q₂.natDegree : ℤ) =
    HAdd.hAdd (α := ℤ) (↑p₂.natDegree : ℤ) (↑q₁.natDegree : ℤ)
⊢ HSub.hSub (α := ℤ) (↑p₁.natDegree : ℤ) (↑q₁.natDegree : ℤ) =
    HSub.hSub (α := ℤ) (↑p₂.natDegree : ℤ) (↑q₂.natDegree : ℤ)

Tactic:
rw [sub_eq_sub_iff_add_eq_add]

Premises used: sub_eq_sub_iff_add_eq_add
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
norm_cast : p₁.natDegree + q₂.natDegree = p₂.natDegree + q₁.natDegree
⊢ HAdd.hAdd (α := ℤ) (↑p₁.natDegree : ℤ) (↑q₂.natDegree : ℤ) =
    HAdd.hAdd (α := ℤ) (↑p₂.natDegree : ℤ) (↑q₁.natDegree : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Polynomial.Degree.Domain
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
rw : (p₁ * q₂).natDegree = p₂.natDegree + q₁.natDegree
rw₁ : (p₁ * q₂).natDegree = (p₂ * q₁).natDegree
rw₂ rw₃ : (p₂ * q₁).natDegree = (p₂ * q₁).natDegree
⊢ p₁.natDegree + q₂.natDegree = p₂.natDegree + q₁.natDegree

Tactic:
rw [← natDegree_mul hp₁ hq₂, ← natDegree_mul hp₂ hq₁, h_eq]

Premises used: Polynomial.natDegree_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
simp : p.natDegree = 0 ∧ p.Monic ↔ p = 1
⊢ p.IsMonicOfDegree 0 ↔ p = 1

Tactic:
simp only [isMonicOfDegree_iff']

Premises used: Polynomial.isMonicOfDegree_iff'
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.natDegree = 0 ∧ p.Monic ↔ p = 1

Tactic:
⟨fun ⟨H₁, H₂⟩ ↦ eq_one_of_monic_natDegree_zero H₂ H₁, fun H ↦ ?_⟩

Premises used: _private.0.Polynomial.isMonicOfDegree_zero_iff.match_1, Iff.intro, Polynomial.eq_one_of_monic_natDegree_zero, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
refine : ∀ (H : p = 1), p.natDegree = 0 ∧ p.Monic
⊢ p.natDegree = 0 ∧ p.Monic ↔ p = 1

Tactic:
refine ⟨fun ⟨H₁, H₂⟩ ↦ eq_one_of_monic_natDegree_zero H₂ H₁, fun H ↦ ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
H : p = 1
subst : natDegree.{u_1} (R := R) 1 = 0 ∧ Monic.{u_1} (R := R) 1
⊢ p.natDegree = 0 ∧ p.Monic

Tactic:
subst H
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
⊢ natDegree.{u_1} (R := R) 1 = 0 ∧ Monic.{u_1} (R := R) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
⊢ p.leadingCoeff = 1

Tactic:
Monic.def.mp hp.monic

Premises used: Polynomial.IsMonicOfDegree.monic, Iff.mp, Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
rw : IsMonicOfDegree.{u_1} (R := R) 1 n ↔ n = 0
⊢ p.IsMonicOfDegree n ↔ n = 0

Tactic:
rw [Subsingleton.eq_one p]

Premises used: Subsingleton.eq_one
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
⊢ IsMonicOfDegree.{u_1} (R := R) 1 n ↔ n = 0

Tactic:
⟨fun ⟨H, _⟩ ↦ ?_, fun H ↦ ?_⟩

Premises used: _private.0.Polynomial.isMonicOfDegree_iff_of_subsingleton.match_1, Iff.intro, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
refine_1 : IsMonicOfDegree.{u_1} (R := R) 1 n → ∀ (H : natDegree.{u_1} (R := R) 1 = n), Monic.{u_1} (R := R) 1 → n = 0
refine_2 : ∀ (H : n = 0), IsMonicOfDegree.{u_1} (R := R) 1 n
⊢ IsMonicOfDegree.{u_1} (R := R) 1 n ↔ n = 0

Tactic:
refine ⟨fun ⟨H, _⟩ ↦ ?_, fun H ↦ ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
h : IsMonicOfDegree.{u_1} (R := R) 1 n
H : natDegree.{u_1} (R := R) 1 = n
monic : Monic.{u_1} (R := R) 1
refine_1 : ∀ (H : 0 = n), Monic.{u_1} (R := R) 1 → n = 0
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (H : n = 0), Monic.{u_1} (R := R) 1 → n = 0
⊢ n = 0

Tactic:
rwa [natDegree_one, eq_comm] at H

Premises used: eq_comm, Polynomial.natDegree_one
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Subsingleton R
p : R[X]
n : ℕ
H : n = 0
refine_2 : IsMonicOfDegree.{u_1} (R := R) 1 0
refine_2₁ refine_2₂ : Eq.{u_1 + 1} (α := R[X]) 1 1
⊢ IsMonicOfDegree.{u_1} (R := R) 1 n

Tactic:
rw [H, isMonicOfDegree_zero_iff]

Premises used: Polynomial.isMonicOfDegree_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
simp : p.natDegree = n ∧ p.Monic ↔ p.natDegree ≤ n ∧ p.coeff n = 1
⊢ p.IsMonicOfDegree n ↔ p.natDegree ≤ n ∧ p.coeff n = 1

Tactic:
simp only [isMonicOfDegree_iff']

Premises used: Polynomial.isMonicOfDegree_iff'
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
⊢ p.natDegree = n ∧ p.Monic ↔ p.natDegree ≤ n ∧ p.coeff n = 1

Tactic:
⟨fun ⟨H₁, H₂⟩ ↦ ⟨H₁.le, H₁ ▸ Monic.coeff_natDegree H₂⟩, fun ⟨H₁, H₂⟩ ↦ ⟨?_, ?_⟩⟩

Premises used: Eq.rec, Eq.le, LE.le, Polynomial.coeff, _private.0.Polynomial.isMonicOfDegree_iff.match_1, Polynomial.Monic, And, And.intro, Iff.intro, Polynomial.Monic.coeff_natDegree, _private.0.Polynomial.isMonicOfDegree_iff.match_2, Polynomial.natDegree, OfNat.ofNat, Eq
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
refine_1 : p.natDegree ≤ n ∧ p.coeff n = 1 → ∀ (H₁ : p.natDegree ≤ n) (H₂ : p.coeff n = 1), p.natDegree = n
refine_2 : p.natDegree ≤ n ∧ p.coeff n = 1 → ∀ (H₁ : p.natDegree ≤ n) (H₂ : p.coeff n = 1), p.Monic
⊢ p.natDegree = n ∧ p.Monic ↔ p.natDegree ≤ n ∧ p.coeff n = 1

Tactic:
refine ⟨fun ⟨H₁, H₂⟩ ↦ ⟨H₁.le, H₁ ▸ Monic.coeff_natDegree H₂⟩, fun ⟨H₁, H₂⟩ ↦ ⟨?_, ?_⟩⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
h : p.natDegree ≤ n ∧ p.coeff n = 1
H₁ : p.natDegree ≤ n
H₂ : p.coeff n = 1
⊢ p.natDegree = n

Tactic:
natDegree_eq_of_le_of_coeff_ne_zero H₁ <| H₂ ▸ one_ne_zero

Premises used: Eq.rec, Polynomial.natDegree_eq_of_le_of_coeff_ne_zero, one_ne_zero, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
h : p.natDegree ≤ n ∧ p.coeff n = 1
H₁ : p.natDegree ≤ n
H₂ : p.coeff n = 1
⊢ p.natDegree = n

Tactic:
exact natDegree_eq_of_le_of_coeff_ne_zero H₁ <| H₂ ▸ one_ne_zero

Premises used: Polynomial.natDegree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
h : p.natDegree ≤ n ∧ p.coeff n = 1
H₁ : p.natDegree ≤ n
H₂ : p.coeff n = 1
⊢ p.Monic

Tactic:
monic_of_natDegree_le_of_coeff_eq_one n H₁ H₂

Premises used: Polynomial.monic_of_natDegree_le_of_coeff_eq_one
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
h : p.natDegree ≤ n ∧ p.coeff n = 1
H₁ : p.natDegree ≤ n
H₂ : p.coeff n = 1
⊢ p.Monic

Tactic:
exact monic_of_natDegree_le_of_coeff_eq_one n H₁ H₂

Premises used: Polynomial.monic_of_natDegree_le_of_coeff_eq_one
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ ∃ (q : R[X]), p = HPow.hPow (α := R[X]) X n + q ∧ q.natDegree < n

Tactic:
⟨p.eraseLead, ?_, ?_⟩

Premises used: Polynomial.eraseLead, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
refine_1 : p = HPow.hPow (α := R[X]) X n + p.eraseLead
refine_2 : p.eraseLead.natDegree < n
⊢ ∃ (q : R[X]), p = HPow.hPow (α := R[X]) X n + q ∧ q.natDegree < n

Tactic:
refine ⟨p.eraseLead, ?_, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
refine_1 :
  p.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
    HPow.hPow (α := R[X]) X n + p.eraseLead
⊢ p = HPow.hPow (α := R[X]) X n + p.eraseLead

Tactic:
nth_rewrite 1 [← p.eraseLead_add_C_mul_X_pow]

Premises used: Polynomial.eraseLead_add_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
refine_1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      p.eraseLead =
    HPow.hPow (α := R[X]) X n + p.eraseLead
refine_1₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X n) + p.eraseLead =
    HPow.hPow (α := R[X]) X n + p.eraseLead
refine_1₂ : (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n + p.eraseLead = HPow.hPow (α := R[X]) X n + p.eraseLead
refine_1₃ : 1 * HPow.hPow (α := R[X]) X n + p.eraseLead = HPow.hPow (α := R[X]) X n + p.eraseLead
refine_1₄ refine_1₅ : HPow.hPow (α := R[X]) X n + p.eraseLead = HPow.hPow (α := R[X]) X n + p.eraseLead
⊢ p.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) =
    HPow.hPow (α := R[X]) X n + p.eraseLead

Tactic:
rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq, add_comm, map_one, one_mul, Polynomial.IsMonicOfDegree.leadingCoeff_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p.eraseLead.natDegree < n

Tactic:
p.eraseLead_natDegree_le.trans_lt ?_

Premises used: Polynomial.eraseLead_natDegree_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
refine_2 : p.natDegree - 1 < n
⊢ p.eraseLead.natDegree < n

Tactic:
refine p.eraseLead_natDegree_le.trans_lt ?_

Premises used: Polynomial.eraseLead_natDegree_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
refine_2 : n - 1 < n
⊢ p.natDegree - 1 < n

Tactic:
rw [hp.natDegree_eq]

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ n - 1 < n

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
inl : ∀ (H : Subsingleton R), (p * q).IsMonicOfDegree (m + n)
inr : ∀ (H : Nontrivial R), (p * q).IsMonicOfDegree (m + n)
⊢ (p * q).IsMonicOfDegree (m + n)

Tactic:
rcases subsingleton_or_nontrivial R with H | H

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Subsingleton R
inl : ∀ (hp : m = 0) (hq : n = 0), m = 0 ∧ n = 0
⊢ (p * q).IsMonicOfDegree (m + n)

Tactic:
simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hp hq ⊢

Premises used: Nat.add_eq_zero_iff, Polynomial.isMonicOfDegree_iff_of_subsingleton
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
H : Subsingleton R
hp : m = 0
hq : n = 0
⊢ m = 0 ∧ n = 0

Tactic:
⟨hp, hq⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
H : Subsingleton R
hp : m = 0
hq : n = 0
⊢ m = 0 ∧ n = 0

Tactic:
exact ⟨hp, hq⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ (p * q).IsMonicOfDegree (m + n)

Tactic:
⟨?_, hp.monic.mul hq.monic⟩

Premises used: Polynomial.IsMonicOfDegree.mk, Polynomial.IsMonicOfDegree.monic, Polynomial.Monic.mul
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
inr : (p * q).natDegree = m + n
⊢ (p * q).IsMonicOfDegree (m + n)

Tactic:
refine ⟨?_, hp.monic.mul hq.monic⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
rw : Ne.{u_1 + 1} (α := R) 1 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rw [hp.leadingCoeff_eq, hq.leadingCoeff_eq, one_mul]

Premises used: one_mul, Polynomial.IsMonicOfDegree.leadingCoeff_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ Ne.{u_1 + 1} (α := R) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ Ne.{u_1 + 1} (α := R) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [hp.leadingCoeff_eq, hq.leadingCoeff_eq, one_mul]
    exact one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Nontrivial R
this : p.leadingCoeff * q.leadingCoeff ≠ 0
inr : p.natDegree + q.natDegree = m + n
inr₁ : m + q.natDegree = m + n
inr₂ inr₃ : m + n = m + n
⊢ (p * q).natDegree = m + n

Tactic:
rw [natDegree_mul' this, hp.natDegree_eq, hq.natDegree_eq]

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq, Polynomial.natDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
⊢ (HPow.hPow (β := ℕ) p 0).IsMonicOfDegree (m * 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ n * p).IsMonicOfDegree (m * n + m)

Tactic:
ih.mul hp

Premises used: Polynomial.IsMonicOfDegree.mul
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
ih : (p ^ n).IsMonicOfDegree (m * n)
⊢ (p ^ n * p).IsMonicOfDegree (m * n + m)

Tactic:
exact ih.mul hp

Premises used: Polynomial.IsMonicOfDegree.mul
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
m : ℕ
hp : p.IsMonicOfDegree m
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).IsMonicOfDegree (m * 0)
succ : ∀ (n : ℕ) (ih : (p ^ n).IsMonicOfDegree (m * n)), (p ^ (n + 1)).IsMonicOfDegree (m * (n + 1))
⊢ (p ^ n).IsMonicOfDegree (m * n)

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, mul_add, mul_one]
    exact ih.mul hp

Premises used: pow_succ, mul_add, mul_one
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
m : ℕ
hm : n ≤ m
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.IsMonicOfDegree n
m : ℕ
hm : n ≤ m
h : Nontrivial R
rw :
  ∀ (hp : p.natDegree ≤ n ∧ p.coeff n = 1) (hq : q.natDegree ≤ n ∧ q.coeff n = 1) {m : ℕ} (hm : n ≤ m),
    Nontrivial R → p.coeff m = q.coeff m
⊢ p.coeff m = q.coeff m

Tactic:
rw [isMonicOfDegree_iff] at hp hq

Premises used: Polynomial.isMonicOfDegree_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm : n ≤ m
h : Nontrivial R
inl : ∀ (hm : n ≤ n), p.coeff n = q.coeff n
inr : ∀ (hm : n < m), p.coeff m = q.coeff m
⊢ p.coeff m = q.coeff m

Tactic:
rcases eq_or_lt_of_le hm with rfl | hm

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
h : Nontrivial R
hm : n ≤ n
inl : 1 = q.coeff n
inl₁ inl₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ p.coeff n = q.coeff n

Tactic:
rw [hp.2, hq.2]

Premises used: And.right
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm_1 : n ≤ m
h : Nontrivial R
hm : n < m
⊢ p.natDegree < m

Tactic:
replace hp : p.natDegree < m := hp.1.trans_lt hm
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hq : q.natDegree ≤ n ∧ q.coeff n = 1
m : ℕ
hm_1 : n ≤ m
h : Nontrivial R
hm : n < m
hp : p.natDegree < m
⊢ q.natDegree < m

Tactic:
replace hq : q.natDegree < m := hq.1.trans_lt hm
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n m : ℕ
hm_1 : n ≤ m
h : Nontrivial R
hm : n < m
hp : p.natDegree < m
hq : q.natDegree < m
inr : 0 = q.coeff m
inr₁ inr₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ p.coeff m = q.coeff m

Tactic:
rw [coeff_eq_zero_of_natDegree_lt hp, coeff_eq_zero_of_natDegree_lt hq]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt