awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a - r
h₁ : ∀ (q : R[X]), q * b + r = q * b - -r
convert! : (-r).natDegree < m
⊢ ∃ (q : R[X]), q.IsMonicOfDegree (m - n) ∧ a = q * b + r

Tactic:
convert! ha.of_dvd_add hmn hb ?_ h using 4 with q

Premises used: Polynomial.IsMonicOfDegree.of_dvd_add
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a - r
q : R[X]
h₁ h₂ : q * b + r = q * b + r
⊢ q * b + r = q * b - -r

Tactic:
rw [sub_neg_eq_add]

Premises used: sub_neg_eq_add
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a - r
rwa rwa₁ rwa₂ rwa₃ : r.natDegree < m
⊢ (-r).natDegree < m

Tactic:
rwa [natDegree_neg]

Premises used: Polynomial.natDegree_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
inl :
  ∀ (H : Subsingleton R),
    IsMonicOfDegree.{u_1} (R := R)
      ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n
inr :
  ∀ (H : Nontrivial R),
    IsMonicOfDegree.{u_1} (R := R)
      ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) 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 : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Subsingleton R
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n

Tactic:
simpa using hp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Nontrivial R
inr :
  IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) (n * 1)
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n

Tactic:
rw [← mul_one n]

Premises used: mul_one
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Nontrivial R
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) (n * 1)

Tactic:
hp.comp one_ne_zero (isMonicOfDegree_X_add_one r)

Premises used: Polynomial.isMonicOfDegree_X_add_one, Polynomial.C, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.IsMonicOfDegree.comp, one_ne_zero, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Nontrivial R
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) (n * 1)

Tactic:
exact hp.comp one_ne_zero (isMonicOfDegree_X_add_one r)

Premises used: Polynomial.isMonicOfDegree_X_add_one, Polynomial.IsMonicOfDegree.comp, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
rw :
  IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) : (a : R[X]) → R[X]) p) n
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) : (a : R[X]) → R[X]) p) n

Tactic:
rw [sub_eq_add_neg, ← map_neg]

Premises used: sub_eq_add_neg, map_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) : (a : R[X]) → R[X]) p) n

Tactic:
aeval_add hp (-r)

Premises used: Polynomial.IsMonicOfDegree.aeval_add, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Goal:
R : Type u_1
inst : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
⊢ IsMonicOfDegree.{u_1} (R := R)
    ((aeval (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-r) : R[X])) : (a : R[X]) → R[X]) p) n

Tactic:
exact aeval_add hp (-r)

Premises used: Polynomial.IsMonicOfDegree.aeval_add, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
rw : 0 ≤ p.natDegree * q.natDegree
⊢ (p.comp q).natDegree ≤ p.natDegree * q.natDegree

Tactic:
rw [h0, natDegree_zero]

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ 0 ≤ p.natDegree * q.natDegree

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ 0 ≤ p.natDegree * q.natDegree

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
grw grw₁ :
  (↑(natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff n))) : WithBot ℕ) +
      HSMul.hSMul (β := WithBot ℕ) n (↑q.natDegree : WithBot ℕ) ≤
    (↑(natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff n))) : WithBot ℕ) +
      HSMul.hSMul (β := WithBot ℕ) n (↑q.natDegree : WithBot ℕ)
⊢ (↑(natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff n))) : WithBot ℕ) + n • q.degree ≤
    (↑(natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff n))) : WithBot ℕ) +
      HSMul.hSMul (β := WithBot ℕ) n (↑q.natDegree : WithBot ℕ)

Tactic:
grw [degree_le_natDegree]

Premises used: Polynomial.degree_le_natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
rw : HMul.hMul (α := WithBot ℕ) (↑n : WithBot ℕ) (↑q.natDegree : WithBot ℕ) = (↑(n * q.natDegree) : WithBot ℕ)
⊢ (↑(natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff n))) : WithBot ℕ) +
      HSMul.hSMul (β := WithBot ℕ) n (↑q.natDegree : WithBot ℕ) =
    (↑(n * q.natDegree) : WithBot ℕ)

Tactic:
rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul]

Premises used: Polynomial.natDegree_C, zero_add, nsmul_eq_mul, Nat.cast_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ HMul.hMul (α := WithBot ℕ) (↑n : WithBot ℕ) (↑q.natDegree : WithBot ℕ) = (↑(n * q.natDegree) : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
a : n ≤ p.natDegree
⊢ LE.le (α := ℕ) (↑(n * q.natDegree) : ℕ) (↑(p.natDegree * q.natDegree) : ℕ)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ n ≤ p.natDegree

Tactic:
le_natDegree_of_ne_zero (mem_support_iff.1 hn)

Premises used: Polynomial.mem_support_iff, Iff.mp, Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ n ≤ p.natDegree

Tactic:
exact le_natDegree_of_ne_zero (mem_support_iff.1 hn)

Premises used: Polynomial.mem_support_iff, Iff.mp, Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
pos : ∀ (hq : q.natDegree = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
neg : ∀ (hq : ¬q.natDegree = 0), (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
by_cases hq : natDegree q = 0

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

Tactic:
simp [hq]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
exact le_antisymm natDegree_comp_le (by simp [hq])

Premises used: le_antisymm, Polynomial.natDegree_comp_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
neg : (p.comp q).coeff (p.natDegree * q.natDegree) ≠ 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
apply natDegree_eq_of_le_of_coeff_ne_zero natDegree_comp_le

Premises used: Polynomial.natDegree_eq_of_le_of_coeff_ne_zero, Polynomial.natDegree_comp_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
neg neg₁ neg₂ neg₃ : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) ≠ 0

Tactic:
rwa [coeff_comp_degree_mul_degree hq]

Premises used: Polynomial.coeff_comp_degree_mul_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : p.degree ≤ 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
have := eq_C_of_degree_le_zero hlt
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : p.degree ≤ 0
this : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ p.coeff 0 = 0

Tactic:
rw [IsRoot, this, eval_C] at h

Premises used: Polynomial.eval_C, Polynomial.IsRoot
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : p.degree ≤ 0
this : p = (C : (a : R) → R[X]) (p.coeff 0)
h₁ : p.coeff 0 = 0
⊢ p.degree ≤ 0

Tactic:
rw [IsRoot, this, eval_C] at h

Premises used: Polynomial.eval_C, Polynomial.IsRoot
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : p.degree ≤ 0
this : p = (C : (a : R) → R[X]) (p.coeff 0)
h₁ : p.coeff 0 = 0
hlt₁ : p.degree ≤ 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
rw [IsRoot, this, eval_C] at h

Premises used: Polynomial.eval_C, Polynomial.IsRoot
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : p.degree ≤ 0
this : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ p = 0

Tactic:
simp only [h, map_zero] at this

Premises used: map_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : p.degree ≤ 0
this : p = 0
⊢ False

Tactic:
hp this
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
hp : p ≠ 0
h : p.coeff 0 = 0
hlt : p.degree ≤ 0
this : p = 0
⊢ False

Tactic:
exact hp this
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
simp_rw : p.degree ≤ (↑n : WithBot ℕ) ↔ ∀ (N : ℕ), n < N → p.coeff N = 0
simp_rw₁ :
  (∀ (m : ℕ), LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑m : WithBot ℕ) → p.coeff m = 0) ↔
    ∀ (N : ℕ), n < N → p.coeff N = 0
⊢ p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0

Tactic:
simp_rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero, Nat.cast_lt]

Premises used: Polynomial.degree_le_iff_coeff_zero, Nat.cast_lt, Polynomial.natDegree_le_iff_degree_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
⊢ (p + q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
⟨fun h => ?_, fun h => natDegree_add_le_of_degree_le h qn⟩

Premises used: Polynomial.natDegree_add_le_of_degree_le, Iff.intro
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
refine : ∀ (h : (p + q).natDegree ≤ n), p.natDegree ≤ n
⊢ (p + q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
refine ⟨fun h => ?_, fun h => natDegree_add_le_of_degree_le h qn⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
⊢ p.natDegree ≤ n

Tactic:
natDegree_le_iff_coeff_eq_zero.mpr fun m hm => ?_

Premises used: Iff.mpr, Polynomial.natDegree_le_iff_coeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
refine : ∀ (m : ℕ) (hm : n < m), p.coeff m = 0
⊢ p.natDegree ≤ n

Tactic:
refine natDegree_le_iff_coeff_eq_zero.mpr fun m hm => ?_

Premises used: Iff.mpr, Polynomial.natDegree_le_iff_coeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ (p + q).coeff m = 0

Tactic:
natDegree_le_iff_coeff_eq_zero.mp h m hm

Premises used: Polynomial.natDegree_le_iff_coeff_eq_zero, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
h₁ : p.coeff m = (p + q).coeff m
⊢ p.coeff m = 0

Tactic:
convert! natDegree_le_iff_coeff_eq_zero.mp h m hm using 1

Premises used: Polynomial.natDegree_le_iff_coeff_eq_zero, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
h₁ : p.coeff m = p.coeff m + q.coeff m
h₂ : p.coeff m = p.coeff m + 0
h₃ h₄ : p.coeff m = p.coeff m
⊢ p.coeff m = (p + q).coeff m

Tactic:
rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]

Premises used: Polynomial.natDegree_le_iff_coeff_eq_zero, Polynomial.coeff_add, Iff.mp, add_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
pn : p.natDegree ≤ n
rw : (q + p).natDegree ≤ n ↔ q.natDegree ≤ n
⊢ (p + q).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
pn : p.natDegree ≤ n
⊢ (q + p).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
natDegree_add_le_iff_left _ _ pn

Premises used: Polynomial.natDegree_add_le_iff_left
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
pn : p.natDegree ≤ n
⊢ (q + p).natDegree ≤ n ↔ q.natDegree ≤ n

Tactic:
exact natDegree_add_le_iff_left _ _ pn

Premises used: Polynomial.natDegree_add_le_iff_left
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
a : R
f : R[X]
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f).natDegree ≤ f.natDegree

Tactic:
simpa using natDegree_mul_le (p := C a)

Premises used: Polynomial.natDegree_mul_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
f : R[X]
a : R
⊢ (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) a : R[X])).natDegree ≤ f.natDegree

Tactic:
simpa using natDegree_mul_le (q := C a)

Premises used: Polynomial.natDegree_mul_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
ns : n ∈ p.support
⊢ p.natDegree = n

Tactic:
le_antisymm pn (le_natDegree_of_mem_supp _ ns)

Premises used: Polynomial.le_natDegree_of_mem_supp, le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : ai * a = 1
nth_rw nth_rw₁ : (1 * p).natDegree = (1 * p).natDegree
⊢ p.natDegree = (1 * p).natDegree

Tactic:
nth_rw 1 [← one_mul p]

Premises used: one_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : ai * a = 1
rw :
  ((C : (a : R) → R[X]) 1 * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (ai * a) : R[X]) p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
rw₂ :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ai : R[X]) ((C : (a : R) → R[X]) a : R[X]) * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
rw₃ rw₄ :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ai : R[X]) ((C : (a : R) → R[X]) a : R[X]) * p).natDegree =
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ai : R[X]) ((C : (a : R) → R[X]) a : R[X]) * p).natDegree
⊢ (1 * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree

Tactic:
rw [← C_1, ← au, map_mul, ← mul_assoc]

Premises used: Polynomial.C_1, mul_assoc, map_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : a * ai = 1
nth_rw nth_rw₁ : (p * 1).natDegree = (p * 1).natDegree
⊢ p.natDegree = (p * 1).natDegree

Tactic:
nth_rw 1 [← mul_one p]

Premises used: mul_one
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : a * ai = 1
rw :
  (p * (C : (a : R) → R[X]) 1).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
rw₁ :
  (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (a * ai) : R[X])).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
rw₂ :
  (p * HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) ai : R[X])).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
rw₃ rw₄ :
  (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
⊢ (p * 1).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree

Tactic:
rw [← C_1, ← au, map_mul, ← mul_assoc]

Premises used: Polynomial.C_1, mul_assoc, map_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree

Tactic:
eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) ?_

Premises used: Polynomial.natDegree_mul_C_le, Polynomial.eq_natDegree_of_le_mem_support
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
refine : p.natDegree ∈ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).support
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree

Tactic:
refine eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) ?_

Premises used: Polynomial.natDegree_mul_C_le, Polynomial.eq_natDegree_of_le_mem_support
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ p.natDegree ∈ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).support

Tactic:
mem_support_iff.mpr ?_

Premises used: Iff.mpr, Polynomial.mem_support_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
refine : (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff p.natDegree ≠ 0
⊢ p.natDegree ∈ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).support

Tactic:
refine mem_support_iff.mpr ?_

Premises used: Iff.mpr, Polynomial.mem_support_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
rwa rwa₁ rwa₂ rwa₃ : p.coeff p.natDegree * a ≠ 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff p.natDegree ≠ 0

Tactic:
rwa [coeff_mul_C]

Premises used: Polynomial.coeff_mul_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree = p.natDegree

Tactic:
eq_natDegree_of_le_mem_support (natDegree_C_mul_le a p) ?_

Premises used: Polynomial.natDegree_C_mul_le, Polynomial.eq_natDegree_of_le_mem_support
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
refine : p.natDegree ∈ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).support
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree = p.natDegree

Tactic:
refine eq_natDegree_of_le_mem_support (natDegree_C_mul_le a p) ?_

Premises used: Polynomial.natDegree_C_mul_le, Polynomial.eq_natDegree_of_le_mem_support
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ p.natDegree ∈ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).support

Tactic:
mem_support_iff.mpr ?_

Premises used: Iff.mpr, Polynomial.mem_support_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
refine : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff p.natDegree ≠ 0
⊢ p.natDegree ∈ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).support

Tactic:
refine mem_support_iff.mpr ?_

Premises used: Iff.mpr, Polynomial.mem_support_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
rwa rwa₁ rwa₂ rwa₃ : a * p.coeff p.natDegree ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff p.natDegree ≠ 0

Tactic:
rwa [coeff_C_mul]

Premises used: Polynomial.coeff_C_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ leadingCoeff ((C : (a : R) → R[X]) a) * p.leadingCoeff ≠ 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
rw : degree.{u} (R := R) ((C : (a : R) → R[X]) a) + p.degree = p.degree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree

Tactic:
rw [degree_mul' (by simpa)]

Premises used: Polynomial.degree_mul'