awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
rw : p.trailingDegree = (↑n : ℕ∞) ↔ p.trailingDegree.toNat = n
rw₁ rw₂ : p.trailingDegree = (↑n : ℕ∞) ↔ p.trailingDegree = (↑n : ℕ∞)
⊢ p.trailingDegree = (↑n : ℕ∞) ↔ p.natTrailingDegree = n

Tactic:
rw [natTrailingDegree, ENat.toNat_eq_iff hn]

Premises used: ENat.toNat_eq_iff, Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.trailingDegree = (↑n : ℕ∞)
⊢ p.natTrailingDegree = n

Tactic:
simp [natTrailingDegree, h]

Premises used: Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (↑p.natTrailingDegree : ℕ∞) ≤ p.trailingDegree

Tactic:
ENat.coe_toNat_le_self _

Premises used: ENat.coe_toNat_le_self, Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
q : S[X]
h : p.trailingDegree = q.trailingDegree
rw rw₁ : q.trailingDegree.toNat = q.trailingDegree.toNat
⊢ p.trailingDegree.toNat = q.trailingDegree.toNat

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p.trailingDegree ≤ (↑n : ℕ∞)

Tactic:
min_le (mem_support_iff.2 h)

Premises used: Iff.mpr, Finset.min_le, Polynomial.mem_support_iff, Polynomial.trailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p.natTrailingDegree ≤ n

Tactic:
ENat.toNat_le_of_le_coe <| trailingDegree_le_of_ne_zero h

Premises used: Polynomial.trailingDegree_le_of_ne_zero, ENat.toNat_le_of_le_coe, Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
mp : p.coeff p.natTrailingDegree = 0 → p = 0
mpr : p = 0 → p.coeff p.natTrailingDegree = 0
⊢ p.coeff p.natTrailingDegree = 0 ↔ p = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
mp : ∀ (hp : ¬p = 0), False
⊢ p = 0

Tactic:
by_contra hp
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
⊢ ∃ (a : ℕ), ¬p.coeff a = 0 ∧ (↑a : WithTop ℕ) = p.support.min

Tactic:
simpa using min_mem_image_coe <| support_nonempty.2 hp

Premises used: Iff.mpr, Finset.min_mem_image_coe, Polynomial.support_nonempty
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
mp : ∀ (n : ℕ) (hpn : ¬p.coeff n = 0) (hn : (↑n : WithTop ℕ) = p.support.min), False
⊢ False

Tactic:
obtain ⟨n, hpn, hn⟩ := by simpa using min_mem_image_coe <| support_nonempty.2 hp
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
n : ℕ
hpn : ¬p.coeff n = 0
hn : (↑n : WithTop ℕ) = p.support.min
⊢ ¬p.coeff p.natTrailingDegree = 0

Tactic:
obtain rfl := (trailingDegree_eq_iff_natTrailingDegree_eq hp).1 hn.symm

Premises used: Iff.mp, Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq, Eq.symm, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
n : ℕ
hpn : ¬p.coeff n = 0
hn : (↑n : WithTop ℕ) = p.support.min
hpn₁ : ¬p.coeff p.natTrailingDegree = 0
⊢ (↑p.natTrailingDegree : WithTop ℕ) = p.support.min

Tactic:
obtain rfl := (trailingDegree_eq_iff_natTrailingDegree_eq hp).1 hn.symm

Premises used: Iff.mp, Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq, Eq.symm, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
hpn : ¬p.coeff p.natTrailingDegree = 0
hn : (↑p.natTrailingDegree : WithTop ℕ) = p.support.min
⊢ False

Tactic:
hpn h
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
hpn : ¬p.coeff p.natTrailingDegree = 0
hn : (↑p.natTrailingDegree : WithTop ℕ) = p.support.min
⊢ False

Tactic:
exact hpn h
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (coeff 0 (natTrailingDegree.{u} (R := R) 0)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.coeff p.natTrailingDegree ≠ 0 ↔ p ≠ 0

Tactic:
coeff_natTrailingDegree_eq_zero.not

Premises used: Polynomial.coeff_natTrailingDegree_eq_zero, Iff.not
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.trailingDegree = 0 ↔ p.coeff 0 ≠ 0

Tactic:
Finset.min_eq_bot.trans mem_support_iff

Premises used: Polynomial.mem_support_iff, WithTop.some, Finset.min_eq_bot, ENat, Polynomial.trailingDegree, Iff.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.natTrailingDegree = 0 ↔ p = 0 ∨ p.coeff 0 ≠ 0

Tactic:
simp [natTrailingDegree, or_comm]

Premises used: or_comm, Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : ¬p = 0 ∧ ¬p.coeff 0 ≠ 0 ↔ p ≠ 0 ∧ p.coeff 0 = 0
rw₁ rw₂ : ¬p = 0 ∧ p.coeff 0 = 0 ↔ p ≠ 0 ∧ p.coeff 0 = 0
⊢ ¬(p = 0 ∨ p.coeff 0 ≠ 0) ↔ p ≠ 0 ∧ p.coeff 0 = 0

Tactic:
rw [not_or, not_ne_iff]

Premises used: not_ne_iff, not_or
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.trailingDegree ≠ 0 ↔ p.coeff 0 = 0

Tactic:
trailingDegree_eq_zero.not_left

Premises used: Polynomial.trailingDegree_eq_zero, Iff.not_left
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.coeff p.natTrailingDegree ≠ 0
⊢ q.trailingDegree ≤ p.trailingDegree

Tactic:
(trailingDegree_le_of_ne_zero h).trans natTrailingDegree_le_trailingDegree

Premises used: Polynomial.trailingDegree_le_of_ne_zero, Polynomial.natTrailingDegree_le_trailingDegree, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff 0 ≠ 0
rw : p.coeff p.natTrailingDegree = p.coeff 0
rw₁ rw₂ : p.coeff 0 = p.coeff 0
⊢ p.trailingCoeff = p.coeff 0

Tactic:
rw [trailingCoeff, (natTrailingDegree_eq_zero.mpr <| .inr h)]

Premises used: Iff.mpr, Polynomial.natTrailingDegree_eq_zero, Polynomial.trailingCoeff, Or.inr
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.trailingDegree = (↑n : ℕ∞)
rw : p.trailingDegree.toNat = n
rw₁ : ENat.toNat (↑n : ℕ∞) = n
rw₂ rw₃ : n = n
⊢ p.natTrailingDegree = n

Tactic:
rw [natTrailingDegree, h, ENat.toNat_coe]

Premises used: ENat.toNat_coe, Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
H : (↑n : ℕ∞) ≤ p.trailingDegree
rwa : ∀ (H : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑p.natTrailingDegree : ℕ∞)), n ≤ p.natTrailingDegree
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (H : n ≤ p.natTrailingDegree), n ≤ p.natTrailingDegree
⊢ n ≤ p.natTrailingDegree

Tactic:
rwa [trailingDegree_eq_natTrailingDegree hp, Nat.cast_le] at H

Premises used: Nat.cast_le, Polynomial.trailingDegree_eq_natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q ≠ 0
hpq : p.trailingDegree ≤ q.trailingDegree
⊢ q.trailingDegree ≠ ⊤

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
ha : a ≠ 0
rw : (↑n : WithTop ℕ) = (↑n : ℕ∞)
⊢ trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : ℕ∞)

Tactic:
rw [trailingDegree, support_monomial n ha, min_singleton]

Premises used: Polynomial.support_monomial, Polynomial.trailingDegree, Finset.min_singleton
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
ha : a ≠ 0
⊢ (↑n : WithTop ℕ) = (↑n : ℕ∞)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
ha : a ≠ 0
rw : ENat.toNat (↑n : ℕ∞) = n
⊢ natTrailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = n

Tactic:
rw [natTrailingDegree, trailingDegree_monomial ha]

Premises used: Polynomial.natTrailingDegree, Polynomial.trailingDegree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
ha : a ≠ 0
⊢ ENat.toNat (↑n : ℕ∞) = n

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
this : DecidableEq R := Classical.decEq R
ha : a = 0
⊢ natTrailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) ≤ n

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
this : DecidableEq R := Classical.decEq R
ha : a = 0
⊢ (↑n : ℕ∞) ≤ trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
a : R
inst : Semiring R
ha : a ≠ 0
⊢ trailingDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0

Tactic:
trailingDegree_monomial ha

Premises used: WithTop.some, Polynomial.trailingDegree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
a : R
inst : Semiring R
⊢ 0 ≤ trailingDegree.{u} (R := R) ((C : (a : R) → R[X]) a)

Tactic:
le_trailingDegree_monomial

Premises used: Polynomial.le_trailingDegree_monomial, WithTop.some
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ 0 ≤ trailingDegree.{u} (R := R) ((C : (a : R) → R[X]) 1)

Tactic:
le_trailingDegree_C

Premises used: Polynomial.le_trailingDegree_C
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ 0 ≤ trailingDegree.{u} (R := R) ((C : (a : R) → R[X]) 1)

Tactic:
exact le_trailingDegree_C

Premises used: Polynomial.le_trailingDegree_C
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
a : R
⊢ natTrailingDegree.{u} (R := R) ((C : (a : R) → R[X]) a) = 0

Tactic:
nonpos_iff_eq_zero.1 natTrailingDegree_monomial_le

Premises used: Iff.mp, Polynomial.natTrailingDegree_monomial_le, nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ natTrailingDegree.{u} (R := R) 1 = 0

Tactic:
natTrailingDegree_C 1

Premises used: Polynomial.natTrailingDegree_C, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ natTrailingDegree.{u} (R := R) (↑n : R[X]) = 0

Tactic:
simp only [← C_eq_natCast, natTrailingDegree_C]

Premises used: Polynomial.natTrailingDegree_C, Polynomial.C_eq_natCast
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
ha : a ≠ 0
rw : trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).trailingDegree = (↑n : ℕ∞)

Tactic:
rw [C_mul_X_pow_eq_monomial, trailingDegree_monomial ha]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.trailingDegree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
rw : (↑n : ℕ∞) ≤ trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)
⊢ (↑n : ℕ∞) ≤ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).trailingDegree

Tactic:
rw [C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ (↑n : ℕ∞) ≤ trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)

Tactic:
le_trailingDegree_monomial

Premises used: Polynomial.le_trailingDegree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ (↑n : ℕ∞) ≤ trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)

Tactic:
exact le_trailingDegree_monomial

Premises used: Polynomial.le_trailingDegree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
h : (↑n : ℕ∞) < p.trailingDegree
⊢ p.coeff n = 0

Tactic:
Classical.not_not.1 (mt trailingDegree_le_of_ne_zero (not_le_of_gt h))

Premises used: Classical.not_not, mt, Polynomial.trailingDegree_le_of_ne_zero, Iff.mp, not_le_of_gt
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
h₁ : (↑n : ℕ∞) < p.trailingDegree
⊢ p.coeff n = 0

Tactic:
apply coeff_eq_zero_of_lt_trailingDegree

Premises used: Polynomial.coeff_eq_zero_of_lt_trailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
pos : ∀ (hp : p = 0), (↑n : ℕ∞) < p.trailingDegree
neg : ∀ (hp : ¬p = 0), (↑n : ℕ∞) < p.trailingDegree
⊢ (↑n : ℕ∞) < p.trailingDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
pos : LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤
⊢ (↑n : ℕ∞) < p.trailingDegree

Tactic:
rw [hp, trailingDegree_zero]

Premises used: Polynomial.trailingDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤

Tactic:
WithTop.coe_lt_top n

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤

Tactic:
exact WithTop.coe_lt_top n

Premises used: WithTop.coe_lt_top
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
neg : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑p.natTrailingDegree : ℕ∞)
⊢ (↑n : ℕ∞) < p.trailingDegree

Tactic:
rw [trailingDegree_eq_natTrailingDegree hp]

Premises used: Polynomial.trailingDegree_eq_natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑p.natTrailingDegree : ℕ∞)

Tactic:
WithTop.coe_lt_coe.2 h

Premises used: Iff.mpr, WithTop.coe_lt_coe
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑p.natTrailingDegree : ℕ∞)

Tactic:
exact WithTop.coe_lt_coe.2 h

Premises used: Iff.mpr, WithTop.coe_lt_coe
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : LT.lt (α := ℕ∞) 0 (↑p.natTrailingDegree : ℕ∞)
⊢ p.coeff (p.natTrailingDegree - 1) = 0

Tactic:
coeff_eq_zero_of_lt_natTrailingDegree <|
    Nat.sub_lt (WithTop.coe_pos.mp hp) Nat.one_pos

Premises used: Nat.one_pos, Polynomial.coeff_eq_zero_of_lt_natTrailingDegree, Nat.sub_lt, Iff.mp, WithTop.coe_pos
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (↑n : ℕ∞) ≤ (HPow.hPow (α := R[X]) X n).trailingDegree

Tactic:
simpa only [C_1, one_mul] using le_trailingDegree_C_mul_X_pow n (1 : R)

Premises used: Polynomial.C_1, Polynomial.le_trailingDegree_C_mul_X_pow, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ 1 ≤ trailingDegree.{u} (R := R) X

Tactic:
le_trailingDegree_monomial

Premises used: Polynomial.le_trailingDegree_monomial, WithTop.some, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ natTrailingDegree.{u} (R := R) X ≤ 1

Tactic:
natTrailingDegree_monomial_le

Premises used: Polynomial.natTrailingDegree_monomial_le, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.trailingCoeff = 0 ↔ p = 0

Tactic:
⟨fun h =>
    _root_.by_contradiction fun hp =>
      mt mem_support_iff.1 (Classical.not_not.2 h)
        (mem_of_min (trailingDegree_eq_natTrailingDegree hp)),
    fun h => h.symm ▸ leadingCoeff_zero⟩

Premises used: Iff.mpr, Classical.not_not, Polynomial.leadingCoeff_zero, mt, Eq.rec, Polynomial.mem_support_iff, Finset.mem_of_min, Iff.intro, by_contradiction, Iff.mp, Polynomial.trailingDegree_eq_natTrailingDegree, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.trailingCoeff ≠ 0 ↔ p ≠ 0

Tactic:
not_congr trailingCoeff_eq_zero

Premises used: Polynomial.trailingCoeff_eq_zero, not_congr
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p ≠ 0 → p.natTrailingDegree ∈ p.support

Tactic:
mem_support_iff.mpr ∘ trailingCoeff_nonzero_iff_nonzero.mpr

Premises used: Iff.mpr, Function.comp, Polynomial.mem_support_iff, Polynomial.trailingCoeff_nonzero_iff_nonzero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : ℕ
⊢ a ∈ p.support → p.natTrailingDegree ≤ a

Tactic:
natTrailingDegree_le_of_ne_zero ∘ mem_support_iff.mp

Premises used: Function.comp, Polynomial.mem_support_iff, Iff.mp, Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
rw : p.trailingDegree.toNat = p.support.min' ⋯
rw₁ : ENat.toNat p.support.min = p.support.min' ⋯
rw₂ : ENat.toNat (↑(p.support.min' ⋯) : WithTop ℕ) = p.support.min' ⋯
rw₃ : p.support.Nonempty
rw₄ : ENat.toNat (↑(p.support.min' ⋯) : WithTop ℕ) = p.support.min' ⋯
rw₅ : p.support.Nonempty
rw₆ : p.support.min' ⋯ = p.support.min' ⋯
rw₇ : p.support.Nonempty
rw₈ : p.support.min' ⋯ = p.support.min' ⋯
rw₉ : p.support.Nonempty
⊢ p.natTrailingDegree = p.support.min' ⋯

Tactic:
rw [natTrailingDegree, trailingDegree, ← Finset.coe_min', ENat.some_eq_coe, ENat.toNat_coe]

Premises used: ENat.some_eq_coe, Finset.coe_min', Polynomial.trailingDegree, ENat.toNat_coe, Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hp : p ≠ 0
hn : ∀ m < n, p.coeff m = 0
rw : n ≤ p.support.min' ⋯
⊢ n ≤ p.natTrailingDegree

Tactic:
rw [natTrailingDegree_eq_support_min' hp]

Premises used: Polynomial.natTrailingDegree_eq_support_min'
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hp : p ≠ 0
hn : ∀ m < n, p.coeff m = 0
⊢ n ≤ p.support.min' ⋯

Tactic:
Finset.le_min' _ _ _ fun m hm => not_lt.1 fun hmn => mem_support_iff.1 hm <| hn _ hmn

Premises used: Polynomial.mem_support_iff, not_lt, Iff.mp, Finset.le_min'
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hp : p ≠ 0
hn : ∀ m < n, p.coeff m = 0
⊢ n ≤ p.support.min' ⋯

Tactic:
exact Finset.le_min' _ _ _ fun m hm => not_lt.1 fun hmn => mem_support_iff.1 hm <| hn _ hmn

Premises used: Polynomial.mem_support_iff, not_lt, Iff.mp, Finset.le_min'
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
pos : ∀ (hp : p = 0), p.natTrailingDegree ≤ p.natDegree
neg : ∀ (hp : ¬p = 0), p.natTrailingDegree ≤ p.natDegree
⊢ p.natTrailingDegree ≤ p.natDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p = 0
pos : natTrailingDegree.{u} (R := R) 0 ≤ natDegree.{u} (R := R) 0
pos₁ : natTrailingDegree.{u} (R := R) 0 ≤ 0
pos₂ pos₃ : LE.le (α := ℕ) 0 0
⊢ p.natTrailingDegree ≤ p.natDegree

Tactic:
rw [hp, natDegree_zero, natTrailingDegree_zero]

Premises used: Polynomial.natDegree_zero, Polynomial.natTrailingDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.natTrailingDegree ≤ p.natDegree

Tactic:
le_natDegree_of_ne_zero (mt trailingCoeff_eq_zero.mp hp)

Premises used: mt, Iff.mp, Polynomial.le_natDegree_of_ne_zero, Polynomial.trailingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.natTrailingDegree ≤ p.natDegree

Tactic:
exact le_natDegree_of_ne_zero (mt trailingCoeff_eq_zero.mp hp)

Premises used: mt, Iff.mp, Polynomial.le_natDegree_of_ne_zero, Polynomial.trailingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
a : (p * HPow.hPow (α := R[X]) X n).natTrailingDegree ≤ p.natTrailingDegree + n
a₁ : p.natTrailingDegree + n ≤ (p * HPow.hPow (α := R[X]) X n).natTrailingDegree
⊢ (p * HPow.hPow (α := R[X]) X n).natTrailingDegree = p.natTrailingDegree + n

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * HPow.hPow (α := R[X]) X n).natTrailingDegree ≤ p.natTrailingDegree + n

Tactic:
natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp ?_

Premises used: mt, Iff.mp, Polynomial.trailingCoeff_eq_zero, Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
a : ∀ (h : (p * HPow.hPow (α := R[X]) X n).coeff (p.natTrailingDegree + n) = 0), p.trailingCoeff = 0
⊢ (p * HPow.hPow (α := R[X]) X n).natTrailingDegree ≤ p.natTrailingDegree + n

Tactic:
refine natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp ?_

Premises used: mt, Iff.mp, Polynomial.trailingCoeff_eq_zero, Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * HPow.hPow (α := R[X]) X n).coeff (p.natTrailingDegree + n) = 0
a : p.coeff p.natTrailingDegree = 0
a₁ : (p * HPow.hPow (α := R[X]) X n).coeff (p.natTrailingDegree + n) = 0
a₂ : ℕ
a₃ : (p * HPow.hPow (α := R[X]) X n).coeff (p.natTrailingDegree + n) = 0
a₄ : ℕ
a₅ : (p * HPow.hPow (α := R[X]) X n).coeff (p.natTrailingDegree + n) = 0
a₆ : ℕ
a₇ : (p * HPow.hPow (α := R[X]) X n).coeff (p.natTrailingDegree + n) = 0
a₈ : ℕ
⊢ p.trailingCoeff = 0

Tactic:
rwa [trailingCoeff, ← coeff_mul_X_pow]

Premises used: Polynomial.coeff_mul_X_pow, Polynomial.trailingCoeff
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
a : ∀ y ∈ (p * HPow.hPow (α := R[X]) X n).support, p.natTrailingDegree + n ≤ y
⊢ p.natTrailingDegree + n ≤ (p * HPow.hPow (α := R[X]) X n).natTrailingDegree

Tactic:
rw [natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h), Finset.le_min'_iff]

Premises used: Polynomial.mul_X_pow_eq_zero, Polynomial.natTrailingDegree_eq_support_min', Finset.le_min'_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * HPow.hPow (α := R[X]) X n).support
⊢ (if n ≤ y then p.coeff (y - n) else 0) ≠ 0

Tactic:
rw [mem_support_iff, coeff_mul_X_pow'] at hy

Premises used: Polynomial.mem_support_iff, Polynomial.coeff_mul_X_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : (if n ≤ y then p.coeff (y - n) else 0) ≠ 0
⊢ n ≤ y

Tactic:
by_contra fun h => hy (if_neg h)

Premises used: by_contra, if_neg