awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact by_contra fun h => hy (if_neg h)

Premises used: by_contra, if_neg
-- 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
⊢ n ≤ y

Tactic:
have key : n ≤ y := by
      rw [mem_support_iff, coeff_mul_X_pow'] at hy
      exact by_contra fun h => hy (if_neg h)
-- 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
key : n ≤ y
⊢ p.coeff (y - n) ≠ 0

Tactic:
rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy

Premises used: Polynomial.mem_support_iff, if_pos, 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 : y ∈ (p * HPow.hPow (α := R[X]) X n).support
key : n ≤ y
hy₁ : p.coeff (y - n) ≠ 0
⊢ n ≤ y

Tactic:
rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy

Premises used: Polynomial.mem_support_iff, if_pos, 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 : p.coeff (y - n) ≠ 0
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y

Tactic:
(le_tsub_iff_right key).mp (natTrailingDegree_le_of_ne_zero hy)

Premises used: Iff.mp, le_tsub_iff_right, 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 y : ℕ
hy : p.coeff (y - n) ≠ 0
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y

Tactic:
exact (le_tsub_iff_right key).mp (natTrailingDegree_le_of_ne_zero hy)

Premises used: Iff.mp, le_tsub_iff_right, Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Tactic:
Finset.le_min fun n hn => ?_

Premises used: Finset.le_min, Polynomial.trailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
refine : ∀ (n : ℕ) (hn : n ∈ (p * q).support), p.trailingDegree + q.trailingDegree ≤ (↑n : WithTop ℕ)
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Tactic:
refine Finset.le_min fun n hn => ?_

Premises used: Finset.le_min
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ (p * q).support
⊢ Ne.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) 0

Tactic:
rw [mem_support_iff, coeff_mul] at hn

Premises used: Polynomial.mem_support_iff, Polynomial.coeff_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hn : Ne.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) 0
obtain :
  ∀ (i j : ℕ) (hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n) (hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0),
    p.trailingDegree + q.trailingDegree ≤ (↑n : WithTop ℕ)
⊢ p.trailingDegree + q.trailingDegree ≤ (↑n : WithTop ℕ)

Tactic:
obtain ⟨⟨i, j⟩, hij, hpq⟩ := exists_ne_zero_of_sum_ne_zero hn

Premises used: Finset.exists_ne_zero_of_sum_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hn : Ne.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) 0
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ (↑n : WithTop ℕ)

Tactic:
(add_le_add (min_le (mem_support_iff.mpr (left_ne_zero_of_mul hpq)))
          (min_le (mem_support_iff.mpr (right_ne_zero_of_mul hpq)))).trans_eq ?_

Premises used: Iff.mpr, LE.le.trans_eq, add_le_add, Finset.min_le, Polynomial.mem_support_iff, right_ne_zero_of_mul, left_ne_zero_of_mul, Polynomial.trailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hn : Ne.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) 0
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
this : (↑(i, j).1 : WithTop ℕ) + (↑(i, j).2 : WithTop ℕ) = (↑n : WithTop ℕ)
⊢ p.trailingDegree + q.trailingDegree ≤ (↑n : WithTop ℕ)

Tactic:
refine
    (add_le_add (min_le (mem_support_iff.mpr (left_ne_zero_of_mul hpq)))
          (min_le (mem_support_iff.mpr (right_ne_zero_of_mul hpq)))).trans_eq ?_

Premises used: Iff.mpr, LE.le.trans_eq, add_le_add, Finset.min_le, Polynomial.mem_support_iff, right_ne_zero_of_mul, left_ne_zero_of_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hn : Ne.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) 0
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
rwa : (↑((i, j).1 + (i, j).2) : WithTop ℕ) = (↑n : WithTop ℕ)
rwa₁ : (i, j).1 + (i, j).2 = n
rwa₂ rwa₃ rwa₄ rwa₅ : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ (↑(i, j).1 : WithTop ℕ) + (↑(i, j).2 : WithTop ℕ) = (↑n : WithTop ℕ)

Tactic:
rwa [← WithTop.coe_add, WithTop.coe_eq_coe, ← mem_antidiagonal]

Premises used: WithTop.coe_eq_coe, Finset.HasAntidiagonal.mem_antidiagonal, WithTop.coe_add
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p = 0
rw : 0 * q = 0
rw₁ rw₂ : Eq.{u + 1} (α := R[X]) 0 0
⊢ p * q = 0

Tactic:
rw [hp, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p * q ≠ 0
⊢ p ≠ 0

Tactic:
have hp : p ≠ 0 := fun hp => h (by rw [hp, zero_mul])
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q = 0
rw : p * 0 = 0
rw₁ rw₂ : Eq.{u + 1} (α := R[X]) 0 0
⊢ p * q = 0

Tactic:
rw [hq, mul_zero]

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

Tactic:
have hq : q ≠ 0 := fun hq => h (by rw [hq, mul_zero])
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw : p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree
⊢ p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree

Tactic:
rw [← WithTop.coe_le_coe, WithTop.coe_add, ← Nat.cast_withTop (natTrailingDegree p),
    ← Nat.cast_withTop (natTrailingDegree q), ← Nat.cast_withTop (natTrailingDegree (p * q)),
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq,
    ← trailingDegree_eq_natTrailingDegree h]

Premises used: HMul.hMul, Nat.cast_withTop, WithTop.coe_le_coe, Polynomial.trailingDegree_eq_natTrailingDegree, Polynomial.natTrailingDegree, WithTop.coe_add
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Tactic:
le_trailingDegree_mul

Premises used: Polynomial.le_trailingDegree_mul, WithTop
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree

Tactic:
exact le_trailingDegree_mul

Premises used: Polynomial.le_trailingDegree_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
rw :
  ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natTrailingDegree + q.natTrailingDegree), p.coeff x.1 * q.coeff x.2 =
    p.trailingCoeff * q.trailingCoeff
⊢ (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff

Tactic:
rw [coeff_mul]

Premises used: Polynomial.coeff_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natTrailingDegree + q.natTrailingDegree), p.coeff x.1 * q.coeff x.2 =
    p.trailingCoeff * q.trailingCoeff

Tactic:
Finset.sum_eq_single (p.natTrailingDegree, q.natTrailingDegree) ?_ fun h =>
      (h (mem_antidiagonal.mpr rfl)).elim

Premises used: Iff.mpr, False.elim, Prod.mk, Finset.sum_eq_single, Finset.HasAntidiagonal.mem_antidiagonal, Polynomial.trailingCoeff, ENat.toNat, WithTop.untopD, Polynomial.natTrailingDegree, WithTop.recTopCoe, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
fun :
  ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natTrailingDegree + q.natTrailingDegree),
    b ≠ (p.natTrailingDegree, q.natTrailingDegree) → p.coeff b.1 * q.coeff b.2 = 0
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natTrailingDegree + q.natTrailingDegree), p.coeff x.1 * q.coeff x.2 =
    p.trailingCoeff * q.trailingCoeff

Tactic:
refine
    Finset.sum_eq_single (p.natTrailingDegree, q.natTrailingDegree) ?_ fun h =>
      (h (mem_antidiagonal.mpr rfl)).elim

Premises used: Iff.mpr, False.elim, Prod.mk, Finset.sum_eq_single, Finset.HasAntidiagonal.mem_antidiagonal, Polynomial.natTrailingDegree, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natTrailingDegree + q.natTrailingDegree)
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
⊢ (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree

Tactic:
rw [mem_antidiagonal] at h₁

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natTrailingDegree + q.natTrailingDegree)
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
h₃ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
⊢ (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)

Tactic:
rw [mem_antidiagonal] at h₁

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
pos : ∀ (hi : i < p.natTrailingDegree), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
neg : ∀ (hi : p.natTrailingDegree ≤ i), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
by_cases! hi : i < p.natTrailingDegree

Premises used: Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : i < p.natTrailingDegree
pos : 0 * q.coeff (i, j).2 = 0
pos₁ pos₂ : Eq.{u + 1} (α := R) 0 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [coeff_eq_zero_of_lt_natTrailingDegree hi, zero_mul]

Premises used: Polynomial.coeff_eq_zero_of_lt_natTrailingDegree, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
pos : ∀ (hj : j < q.natTrailingDegree), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
neg : ∀ (hj : q.natTrailingDegree ≤ j), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
by_cases! hj : j < q.natTrailingDegree

Premises used: Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : j < q.natTrailingDegree
pos : p.coeff (i, j).1 * 0 = 0
pos₁ pos₂ : Eq.{u + 1} (α := R) 0 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [coeff_eq_zero_of_lt_natTrailingDegree hj, mul_zero]

Premises used: Polynomial.coeff_eq_zero_of_lt_natTrailingDegree, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : q.natTrailingDegree ≤ j
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
(h₂ (Prod.ext_iff.mpr ?_).symm).elim

Premises used: Iff.mpr, False.elim, Prod.ext_iff, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : q.natTrailingDegree ≤ j
neg : (p.natTrailingDegree, q.natTrailingDegree).1 = (i, j).1 ∧ (p.natTrailingDegree, q.natTrailingDegree).2 = (i, j).2
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
refine (h₂ (Prod.ext_iff.mpr ?_).symm).elim

Premises used: Iff.mpr, False.elim, Prod.ext_iff, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : q.natTrailingDegree ≤ j
⊢ (p.natTrailingDegree, q.natTrailingDegree).1 = (i, j).1 ∧ (p.natTrailingDegree, q.natTrailingDegree).2 = (i, j).2

Tactic:
(add_eq_add_iff_eq_and_eq hi hj).mp h₁.symm

Premises used: add_eq_add_iff_eq_and_eq, Iff.mp, ENat.toNat, WithTop.untopD, Polynomial.natTrailingDegree, Eq.symm, WithTop.recTopCoe
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : q.natTrailingDegree ≤ j
⊢ (p.natTrailingDegree, q.natTrailingDegree).1 = (i, j).1 ∧ (p.natTrailingDegree, q.natTrailingDegree).2 = (i, j).2

Tactic:
exact (add_eq_add_iff_eq_and_eq hi hj).mp h₁.symm

Premises used: add_eq_add_iff_eq_and_eq, Iff.mp, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p = 0
rw : trailingCoeff 0 * q.trailingCoeff = 0
rw₁ : 0 * q.trailingCoeff = 0
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ p.trailingCoeff * q.trailingCoeff = 0

Tactic:
rw [hp, trailingCoeff_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.trailingCoeff_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
⊢ p ≠ 0

Tactic:
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
rw : p.trailingCoeff * trailingCoeff 0 = 0
rw₁ : p.trailingCoeff * 0 = 0
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ p.trailingCoeff * q.trailingCoeff = 0

Tactic:
rw [hq, trailingCoeff_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.trailingCoeff_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
⊢ q ≠ 0

Tactic:
have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
le_antisymm ?_ le_trailingDegree_mul

Premises used: Polynomial.le_trailingDegree_mul, le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
refine : (p * q).trailingDegree ≤ p.trailingDegree + q.trailingDegree
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
refine le_antisymm ?_ le_trailingDegree_mul

Premises used: Polynomial.le_trailingDegree_mul, le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw : (p * q).trailingDegree ≤ (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
⊢ (p * q).trailingDegree ≤ p.trailingDegree + q.trailingDegree

Tactic:
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq, ←
    ENat.coe_add]

Premises used: Polynomial.trailingDegree_eq_natTrailingDegree, ENat.coe_add
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
h₁ : (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) ≠ 0
⊢ (p * q).trailingDegree ≤ (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)

Tactic:
apply trailingDegree_le_of_ne_zero

Premises used: Polynomial.trailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
h₁ h₂ h₃ h₄ : p.trailingCoeff * q.trailingCoeff ≠ 0
⊢ (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) ≠ 0

Tactic:
rwa [coeff_mul_natTrailingDegree_add_natTrailingDegree]

Premises used: Polynomial.coeff_mul_natTrailingDegree_add_natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
h₁ : (p * q).trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Tactic:
apply natTrailingDegree_eq_of_trailingDegree_eq_some

Premises used: Polynomial.natTrailingDegree_eq_of_trailingDegree_eq_some
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
h₁ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
h₂ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : WithTop ℕ)
h₃ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
h₄ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
h₅ :
  p.trailingDegree + q.trailingDegree =
    HAdd.hAdd (α := WithTop ℕ) (↑p.natTrailingDegree : WithTop ℕ) (↑q.natTrailingDegree : WithTop ℕ)
h₆ : p.trailingDegree + q.trailingDegree = p.trailingDegree + (↑q.natTrailingDegree : WithTop ℕ)
h₇ h₈ : p.trailingDegree + q.trailingDegree = p.trailingDegree + q.trailingDegree
⊢ (p * q).trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)

Tactic:
rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
    WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]

Premises used: Nat.cast_withTop, HAdd.hAdd, Polynomial.trailingDegree_eq_natTrailingDegree, Polynomial.natTrailingDegree, Polynomial.trailingDegree_mul', WithTop.coe_add
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Tactic:
natTrailingDegree_mul'
    (mul_ne_zero (mt trailingCoeff_eq_zero.mp hp) (mt trailingCoeff_eq_zero.mp hq))

Premises used: mt, Iff.mp, mul_ne_zero, Polynomial.trailingCoeff_eq_zero, Polynomial.natTrailingDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ trailingDegree.{u} (R := R) 1 = 0

Tactic:
trailingDegree_C one_ne_zero

Premises used: Polynomial.trailingDegree_C, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
⊢ trailingDegree.{u} (R := R) X = 1

Tactic:
trailingDegree_monomial one_ne_zero

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

Tactic:
natTrailingDegree_monomial one_ne_zero

Premises used: Polynomial.natTrailingDegree_monomial, one_ne_zero, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
rw : trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) 1) = (↑n : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
⊢ (HPow.hPow (α := R[X]) X n).trailingDegree = (↑n : ℕ∞)

Tactic:
rw [X_pow_eq_monomial, trailingDegree_monomial one_ne_zero]

Premises used: Polynomial.X_pow_eq_monomial, one_ne_zero, Polynomial.trailingDegree_monomial
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
rw : natTrailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) 1) = n
rw₁ rw₂ : n = n
⊢ (HPow.hPow (α := R[X]) X n).natTrailingDegree = n

Tactic:
rw [X_pow_eq_monomial, natTrailingDegree_monomial one_ne_zero]

Premises used: Polynomial.X_pow_eq_monomial, Polynomial.natTrailingDegree_monomial, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Ring R
p : R[X]
rw rw₁ : p.support.min = p.support.min
⊢ (-p).support.min = p.support.min

Tactic:
rw [support_neg]

Premises used: Polynomial.support_neg
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ (-p).natTrailingDegree = p.natTrailingDegree

Tactic:
simp [natTrailingDegree]

Premises used: Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Ring R
n : ℤ
⊢ natTrailingDegree.{u} (R := R) (↑n : R[X]) = 0

Tactic:
simp only [← C_eq_intCast, natTrailingDegree_C]

Premises used: Polynomial.natTrailingDegree_C, Polynomial.C_eq_intCast
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R) (nextCoeffUp 0) 0

Tactic:
simp [nextCoeffUp]

Premises used: Polynomial.nextCoeffUp
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
c : R
⊢ Eq.{u + 1} (α := R)
    (if natTrailingDegree.{u} (R := R) ((C : (a : R) → R[X]) c) = 0 then 0
    else coeff ((C : (a : R) → R[X]) c) (natTrailingDegree.{u} (R := R) ((C : (a : R) → R[X]) c) + 1))
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.coeff 0 = 0
inl :
  ∀ (hp : Eq.{u + 1} (α := R) (coeff 0 0) 0),
    Eq.{u + 1} (α := R) (nextCoeffUp 0) (coeff 0 (natTrailingDegree.{u} (R := R) 0 + 1))
inr : ∀ (hp₀ : p ≠ 0), p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)

Tactic:
obtain rfl | hp₀ := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Goal:
R : Type u
inst : Semiring R
hp : Eq.{u + 1} (α := R) (coeff 0 0) 0
⊢ Eq.{u + 1} (α := R) (nextCoeffUp 0) (coeff 0 (natTrailingDegree.{u} (R := R) 0 + 1))

Tactic:
simp