awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
h : Nontrivial R
⊢ p.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) b) ≠ 0

Tactic:
simp [leadingCoeff_C b, hp]

Premises used: Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
H : p.degree < (↑n : WithBot ℕ)
rw : (HPow.hPow (α := R[X]) X n).coeff n + p.coeff n = 1
rw₁ : (if n = n then 1 else 0) + p.coeff n = 1
rw₂ : 1 + p.coeff n = 1
rw₃ : HAdd.hAdd (α := R) 1 0 = 1
rw₄ rw₅ : Eq.{u + 1} (α := R) 1 1
⊢ (HPow.hPow (α := R[X]) X n + p).coeff n = 1

Tactic:
rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero]

Premises used: Polynomial.coeff_X_pow, Polynomial.coeff_add, if_pos, add_zero, rfl, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
h : n ≠ 0
⊢ LT.lt (α := WithBot ℕ) 0 (↑n : WithBot ℕ)

Tactic:
simp only [Nat.cast_pos, Nat.pos_iff_ne_zero, ne_eq, h, not_false_eq_true]

Premises used: Nat.cast_pos, Nat.pos_iff_ne_zero, ne_eq, not_false_eq_true
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
x : R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).Monic

Tactic:
pow_one (X : R[X]) ▸ monic_X_pow_add_C x one_ne_zero

Premises used: Polynomial.monic_X_pow_add_C, Eq.rec, pow_one, one_ne_zero, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h0 : ¬Eq.{u + 1} (α := R) 0 1
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]

Premises used: Ne.symm, Iff.mp, Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h0 : ¬Eq.{u + 1} (α := R) 0 1
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
      simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this_1 : DecidableEq R := Classical.decEq R
h0 : ¬Eq.{u + 1} (α := R) 0 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
rw : (p * q).leadingCoeff = 1
rw₁ : p.leadingCoeff * q.leadingCoeff = 1
rw₂ : 1 * q.leadingCoeff = 1
rw₃ : HMul.hMul (α := R) 1 1 = 1
rw₄ rw₅ : Eq.{u + 1} (α := R) 1 1
⊢ (p * q).Monic

Tactic:
rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]

Premises used: Polynomial.leadingCoeff_mul', Iff.mp, Polynomial.Monic.def, one_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n * p).Monic

Tactic:
(Monic.pow hp n).mul hp

Premises used: Polynomial.Monic.mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
⊢ (p ^ n * p).Monic

Tactic:
exact (Monic.pow hp n).mul hp

Premises used: Polynomial.Monic.mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
rwa : (p + q).leadingCoeff = 1
rwa₁ : (q + p).leadingCoeff = 1
rwa₂ rwa₃ rwa₄ rwa₅ : p.leadingCoeff = 1
⊢ (p + q).Monic

Tactic:
rwa [Monic, add_comm, leadingCoeff_add_of_degree_lt hpq]

Premises used: add_comm, Polynomial.Monic, Polynomial.leadingCoeff_add_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
hpq : p.degree < q.degree
rwa : (p + q).leadingCoeff = 1
rwa₁ rwa₂ rwa₃ rwa₄ : q.leadingCoeff = 1
⊢ (p + q).Monic

Tactic:
rwa [Monic, leadingCoeff_add_of_degree_lt hpq]

Premises used: Polynomial.Monic, Polynomial.leadingCoeff_add_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hpq : (p * q).Monic
contrapose : ∀ (hpq : ¬q.Monic), ¬(p * q).Monic
⊢ q.Monic

Tactic:
contrapose hpq
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.Monic
⊢ ¬q.leadingCoeff = 1

Tactic:
rw [Monic.def] at hpq ⊢

Premises used: Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hpq rwa rwa₁ rwa₂ rwa₃ : ¬q.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1

Tactic:
rwa [leadingCoeff_monic_mul hp]

Premises used: Polynomial.leadingCoeff_monic_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
hpq : (p * q).Monic
contrapose : ∀ (hpq : ¬p.Monic), ¬(p * q).Monic
⊢ p.Monic

Tactic:
contrapose hpq
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.Monic
⊢ ¬p.leadingCoeff = 1

Tactic:
rw [Monic.def] at hpq ⊢

Premises used: Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
hpq rwa rwa₁ rwa₂ rwa₃ : ¬p.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1

Tactic:
rwa [leadingCoeff_mul_monic hq]

Premises used: Polynomial.leadingCoeff_mul_monic
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0

Tactic:
simp [hp.leadingCoeff, hq.leadingCoeff]

Premises used: Polynomial.Monic.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
have : (p.comp q).natDegree = p.natDegree * q.natDegree :=
    natDegree_comp_eq_of_mul_ne_zero <| by simp [hp.leadingCoeff, hq.leadingCoeff]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
rw : (p.comp q).leadingCoeff = 1
rw₁ : (p.comp q).coeff (p.comp q).natDegree = 1
rw₂ : (p.comp q).coeff (p.natDegree * q.natDegree) = 1
rw₃ : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
rw₄ : 1 * q.leadingCoeff ^ p.natDegree = 1
rw₅ : 1 * HPow.hPow (α := R) 1 p.natDegree = 1
rw₆ : HMul.hMul (α := R) 1 1 = 1
rw₇ rw₈ : Eq.{u + 1} (α := R) 1 1
⊢ (p.comp q).Monic

Tactic:
rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]

Premises used: one_pow, Polynomial.leadingCoeff, Polynomial.Monic.def, Polynomial.Monic.leadingCoeff, mul_one, Polynomial.coeff_comp_degree_mul_degree
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
h : Nontrivial R
⊢ (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))).Monic

Tactic:
hp.comp (monic_X_add_C _) fun ha ↦ ?_

Premises used: Polynomial.monic_X_add_C, Polynomial.Monic.comp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
h : Nontrivial R
refine : ∀ (ha : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree = 0), False
⊢ (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))).Monic

Tactic:
refine hp.comp (monic_X_add_C _) fun ha ↦ ?_

Premises used: Polynomial.monic_X_add_C, Polynomial.Monic.comp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
h : Nontrivial R
ha : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).natDegree = 0
⊢ Eq (α := ℕ) 1 0

Tactic:
rw [natDegree_X_add_C] at ha

Premises used: Polynomial.natDegree_X_add_C
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
h : Nontrivial R
ha : Eq (α := ℕ) 1 0
⊢ False

Tactic:
one_ne_zero ha

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
h : Nontrivial R
ha : Eq (α := ℕ) 1 0
⊢ False

Tactic:
exact one_ne_zero ha

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
rw : p.degree ≤ 0 ↔ p.natDegree = 0
rw₁ rw₂ : p.degree ≤ 0 ↔ p.degree ≤ 0
⊢ p.degree ≤ 0 ↔ p = 1

Tactic:
rw [← hp.natDegree_eq_zero, natDegree_eq_zero_iff_degree_le_zero]

Premises used: Polynomial.Monic.natDegree_eq_zero, Polynomial.natDegree_eq_zero_iff_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h_1 : Nontrivial R
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
apply natDegree_mul'

Premises used: Polynomial.natDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simp [hp.leadingCoeff, hq.leadingCoeff]

Premises used: Polynomial.Monic.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
pos : ∀ (h : q = 0), (p * q).degree = (q * p).degree
neg : ∀ (h : ¬q = 0), (p * q).degree = (q * p).degree
⊢ (p * q).degree = (q * p).degree

Tactic:
by_cases h : q = 0
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).degree = (q * p).degree

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
neg : p.degree + q.degree = q.degree + p.degree
neg₁ : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).degree = (q * p).degree

Tactic:
rw [degree_mul', hp.degree_mul]

Premises used: Polynomial.degree_mul', Polynomial.Monic.degree_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = q.degree + p.degree

Tactic:
add_comm _ _

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = q.degree + p.degree

Tactic:
exact add_comm _ _

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
neg : 1 * q.leadingCoeff ≠ 0
neg₁ : q.leadingCoeff ≠ 0
neg₂ neg₃ neg₄ neg₅ : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]

Premises used: Polynomial.leadingCoeff_ne_zero, Polynomial.Monic.leadingCoeff, one_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
rw : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
rw [natDegree_mul']

Premises used: Polynomial.Monic.natDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

Premises used: Polynomial.leadingCoeff_ne_zero, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
pos : ∀ (h : q = 0), (p * q).natDegree = (q * p).natDegree
neg : ∀ (h : ¬q = 0), (p * q).natDegree = (q * p).natDegree
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
by_cases h : q = 0
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
neg : q.leadingCoeff * p.leadingCoeff ≠ 0
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
rw [hp.natDegree_mul' h, Polynomial.natDegree_mul', add_comm]

Premises used: Polynomial.natDegree_mul', add_comm, Polynomial.Monic.natDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q.leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

Premises used: Polynomial.leadingCoeff_ne_zero, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
a : R
g : R[X]
hfg : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * g = 1
hgf : g * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 1
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * g).natDegree =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree + g.natDegree

Tactic:
have h := (monic_X_add_C a).natDegree_mul' (right_ne_zero_of_mul_eq_one hfg)
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
a : R
g : R[X]
hfg : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * g = 1
hgf : g * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 1
h :
  (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * g).natDegree =
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree + g.natDegree
⊢ 0 = 1 + g.natDegree

Tactic:
rw [hfg, natDegree_one, natDegree_X_add_C] at h

Premises used: Polynomial.natDegree_X_add_C, Polynomial.natDegree_one
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
a : R
g : R[X]
hfg : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * g = 1
hgf : g * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = 1
h : 0 = 1 + g.natDegree
⊢ False

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
h0 : p * r ≠ 0
hl : (p * r).natDegree < p.natDegree
⊢ p.natDegree + r.natDegree < p.natDegree

Tactic:
rw [hp.natDegree_mul' <| right_ne_zero_of_mul h0] at hl

Premises used: right_ne_zero_of_mul, Polynomial.Monic.natDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
h0 : p * r ≠ 0
hl : p.natDegree + r.natDegree < p.natDegree
⊢ False

Tactic:
hl.not_ge (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, LT.lt.not_ge
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
h0 : p * r ≠ 0
hl : p.natDegree + r.natDegree < p.natDegree
⊢ False

Tactic:
exact hl.not_ge (Nat.le_add_right _ _)

Premises used: Nat.le_add_right, LT.lt.not_ge
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
h0 : q ≠ 0
hl : q.degree < p.degree
⊢ ¬p ∣ q

Tactic:
Monic.not_dvd_of_natDegree_lt hp h0 <| natDegree_lt_natDegree h0 hl

Premises used: Polynomial.Monic.not_dvd_of_natDegree_lt, Polynomial.natDegree_lt_natDegree
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
⊢ Nontrivial R

Tactic:
nontriviality
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Nontrivial R
simp : (p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1
⊢ (p * q).nextCoeff = p.nextCoeff + q.nextCoeff

Tactic:
simp only [← coeff_one_reverse]

Premises used: Polynomial.coeff_one_reverse
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Nontrivial R
rw : (p.reverse * q.reverse).coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1
rw₁ : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1

Tactic:
rw [reverse_mul]

Premises used: Polynomial.reverse_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Nontrivial R
⊢ (p.reverse * q.reverse).coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1

Tactic:
simp [hp.leadingCoeff, hq.leadingCoeff, mul_coeff_one, add_comm]

Premises used: add_comm, Polynomial.Monic.leadingCoeff, Polynomial.mul_coeff_one
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simp [hp.leadingCoeff, hq.leadingCoeff, mul_coeff_one, add_comm]

Premises used: add_comm, Polynomial.Monic.leadingCoeff, Polynomial.mul_coeff_one
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
zero : nextCoeff 1 = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
zero₁ : Eq.{u + 1} (α := R) (nextCoeff 1) 0
zero₂ : Eq.{u + 1} (α := R) (nextCoeff ((C : (a : R) → R[X]) 1)) 0
zero₃ zero₄ : Eq.{u + 1} (α := R) 0 0
⊢ (HPow.hPow (β := ℕ) p 0).nextCoeff = HSMul.hSMul (α := ℕ) 0 p.nextCoeff

Tactic:
rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]

Premises used: Polynomial.C, Polynomial.nextCoeff_C_eq_zero, pow_zero, zero_smul, map_one
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
succ : (p ^ n * p).nextCoeff = (n + 1) • p.nextCoeff
succ₁ : (p ^ n).nextCoeff + p.nextCoeff = (n + 1) • p.nextCoeff
succ₂ : n • p.nextCoeff + p.nextCoeff = (n + 1) • p.nextCoeff
succ₃ succ₄ : n • p.nextCoeff + p.nextCoeff = n • p.nextCoeff + p.nextCoeff
⊢ (p ^ (n + 1)).nextCoeff = (n + 1) • p.nextCoeff

Tactic:
rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]

Premises used: pow_succ, Polynomial.Monic.nextCoeff_mul, Polynomial.Monic.pow, succ_nsmul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).nextCoeff = HSMul.hSMul (α := ℕ) 0 p.nextCoeff
succ : ∀ (n : ℕ) (ih : (p ^ n).nextCoeff = n • p.nextCoeff), (p ^ (n + 1)).nextCoeff = (n + 1) • p.nextCoeff
⊢ (p ^ n).nextCoeff = n • p.nextCoeff

Tactic:
induction n with
  | zero => rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
  | succ n ih => rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]

Premises used: Polynomial.C, pow_succ, Polynomial.Monic.nextCoeff_mul, Polynomial.nextCoeff_C_eq_zero, pow_zero, zero_smul, map_one, Polynomial.Monic.pow, succ_nsmul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
rw : Ne.{u_1 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)
⊢ p.degree = 0

Tactic:
rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]

Premises used: Polynomial.degree_map_eq_of_leadingCoeff_ne_zero, Polynomial.degree_one
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
rw : Ne.{u_1 + 1} (α := S) 1 0
⊢ Ne.{u_1 + 1} (α := S) ((f : (a : R) → S) p.leadingCoeff : S) (0 : S)

Tactic:
rw [hp.leadingCoeff, f.map_one]

Premises used: RingHom.map_one, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
⊢ Ne.{u_1 + 1} (α := S) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
⊢ Ne.{u_1 + 1} (α := S) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
⊢ p.degree = 0

Tactic:
have hdeg : p.degree = 0 := by
    rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]
    · rw [hp.leadingCoeff, f.map_one]
      exact one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
hdeg : p.degree = 0
⊢ p.natDegree = 0

Tactic:
have hndeg : p.natDegree = 0 :=
    WithBot.coe_eq_coe.mp ((degree_eq_natDegree hp.ne_zero).symm.trans hdeg)
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
eq_C_of_degree_eq_zero hdeg

Premises used: Polynomial.eq_C_of_degree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h_1 : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
⊢ p = 1

Tactic:
convert! eq_C_of_degree_eq_zero hdeg

Premises used: Polynomial.eq_C_of_degree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
h_1 : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X])
h₁ : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
h₂ : Eq.{u + 1} (α := R[X]) 1 ((C : (a : R) → R[X]) 1)
h₃ h₄ : Eq.{u + 1} (α := R[X]) 1 1
⊢ Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])

Tactic:
rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]

Premises used: Polynomial.C, RingHom.map_one, Polynomial.leadingCoeff, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
⊢ (HPow.hPow (β := ℕ) p 0).natDegree = 0 * p.natDegree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
succ : (p ^ n * p).natDegree = (n + 1) * p.natDegree
succ₁ : (p ^ n).natDegree + p.natDegree = (n + 1) * p.natDegree
succ₂ : n * p.natDegree + p.natDegree = (n + 1) * p.natDegree
succ₃ : n * p.natDegree + p.natDegree = n * p.natDegree + p.natDegree
succ₄ succ₅ : p.natDegree + n * p.natDegree = p.natDegree + n * p.natDegree
⊢ (p ^ (n + 1)).natDegree = (n + 1) * p.natDegree

Tactic:
rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]

Premises used: pow_succ, add_comm, Nat.succ_mul, Polynomial.Monic.pow, Polynomial.Monic.natDegree_mul