awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p = (C : (a : R) → R[X]) (p.coeff 0)
rw : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0)) = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ p.natDegree = 0

Tactic:
rw [h, natDegree_C]

Premises used: Polynomial.natDegree_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hf : p.Monic
hfd : p.natDegree = 0
⊢ p.coeff 0 = 1

Tactic:
rw [Monic.def, leadingCoeff, hfd] at hf

Premises used: Polynomial.leadingCoeff, Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hf : p.Monic
hfd : p.natDegree = 0
hf₁ : p.coeff 0 = 1
⊢ p.natDegree = 0

Tactic:
rw [Monic.def, leadingCoeff, hfd] at hf

Premises used: Polynomial.leadingCoeff, Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
rw : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (1 : R[X])
rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
rw₂ rw₃ : Eq.{u + 1} (α := R[X]) 1 1
⊢ p = 1

Tactic:
rw [eq_C_of_natDegree_eq_zero hfd, hf, map_one]

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, map_one
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
hf : Monic.{u} (R := R) 1
⊢ natDegree.{u} (R := R) 1 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
f : Fin n → R
⊢ degree.{u} (R := R)
      (∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f i) : R[X]) (HPow.hPow (α := R[X]) X (↑i : ℕ))) <
    (↑n : WithBot ℕ)

Tactic:
(degree_sum_le _ _).trans_lt <|
    (Finset.sup_lt_iff <| WithBot.bot_lt_coe n).2 fun k _hk =>
      (degree_C_mul_X_pow_le _ _).trans_lt <| WithBot.coe_lt_coe.2 k.is_lt

Premises used: Iff.mpr, Fin.is_lt, Polynomial.degree_sum_le, Finset.sup_lt_iff, Polynomial.degree_C_mul_X_pow_le, Fin.val, WithBot.coe_lt_coe, WithBot.bot_lt_coe, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) b) <
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).degree

Tactic:
simpa only [degree_C_mul_X ha] using degree_C_lt

Premises used: Polynomial.degree_C_lt, Polynomial.degree_C_mul_X
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p ≠ 0
⊢ p.leadingCoeff * leadingCoeff X ≠ 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p ≠ 0
rw : p.natDegree + natDegree.{u} (R := R) X = p.natDegree + 1
rw₁ rw₂ : p.natDegree + 1 = p.natDegree + 1
⊢ (p * X).natDegree = p.natDegree + 1

Tactic:
rw [natDegree_mul' (by simpa), natDegree_X]

Premises used: Polynomial.natDegree_X, Polynomial.natDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p ≠ 0
rw : (p * X).natDegree = p.natDegree + 1
rw₁ rw₂ : p.natDegree + 1 = p.natDegree + 1
⊢ (X * p).natDegree = p.natDegree + 1

Tactic:
rw [commute_X p, natDegree_mul_X hp]

Premises used: Polynomial.natDegree_mul_X, Polynomial.commute_X
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.leadingCoeff * (HPow.hPow (α := R[X]) X n).leadingCoeff ≠ 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
rw : p.natDegree + (HPow.hPow (α := R[X]) X n).natDegree = p.natDegree + n
rw₁ rw₂ : p.natDegree + n = p.natDegree + n
⊢ (p * HPow.hPow (α := R[X]) X n).natDegree = p.natDegree + n

Tactic:
rw [natDegree_mul' (by simpa), natDegree_X_pow]

Premises used: Polynomial.natDegree_mul', Polynomial.natDegree_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
rw : (p * HPow.hPow (α := R[X]) X n).natDegree = p.natDegree + n
rw₁ rw₂ : p.natDegree + n = p.natDegree + n
⊢ (HPow.hPow (α := R[X]) X n * p).natDegree = p.natDegree + n

Tactic:
rw [commute_X_pow, natDegree_mul_X_pow n hp]

Premises used: Polynomial.natDegree_mul_X_pow, Polynomial.commute_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
h : Nontrivial R
rw rw₁ : n ≤ n
⊢ (HPow.hPow (α := R[X]) X n).natDegree ≤ n

Tactic:
rw [Polynomial.natDegree_X_pow]

Premises used: Polynomial.natDegree_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h : IsUnit.{u} (M := R[X]) X
g : R[X]
_hfg : (monomial 1 : (a : R) → R[X]) 1 * g = 1
hgf : g * (monomial 1 : (a : R) → R[X]) 1 = 1
rw : 0 = (g * (monomial 1 : (a : R) → R[X]) 1).coeff 0
⊢ Eq.{u + 1} (α := R) 0 1

Tactic:
rw [← coeff_one_zero, ← hgf]

Premises used: Polynomial.coeff_one_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h : IsUnit.{u} (M := R[X]) X
g : R[X]
_hfg : (monomial 1 : (a : R) → R[X]) 1 * g = 1
hgf : g * (monomial 1 : (a : R) → R[X]) 1 = 1
⊢ 0 = (g * (monomial 1 : (a : R) → R[X]) 1).coeff 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
⊢ (p * X).degree = p.degree + 1

Tactic:
simp [monic_X.degree_mul]

Premises used: Polynomial.Monic.degree_mul, Polynomial.monic_X
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
⊢ (p * HPow.hPow (α := R[X]) X n).degree = p.degree + (↑n : WithBot ℕ)

Tactic:
simp [(monic_X_pow n).degree_mul]

Premises used: Polynomial.monic_X_pow, Polynomial.Monic.degree_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Ring R
p : R[X]
hp : 0 < p.degree
rw : (HAdd.hAdd (β := R[X]) p (-(C : (a : R) → R[X]) a : R[X])).degree = p.degree
rw₁ : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) (-a) : R[X])).degree = p.degree
rw₂ rw₃ : p.degree = p.degree
⊢ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree

Tactic:
rw [sub_eq_add_neg, ← C_neg, degree_add_C hp]

Premises used: sub_eq_add_neg, Polynomial.C_neg, Polynomial.degree_add_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
rw : (HAdd.hAdd (β := R[X]) p (-(C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
rw₁ : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) (-a) : R[X])).natDegree = p.natDegree
rw₂ rw₃ : p.natDegree = p.natDegree
⊢ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree

Tactic:
rw [sub_eq_add_neg, ← C_neg, natDegree_add_C]

Premises used: sub_eq_add_neg, Polynomial.C_neg, Polynomial.natDegree_add_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree < p.degree
⊢ (-q).degree < p.degree

Tactic:
rw [← q.degree_neg] at h

Premises used: Polynomial.degree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : (-q).degree < p.degree
rw : (p + -q).leadingCoeff = p.leadingCoeff
rw₁ rw₂ : p.leadingCoeff = p.leadingCoeff
⊢ (p - q).leadingCoeff = p.leadingCoeff

Tactic:
rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt' h]

Premises used: sub_eq_add_neg, Polynomial.leadingCoeff_add_of_degree_lt'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < q.degree
⊢ p.degree < (-q).degree

Tactic:
rw [← q.degree_neg] at h

Premises used: Polynomial.degree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < (-q).degree
rw : (p + -q).leadingCoeff = -q.leadingCoeff
rw₁ : (-q).leadingCoeff = -q.leadingCoeff
rw₂ rw₃ : -q.leadingCoeff = -q.leadingCoeff
⊢ (p - q).leadingCoeff = -q.leadingCoeff

Tactic:
rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt h, leadingCoeff_neg]

Premises used: sub_eq_add_neg, Polynomial.leadingCoeff_add_of_degree_lt, Polynomial.leadingCoeff_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff ≠ q.leadingCoeff
rwa rwa₁ rwa₂ rwa₃ : p.degree = q.degree
⊢ p.degree = (-q).degree

Tactic:
rwa [q.degree_neg]

Premises used: Polynomial.degree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff ≠ q.leadingCoeff
⊢ p.degree = (-q).degree

Tactic:
replace h : degree p = degree (-q) := by rwa [q.degree_neg]
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
hlc : p.leadingCoeff ≠ q.leadingCoeff
h : p.degree = (-q).degree
rwa : ∀ (hlc : p.leadingCoeff - q.leadingCoeff ≠ 0) (h : p.degree = (-q).degree), p.leadingCoeff + (-q).leadingCoeff ≠ 0
rwa₁ :
  ∀ (hlc : p.leadingCoeff + -q.leadingCoeff ≠ 0) (h : p.degree = (-q).degree), p.leadingCoeff + (-q).leadingCoeff ≠ 0
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0) (h : p.degree = (-q).degree), p.leadingCoeff + (-q).leadingCoeff ≠ 0
⊢ p.leadingCoeff + (-q).leadingCoeff ≠ 0

Tactic:
rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc

Premises used: sub_ne_zero, sub_eq_add_neg, Polynomial.leadingCoeff_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
hlc : p.leadingCoeff ≠ q.leadingCoeff
h : p.degree = (-q).degree
⊢ p.leadingCoeff + (-q).leadingCoeff ≠ 0

Tactic:
replace hlc : leadingCoeff p + leadingCoeff (-q) ≠ 0 := by
    rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree = (-q).degree
hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0
rw : (p + -q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
rw₁ : p.leadingCoeff + (-q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
rw₂ : p.leadingCoeff + -q.leadingCoeff = p.leadingCoeff - q.leadingCoeff
rw₃ rw₄ : p.leadingCoeff + -q.leadingCoeff = p.leadingCoeff + -q.leadingCoeff
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff

Tactic:
rw [sub_eq_add_neg, leadingCoeff_add_of_degree_eq h hlc, leadingCoeff_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Polynomial.leadingCoeff_add_of_degree_eq, Polynomial.leadingCoeff_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree < p.degree
⊢ (-q).degree < p.degree

Tactic:
rw [← degree_neg q] at h

Premises used: Polynomial.degree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : (-q).degree < p.degree
rw : (p + -q).degree = p.degree
rw₁ rw₂ : p.degree = p.degree
⊢ (p - q).degree = p.degree

Tactic:
rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h]

Premises used: sub_eq_add_neg, Polynomial.degree_add_eq_left_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < q.degree
⊢ p.degree < (-q).degree

Tactic:
rw [← degree_neg q] at h

Premises used: Polynomial.degree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < (-q).degree
rw : (p + -q).degree = q.degree
rw₁ : (-q).degree = q.degree
rw₂ rw₃ : q.degree = q.degree
⊢ (p - q).degree = q.degree

Tactic:
rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg]

Premises used: Polynomial.degree_add_eq_right_of_degree_lt, sub_eq_add_neg, Polynomial.degree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.natDegree < p.natDegree
⊢ (p - q).natDegree = p.natDegree

Tactic:
natDegree_eq_of_degree_eq (degree_sub_eq_left_of_degree_lt (degree_lt_degree h))

Premises used: Polynomial.degree_lt_degree, Polynomial.degree_sub_eq_left_of_degree_lt, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.natDegree < q.natDegree
⊢ (p - q).natDegree = q.natDegree

Tactic:
natDegree_eq_of_degree_eq (degree_sub_eq_right_of_degree_lt (degree_lt_degree h))

Premises used: Polynomial.degree_lt_degree, Polynomial.natDegree_eq_of_degree_eq, Polynomial.degree_sub_eq_right_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
a : R
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) < degree.{u} (R := R) X

Tactic:
have : degree (C a) < degree (X : R[X]) :=
    calc
      degree (C a) ≤ 0 := degree_C_le
      _ < 1 := WithBot.coe_lt_coe.mpr zero_lt_one
      _ = degree X := degree_X.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
a : R
this : degree.{u} (R := R) ((C : (a : R) → R[X]) a) < degree.{u} (R := R) X
rw : degree.{u} (R := R) X = 1
rw₁ rw₂ : Eq (α := WithBot ℕ) 1 1
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree = 1

Tactic:
rw [degree_add_eq_left_of_degree_lt this, degree_X]

Premises used: Polynomial.degree_add_eq_left_of_degree_lt, Polynomial.degree_X
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
x : R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1

Tactic:
natDegree_eq_of_degree_eq_some <| degree_X_add_C x

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_X_add_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
S : Type v
inst : Semiring S
c : S
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
S : Type v
inst : Semiring S
c : S
h : Nontrivial S
⊢ (HAdd.hAdd (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) c : S[X])).nextCoeff = c

Tactic:
simp [nextCoeff_of_natDegree_pos]

Premises used: Polynomial.nextCoeff_of_natDegree_pos
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
rwa : LT.lt (α := WithBot ℕ) 0 (↑n : WithBot ℕ)
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < n
⊢ 0 < (HPow.hPow (α := R[X]) X n).degree

Tactic:
rwa [degree_X_pow, Nat.cast_pos]

Premises used: Nat.cast_pos, Polynomial.degree_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) < (HPow.hPow (α := R[X]) X n).degree

Tactic:
have : degree (C a) < degree ((X : R[X]) ^ n) := degree_C_le.trans_lt <| by
    rwa [degree_X_pow, Nat.cast_pos]
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
this : degree.{u} (R := R) ((C : (a : R) → R[X]) a) < (HPow.hPow (α := R[X]) X n).degree
rw : (HPow.hPow (α := R[X]) X n).degree = (↑n : WithBot ℕ)
rw₁ rw₂ : Eq (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)

Tactic:
rw [degree_add_eq_left_of_degree_lt this, degree_X_pow]

Premises used: Polynomial.degree_add_eq_left_of_degree_lt, Polynomial.degree_X_pow
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
rw : Ne (α := WithBot ℕ) (↑n : WithBot ℕ) ⊥
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree ≠ ⊥

Tactic:
rw [degree_X_pow_add_C hn a]

Premises used: Polynomial.degree_X_pow_add_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ Ne (α := WithBot ℕ) (↑n : WithBot ℕ) ⊥

Tactic:
WithBot.coe_ne_bot

Premises used: WithBot.coe_ne_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ Ne (α := WithBot ℕ) (↑n : WithBot ℕ) ⊥

Tactic:
exact WithBot.coe_ne_bot

Premises used: WithBot.coe_ne_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
r : R
⊢ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ≠ 0

Tactic:
pow_one (X : R[X]) ▸ X_pow_add_C_ne_zero zero_lt_one r

Premises used: Polynomial.X_pow_add_C_ne_zero, Eq.rec, zero_lt_one, pow_one, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
α : Type u_1
m : Multiset α
f : α → R
⊢ 0 ∉ Multiset.map (fun (a : α) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) m

Tactic:
fun mem =>
  let ⟨_a, _, ha⟩ := Multiset.mem_map.mp mem
  X_add_C_ne_zero _ ha

Premises used: False, Multiset.mem_map, Polynomial.X_add_C_ne_zero, Iff.mp, _private.0.Polynomial.zero_notMem_multiset_map_X_add_C.match_1, Not
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
r : R
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree = n

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
h : HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) = 1
⊢ n = 0

Tactic:
simpa only [natDegree_X_pow_add_C, natDegree_one] using congr_arg natDegree h

Premises used: Polynomial.natDegree_X_pow_add_C, congr_arg, Polynomial.natDegree_one, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
r : R
⊢ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ≠ 1

Tactic:
pow_one (X : R[X]) ▸ X_pow_add_C_ne_one zero_lt_one r

Premises used: Eq.rec, Polynomial.X_pow_add_C_ne_one, zero_lt_one, pow_one, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
r : R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
r : R
h : Nontrivial R
rw :
  (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff
      (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree =
    1
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff n = 1
rw₂ : (HPow.hPow (α := R[X]) X n).coeff n + coeff ((C : (a : R) → R[X]) r) n = 1
rw₃ : HAdd.hAdd (α := R) 1 (coeff ((C : (a : R) → R[X]) r) n) = 1
rw₄ : (1 + if n = 0 then r else 0) = 1
rw₅ : HAdd.hAdd (α := R) 1 0 = 1
rw₆ rw₇ : Eq.{u + 1} (α := R) 1 1
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1

Tactic:
rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
    if_neg (pos_iff_ne_zero.mp hn), add_zero]

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree_X_pow_add_C, Polynomial.coeff_add, Polynomial.coeff_C, Polynomial.coeff_X_pow_self, Iff.mp, add_zero, pos_iff_ne_zero, if_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
S : Type v
inst : Semiring S
r : S
rw : (HAdd.hAdd (β := S[X]) (HPow.hPow (α := S[X]) (β := ℕ) X 1) ((C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
rw₁ rw₂ : Eq.{v + 1} (α := S) 1 1
⊢ (HAdd.hAdd (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1

Tactic:
rw [← pow_one (X : S[X]), leadingCoeff_X_pow_add_C zero_lt_one]

Premises used: Polynomial.leadingCoeff_X_pow_add_C, zero_lt_one, pow_one, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
⊢ (HPow.hPow (α := R[X]) X n + 1).leadingCoeff = 1

Tactic:
leadingCoeff_X_pow_add_C hn

Premises used: Polynomial.leadingCoeff_X_pow_add_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
r : R
i : ℕ
⊢ Nontrivial R

Tactic:
nontriviality
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
r : R
i : ℕ
h : Nontrivial R
rw : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).leadingCoeff ^ i = 1
rw₁ : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).leadingCoeff ^ i ≠ 0
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i).leadingCoeff = 1

Tactic:
rw [leadingCoeff_pow']

Premises used: Polynomial.leadingCoeff_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
r : R
i : ℕ
h : Nontrivial R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).leadingCoeff ^ i = 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
r : R
i : ℕ
h : Nontrivial R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).leadingCoeff ^ i ≠ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
simp only [hp0, degree_zero, zero_mul, WithBot.bot_add]

Premises used: MulZeroClass.zero_mul, WithBot.bot_add, Polynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq0 : q = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
simp only [hq0, degree_zero, mul_zero, WithBot.add_bot]

Premises used: WithBot.add_bot, Polynomial.degree_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
p : R[X]
n : ℕ
⊢ (p ^ n).degree = n • p.degree

Tactic:
map_pow (@degreeMonoidHom R _ _ _) _ _

Premises used: Multiset.foldr, Finset.fold, map_pow, Polynomial.degree, Multiplicative, Finset.max, Finset.sup, Polynomial.degreeMonoidHom, Multiset.fold
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
pos : ∀ (hp : p = 0), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
neg : ∀ (hp : ¬p = 0), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
simp only [hp, zero_mul, leadingCoeff_zero]

Premises used: Polynomial.leadingCoeff_zero, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
pos : ∀ (hq : q = 0), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
neg : ∀ (hq : ¬q = 0), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
simp only [hq, mul_zero, leadingCoeff_zero]

Premises used: Polynomial.leadingCoeff_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
neg : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
rw [leadingCoeff_mul']

Premises used: Polynomial.leadingCoeff_mul'