awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
inl : ∀ (H : Subsingleton R), q.IsMonicOfDegree n
inr : ∀ (H : Nontrivial R), q.IsMonicOfDegree n
⊢ q.IsMonicOfDegree 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
hpq : (p * q).IsMonicOfDegree (m + n)
H : Subsingleton R
inl : ∀ (hpq : m = 0 ∧ n = 0), n = 0
⊢ q.IsMonicOfDegree n

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

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 : ℕ
hp : p.IsMonicOfDegree m
H : Subsingleton R
hpq : m = 0 ∧ n = 0
⊢ n = 0

Tactic:
hpq.2

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

Tactic:
exact hpq.2

Premises used: And.right
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
⊢ q.Monic

Tactic:
have h₂ : q.Monic := hp.monic.of_mul_monic_left hpq.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
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
⊢ q.IsMonicOfDegree n

Tactic:
⟨?_, h₂⟩

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

Tactic:
refine ⟨?_, h₂⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
⊢ (p * q).natDegree = m + n

Tactic:
have := hpq.natDegree_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
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
rw : Ne.{u_1 + 1} (α := R) 1 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rw [hp.leadingCoeff_eq, h₂.leadingCoeff, one_mul]

Premises used: Polynomial.Monic.leadingCoeff, 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
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
⊢ 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
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
⊢ 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
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
have h : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [hp.leadingCoeff_eq, h₂.leadingCoeff, 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
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ m + q.natDegree = m + n

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

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq, Polynomial.natDegree_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
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
this₁ : m + q.natDegree = m + n
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

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

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq, Polynomial.natDegree_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
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : m + q.natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ q.natDegree = n

Tactic:
(Nat.add_left_cancel this.symm).symm

Premises used: Nat.add_left_cancel, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : m + q.natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ q.natDegree = n

Tactic:
exact (Nat.add_left_cancel this.symm).symm

Premises used: Nat.add_left_cancel, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
inl : ∀ (H : Subsingleton R), p.IsMonicOfDegree m
inr : ∀ (H : Nontrivial R), p.IsMonicOfDegree m
⊢ p.IsMonicOfDegree m

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 : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Subsingleton R
inl : ∀ (hpq : m = 0 ∧ n = 0), m = 0
⊢ p.IsMonicOfDegree m

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

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 : ℕ
hq : q.IsMonicOfDegree n
H : Subsingleton R
hpq : m = 0 ∧ n = 0
⊢ m = 0

Tactic:
hpq.1

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

Tactic:
exact hpq.1

Premises used: And.left
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
⊢ p.Monic

Tactic:
have h₂ : p.Monic := hq.monic.of_mul_monic_right hpq.monic
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
⊢ p.IsMonicOfDegree m

Tactic:
⟨?_, h₂⟩

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

Tactic:
refine ⟨?_, h₂⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
⊢ (p * q).natDegree = m + n

Tactic:
have := hpq.natDegree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
rw : Ne.{u_1 + 1} (α := R) 1 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rw [h₂.leadingCoeff, hq.leadingCoeff_eq, one_mul]

Premises used: Polynomial.Monic.leadingCoeff, 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 : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
⊢ 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 : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
⊢ 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 : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
have h : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [h₂.leadingCoeff, 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 : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p.natDegree + n = m + n

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

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq, Polynomial.natDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : (p * q).natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
this₁ : p.natDegree + n = m + n
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

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

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq, Polynomial.natDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : p.natDegree + n = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p.natDegree = m

Tactic:
(Nat.add_right_cancel this.symm).symm

Premises used: Nat.add_right_cancel, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
this : p.natDegree + n = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p.natDegree = m

Tactic:
exact (Nat.add_right_cancel this.symm).symm

Premises used: Nat.add_right_cancel, Eq.symm
-- 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.natDegree < n
inl : ∀ (H : Subsingleton R), (p + q).IsMonicOfDegree n
inr : ∀ (H : Nontrivial R), (p + q).IsMonicOfDegree n
⊢ (p + q).IsMonicOfDegree 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]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
H : Subsingleton R
⊢ (p + q).IsMonicOfDegree n

Tactic:
simpa using hp
-- 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.natDegree < n
H : Nontrivial R
⊢ (p + q).IsMonicOfDegree n

Tactic:
(isMonicOfDegree_iff ..).mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, Polynomial.isMonicOfDegree_iff, And.intro
-- 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.natDegree < n
H : Nontrivial R
inr : (p + q).natDegree ≤ n
inr₁ : (p + q).coeff n = 1
⊢ (p + q).IsMonicOfDegree n

Tactic:
refine (isMonicOfDegree_iff ..).mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, Polynomial.isMonicOfDegree_iff, And.intro
-- 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.natDegree < n
H : Nontrivial R
⊢ (p + q).natDegree ≤ n

Tactic:
natDegree_add_le_of_degree_le hp.natDegree_eq.le hq.le

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq, LT.lt.le, Polynomial.natDegree_add_le_of_degree_le, Eq.le
-- 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.natDegree < n
H : Nontrivial R
⊢ (p + q).natDegree ≤ n

Tactic:
exact natDegree_add_le_of_degree_le hp.natDegree_eq.le hq.le

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq, LT.lt.le, Polynomial.natDegree_add_le_of_degree_le, Eq.le
-- 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.natDegree < n
H : Nontrivial R
inr : p.coeff n = 1
⊢ (p + q).coeff n = 1

Tactic:
rw [coeff_add_eq_left_of_lt hq]

Premises used: Polynomial.coeff_add_eq_left_of_lt
-- 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.natDegree < n
H : Nontrivial R
⊢ p.coeff n = 1

Tactic:
((isMonicOfDegree_iff p n).mp hp).2

Premises used: Polynomial.isMonicOfDegree_iff, And.right, Iff.mp
-- 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.natDegree < n
H : Nontrivial R
⊢ p.coeff n = 1

Tactic:
exact ((isMonicOfDegree_iff p n).mp hp).2

Premises used: Polynomial.isMonicOfDegree_iff, And.right, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree < n
hq : q.IsMonicOfDegree n
rw : (q + p).IsMonicOfDegree n
⊢ (p + q).IsMonicOfDegree n

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree < n
hq : q.IsMonicOfDegree n
⊢ (q + p).IsMonicOfDegree n

Tactic:
hq.add_right hp

Premises used: Polynomial.IsMonicOfDegree.add_right
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree < n
hq : q.IsMonicOfDegree n
⊢ (q + p).IsMonicOfDegree n

Tactic:
exact hq.add_right hp

Premises used: Polynomial.IsMonicOfDegree.add_right
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
inl : ∀ (h : Subsingleton R), (p.comp q).IsMonicOfDegree (m * n)
inr : ∀ (h : Nontrivial R), (p.comp q).IsMonicOfDegree (m * n)
⊢ (p.comp 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 : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Subsingleton R
inl : ∀ (hp : m = 0), m = 0 ∨ n = 0
⊢ (p.comp q).IsMonicOfDegree (m * n)

Tactic:
simp only [isMonicOfDegree_iff_of_subsingleton, mul_eq_zero] at hp ⊢

Premises used: mul_eq_zero, 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 : ℕ
hn : n ≠ 0
hq : q.IsMonicOfDegree n
h : Subsingleton R
hp : m = 0
⊢ m = 0 ∨ n = 0

Tactic:
.inl hp

Premises used: Or.inl
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hq : q.IsMonicOfDegree n
h : Subsingleton R
hp : m = 0
⊢ m = 0 ∨ n = 0

Tactic:
exact .inl hp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
inr : (p.comp q).IsMonicOfDegree (p.natDegree * q.natDegree)
⊢ (p.comp q).IsMonicOfDegree (m * n)

Tactic:
rw [← hp.natDegree_eq, ← hq.natDegree_eq]

Premises used: Polynomial.IsMonicOfDegree.natDegree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ (p.comp q).IsMonicOfDegree (p.natDegree * q.natDegree)

Tactic:
(isMonicOfDegree_iff ..).mpr ⟨natDegree_comp_le, ?_⟩

Premises used: Iff.mpr, Polynomial.isMonicOfDegree_iff, And.intro, Polynomial.natDegree_comp_le
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
inr : (p.comp q).coeff (p.natDegree * q.natDegree) = 1
⊢ (p.comp q).IsMonicOfDegree (p.natDegree * q.natDegree)

Tactic:
refine (isMonicOfDegree_iff ..).mpr ⟨natDegree_comp_le, ?_⟩

Premises used: Iff.mpr, Polynomial.isMonicOfDegree_iff, And.intro, Polynomial.natDegree_comp_le
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
inr : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
inr₁ : 1 * q.leadingCoeff ^ p.natDegree = 1
inr₂ : 1 * HPow.hPow (α := R) 1 p.natDegree = 1
inr₃ : HMul.hMul (α := R) 1 1 = 1
inr₄ inr₅ : Eq.{u_1 + 1} (α := R) 1 1
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = 1

Tactic:
rw [coeff_comp_degree_mul_degree (hq.natDegree_eq ▸ hn), hp.leadingCoeff_eq, hq.leadingCoeff_eq,
    one_pow, one_mul]

Premises used: one_pow, Polynomial.coeff_comp_degree_mul_degree, one_mul, Polynomial.IsMonicOfDegree.leadingCoeff_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
h : p.IsMonicOfDegree n
⊢ p ≠ 0

Tactic:
h.monic.ne_zero

Premises used: Polynomial.IsMonicOfDegree.monic, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
⊢ IsMonicOfDegree.{u_1} (R := R) X 1

Tactic:
(isMonicOfDegree_iff ..).mpr ⟨natDegree_X_le, coeff_X_one⟩

Premises used: Iff.mpr, Polynomial.isMonicOfDegree_iff, Polynomial.coeff_X_one, And.intro, Polynomial.natDegree_X_le
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).IsMonicOfDegree n

Tactic:
(isMonicOfDegree_iff ..).mpr ⟨natDegree_X_pow_le n, coeff_X_pow_self n⟩

Premises used: Iff.mpr, Polynomial.isMonicOfDegree_iff, Polynomial.natDegree_X_pow_le, Polynomial.coeff_X_pow_self, And.intro
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
⊢ IsMonicOfDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) 1) n

Tactic:
simpa only [monomial_one_right_eq_X_pow] using isMonicOfDegree_X_pow R n

Premises used: Polynomial.monomial_one_right_eq_X_pow, Polynomial.isMonicOfDegree_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
r : R
rw : LT.lt (α := ℕ) 0 1
⊢ natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) r) < 1

Tactic:
rw [natDegree_C]

Premises used: Polynomial.natDegree_C
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
r : R
⊢ LT.lt (α := ℕ) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
r : R
⊢ LT.lt (α := ℕ) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
⊢ f.IsMonicOfDegree 1 ↔ ∃ (r : R), f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])

Tactic:
⟨fun H ↦ ?_, fun ⟨r, H⟩ ↦ H ▸ isMonicOfDegree_X_add_one r⟩

Premises used: Polynomial.isMonicOfDegree_X_add_one, _private.0.Polynomial.isMonicOfDegree_one_iff.match_1, Eq.rec, Iff.intro, Polynomial.IsMonicOfDegree, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
refine : ∀ (H : f.IsMonicOfDegree 1), ∃ (r : R), f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])
⊢ f.IsMonicOfDegree 1 ↔ ∃ (r : R), f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])

Tactic:
refine ⟨fun H ↦ ?_, fun ⟨r, H⟩ ↦ H ▸ isMonicOfDegree_X_add_one r⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
⊢ ∃ (r : R), f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])

Tactic:
⟨f.coeff 0, ?_⟩

Premises used: Polynomial.coeff, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
refine : f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
⊢ ∃ (r : R), f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])

Tactic:
refine ⟨f.coeff 0, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
a : ∀ (n : ℕ), f.coeff n = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff n
⊢ f = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])

Tactic:
ext1 n
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
n : ℕ
a : f.coeff 0 = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff 0
a₁ : ∀ (hn : n > 0), f.coeff n = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff n
⊢ f.coeff n = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
⊢ f.coeff 0 = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
n : ℕ
hn : n > 0
⊢ 1 ≤ n

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
n : ℕ
hn : n > 0
⊢ f.coeff n = (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f.coeff 0) : R[X])).coeff n

Tactic:
exact H.coeff_eq (isMonicOfDegree_X_add_one _) (by lia)

Premises used: Polynomial.isMonicOfDegree_X_add_one, Polynomial.IsMonicOfDegree.coeff_eq