awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
rw : p.leadingCoeff * leadingCoeff 0 = 0
rw₁ : p.leadingCoeff * 0 = 0
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ p.leadingCoeff * q.leadingCoeff = 0

Tactic:
rw [hq, leadingCoeff_zero, mul_zero]

Premises used: Polynomial.leadingCoeff_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
⊢ q = 0 → p.leadingCoeff * q.leadingCoeff = 0

Tactic:
exact fun hq => by rw [hq, leadingCoeff_zero, mul_zero]
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw : HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ) ≤ (p * q).degree
⊢ p.degree + q.degree ≤ (p * q).degree

Tactic:
rw [degree_eq_natDegree hp, degree_eq_natDegree hq]

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ) ≤ (p * q).degree

Tactic:
le_degree_of_ne_zero (n := natDegree p + natDegree q) ?_

Premises used: WithBot.some, Polynomial.le_degree_of_ne_zero, WithBot.map₂, Option.map₂
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
refine : (p * q).coeff (p.natDegree + q.natDegree) ≠ 0
⊢ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ) ≤ (p * q).degree

Tactic:
refine le_degree_of_ne_zero (n := natDegree p + natDegree q) ?_

Premises used: Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rwa rwa₁ rwa₂ rwa₃ : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).coeff (p.natDegree + q.natDegree) ≠ 0

Tactic:
rwa [coeff_mul_degree_add_degree]

Premises used: Polynomial.coeff_mul_degree_add_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : p = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
rwa : p.leadingCoeff * 1 ≠ 0
rwa₁ : p.leadingCoeff ≠ 0
rwa₂ : ¬p.leadingCoeff = 0
rwa₃ rwa₄ rwa₅ rwa₆ : ¬p = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rwa [hq.leadingCoeff, mul_one, Ne, leadingCoeff_eq_zero]

Premises used: Ne, Polynomial.Monic.leadingCoeff, mul_one, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
h₁ : p.leadingCoeff = 0
rw : 0 * q.leadingCoeff = 0
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ p.leadingCoeff * q.leadingCoeff = 0

Tactic:
rw [h₁, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
h₁ : q.leadingCoeff = 0
rw : p.leadingCoeff * 0 = 0
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ p.leadingCoeff * q.leadingCoeff = 0

Tactic:
rw [h₁, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw : p.degree + q.degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
rw₁ : p.degree + q.degree = HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
rw₂ :
  (↑p.natDegree : WithBot ℕ) + q.degree =
    HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
rw₃ rw₄ :
  HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ) =
    HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ (p * q).degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)

Tactic:
rw [degree_mul' h, Nat.cast_add, degree_eq_natDegree hp, degree_eq_natDegree hq]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.degree_mul', Nat.cast_add
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
simp [← coeff_natDegree, natDegree_mul' h, coeff_mul_degree_add_degree]

Premises used: Polynomial.coeff_natDegree, Polynomial.natDegree_mul', Polynomial.coeff_mul_degree_add_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
pos : ∀ (hr : r = 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).leadingCoeff = r
neg : ∀ (hr : ¬r = 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).leadingCoeff = r
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).leadingCoeff = r

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
hr : r = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).leadingCoeff = r

Tactic:
simp_all [leadingCoeff_mul']

Premises used: Polynomial.leadingCoeff_mul'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
hr : ¬r = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).leadingCoeff = r

Tactic:
simp_all [leadingCoeff_mul']

Premises used: Polynomial.leadingCoeff_mul'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
⊢ p.leadingCoeff ^ Nat.zero ≠ 0 → (p ^ Nat.zero).leadingCoeff = p.leadingCoeff ^ Nat.zero

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n = 0
rw : p.leadingCoeff ^ n * p.leadingCoeff = 0
rw₁ : 0 * p.leadingCoeff = 0
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ p.leadingCoeff ^ n.succ = 0

Tactic:
rw [pow_succ, h₁, zero_mul]

Premises used: pow_succ, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
rwa :
  ∀ (h : p.leadingCoeff * p.leadingCoeff ^ n ≠ 0) (h₁ : p.leadingCoeff ^ n ≠ 0),
    p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0) (h₁ : p.leadingCoeff ^ n ≠ 0),
    p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0

Tactic:
rwa [pow_succ', ← ih h₁] at h

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0

Tactic:
have h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0 := by rwa [pow_succ', ← ih h₁] at h
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
rw : (p * p ^ n).leadingCoeff = p.leadingCoeff ^ n.succ
rw₁ : (p * p ^ n).leadingCoeff = p.leadingCoeff * p.leadingCoeff ^ n
rw₂ : p.leadingCoeff * (p ^ n).leadingCoeff = p.leadingCoeff * p.leadingCoeff ^ n
rw₃ rw₄ : p.leadingCoeff * p.leadingCoeff ^ n = p.leadingCoeff * p.leadingCoeff ^ n
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ

Tactic:
rw [pow_succ', pow_succ', leadingCoeff_mul' h₂, ih h₁]

Premises used: Polynomial.leadingCoeff_mul', pow_succ'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : HPow.hPow (β := ℕ) p.leadingCoeff 0 ≠ 0
⊢ Ne.{u + 1} (α := R) 1 0

Tactic:
rw [pow_zero, ← C_1] at *

Premises used: Polynomial.C_1, pow_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Ne.{u + 1} (α := R) 1 0
rw : 0 = HSMul.hSMul (α := ℕ) 0 p.degree
rw₁ rw₂ : Eq (α := WithBot ℕ) 0 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) 1) = HSMul.hSMul (α := ℕ) 0 p.degree

Tactic:
rw [degree_C h, zero_nsmul]

Premises used: Polynomial.degree_C, zero_nsmul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n = 0
rw : p.leadingCoeff ^ n * p.leadingCoeff = 0
rw₁ : 0 * p.leadingCoeff = 0
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ p.leadingCoeff ^ (n + 1) = 0

Tactic:
rw [pow_succ, h₁, zero_mul]

Premises used: pow_succ, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
rwa :
  ∀ (h : p.leadingCoeff ^ n * p.leadingCoeff ≠ 0) (h₁ : p.leadingCoeff ^ n ≠ 0),
    (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0) (h₁ : p.leadingCoeff ^ n ≠ 0),
    (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
rwa [pow_succ, ← leadingCoeff_pow' h₁] at h

Premises used: pow_succ, Polynomial.leadingCoeff_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
have h₂ : leadingCoeff (p ^ n) * leadingCoeff p ≠ 0 := by
      rwa [pow_succ, ← leadingCoeff_pow' h₁] at h
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
rw : (p ^ n * p).degree = (n + 1) • p.degree
rw₁ : (p ^ n).degree + p.degree = (n + 1) • p.degree
rw₂ : (p ^ n).degree + p.degree = n • p.degree + p.degree
rw₃ rw₄ : n • p.degree + p.degree = n • p.degree + p.degree
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree

Tactic:
rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]

Premises used: pow_succ, Polynomial.degree_mul', succ_nsmul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : n = 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : ¬n = 0
rw : natDegree.{u} (R := R) 0 = n * natDegree.{u} (R := R) 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
rw [hp0, zero_pow hn0]

Premises used: zero_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : ¬n = 0
⊢ natDegree.{u} (R := R) 0 = n * natDegree.{u} (R := R) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
have h1 := h
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ Ne.{u + 1} (α := R) 0 0

Tactic:
rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h

Premises used: Polynomial.leadingCoeff_zero, Polynomial.leadingCoeff_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
h₁ : Ne.{u + 1} (α := R) 0 0
⊢ ¬p = 0

Tactic:
rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h

Premises used: Polynomial.leadingCoeff_zero, Polynomial.leadingCoeff_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
h₁ : Ne.{u + 1} (α := R) 0 0
hp0₁ : ¬p = 0
⊢ p ^ n = 0

Tactic:
rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h

Premises used: Polynomial.leadingCoeff_zero, Polynomial.leadingCoeff_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
h₁ : Ne.{u + 1} (α := R) 0 0
hp0₁ : ¬p = 0
hpn0₁ : p ^ n = 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h

Premises used: Polynomial.leadingCoeff_zero, Polynomial.leadingCoeff_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : Ne.{u + 1} (α := R) 0 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ False

Tactic:
h rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : Ne.{u + 1} (α := R) 0 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ False

Tactic:
exact h rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
rw : HSMul.hSMul (β := WithBot ℕ) n (↑p.natDegree : WithBot ℕ) = (↑(n * p.natDegree) : WithBot ℕ)
⊢ Eq (α := WithBot ℕ) (↑(p ^ n).natDegree : WithBot ℕ) (↑(n * p.natDegree) : WithBot ℕ)

Tactic:
rw [← degree_eq_natDegree hpn, degree_pow' h, degree_eq_natDegree hp0]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.degree_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ HSMul.hSMul (β := WithBot ℕ) n (↑p.natDegree : WithBot ℕ) = (↑(n * p.natDegree) : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
inl : (p * 0).leadingCoeff = leadingCoeff 0
inr : ∀ (H : q ≠ 0), (p * q).leadingCoeff = q.leadingCoeff
⊢ (p * q).leadingCoeff = q.leadingCoeff

Tactic:
rcases eq_or_ne q 0 with (rfl | H)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
⊢ (p * 0).leadingCoeff = leadingCoeff 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
inr : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff

Tactic:
rw [leadingCoeff_mul', hp.leadingCoeff, one_mul]

Premises used: Polynomial.leadingCoeff_mul', Polynomial.Monic.leadingCoeff, one_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
inr : 1 * q.leadingCoeff ≠ 0
inr₁ : q.leadingCoeff ≠ 0
inr₂ : ¬q.leadingCoeff = 0
inr₃ inr₄ inr₅ inr₆ : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rwa [hp.leadingCoeff, one_mul, Ne, leadingCoeff_eq_zero]

Premises used: Ne, Polynomial.Monic.leadingCoeff, Polynomial.leadingCoeff_eq_zero, one_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff = 0
rw : (p * q).leadingCoeff = 0
rw₁ : (0 * q).leadingCoeff = 0
rw₂ : Eq.{u + 1} (α := R) (leadingCoeff 0) 0
rw₃ rw₄ : Eq.{u + 1} (α := R) 0 0
⊢ (p * q).leadingCoeff = p.leadingCoeff

Tactic:
rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_zero]

Premises used: Polynomial.leadingCoeff_zero, MulZeroClass.zero_mul, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
rw : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = p.leadingCoeff

Tactic:
rw [leadingCoeff_mul', hq.leadingCoeff, mul_one]

Premises used: Polynomial.leadingCoeff_mul', Polynomial.Monic.leadingCoeff, mul_one
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
rwa : p.leadingCoeff * 1 ≠ 0
rwa₁ rwa₂ rwa₃ rwa₄ : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rwa [hq.leadingCoeff, mul_one]

Premises used: Polynomial.Monic.leadingCoeff, mul_one
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
inl : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])).degree = degree.{u} (R := R) 0
inr : ∀ (hp : p ≠ 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree

Tactic:
obtain rfl | hp := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])).degree = degree.{u} (R := R) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
h : Nontrivial R
rw : 0 + p.degree = p.degree
rw₁ : leadingCoeff ((C : (a : R) → R[X]) a) * p.leadingCoeff ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree

Tactic:
rw [degree_mul', degree_C ha.ne_zero]

Premises used: Polynomial.degree_C, Polynomial.degree_mul', IsUnit.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
h : Nontrivial R
⊢ 0 + p.degree = p.degree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
h : Nontrivial R
⊢ leadingCoeff ((C : (a : R) → R[X]) a) * p.leadingCoeff ≠ 0

Tactic:
simpa [ha.mul_right_eq_zero]

Premises used: IsUnit.mul_right_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
inl : (HMul.hMul (α := R[X]) (β := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) a : R[X])).degree = degree.{u} (R := R) 0
inr : ∀ (hp : p ≠ 0), (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree

Tactic:
obtain rfl | hp := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
⊢ (HMul.hMul (α := R[X]) (β := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) a : R[X])).degree = degree.{u} (R := R) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
h : Nontrivial R
rw : p.degree + 0 = p.degree
rw₁ : p.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) a) ≠ 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree

Tactic:
rw [degree_mul', degree_C ha.ne_zero]

Premises used: Polynomial.degree_C, Polynomial.degree_mul', IsUnit.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
h : Nontrivial R
⊢ p.degree + 0 = p.degree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
h : Nontrivial R
⊢ p.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) a) ≠ 0

Tactic:
simpa [ha.mul_left_eq_zero]

Premises used: IsUnit.mul_left_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree = p.natDegree

Tactic:
simp [natDegree, degree_C_mul_of_isUnit ha]

Premises used: Polynomial.degree_C_mul_of_isUnit, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree

Tactic:
simp [natDegree, degree_mul_C_of_isUnit ha]

Premises used: Polynomial.degree_mul_C_of_isUnit, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
rwa :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree =
    a * p.leadingCoeff
rwa₁ : a * p.coeff (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree = a * p.leadingCoeff
rwa₂ : a * p.coeff p.natDegree = a * p.leadingCoeff
ha₁ : IsUnit a
rwa₃ : a * p.coeff p.natDegree = a * p.coeff p.natDegree
ha₂ : IsUnit a
rwa₄ : a * p.coeff p.natDegree = a * p.coeff p.natDegree
ha₃ ha₄ ha₅ : IsUnit a
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).leadingCoeff = a * p.leadingCoeff

Tactic:
rwa [leadingCoeff, coeff_C_mul, natDegree_C_mul_of_isUnit, leadingCoeff]

Premises used: Polynomial.coeff_C_mul, Polynomial.leadingCoeff, Polynomial.natDegree_C_mul_of_isUnit
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
rwa :
  (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff
      (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree =
    p.leadingCoeff * a
rwa₁ : p.coeff (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree * a = p.leadingCoeff * a
rwa₂ : p.coeff p.natDegree * a = p.leadingCoeff * a
ha₁ : IsUnit a
rwa₃ : p.coeff p.natDegree * a = p.coeff p.natDegree * a
ha₂ : IsUnit a
rwa₄ : p.coeff p.natDegree * a = p.coeff p.natDegree * a
ha₃ ha₄ ha₅ : IsUnit a
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff * a

Tactic:
rwa [leadingCoeff, coeff_mul_C, natDegree_mul_C_of_isUnit, leadingCoeff]

Premises used: Polynomial.leadingCoeff, Polynomial.coeff_mul_C, Polynomial.natDegree_mul_C_of_isUnit