awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.degree
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) < p.natDegree

Tactic:
rw [degree_eq_natDegree hp, Nat.cast_pos, ← natDegree_C a] at hpd

Premises used: Nat.cast_pos, Polynomial.degree_eq_natDegree, Polynomial.natDegree_C
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) < p.natDegree
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree

Tactic:
natDegree_add_eq_left_of_natDegree_lt hpd

Premises used: Polynomial.natDegree_add_eq_left_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : natDegree.{u} (R := R) ((C : (a : R) → R[X]) a) < p.natDegree
⊢ (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree

Tactic:
exact natDegree_add_eq_left_of_natDegree_lt hpd

Premises used: Polynomial.natDegree_add_eq_left_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : R
⊢ (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree = p.natDegree

Tactic:
simp [add_comm _ p]

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : p.degree < q.degree
rw : max p.degree q.degree ≤ q.degree
rw₁ rw₂ : q.degree ≤ q.degree
⊢ max p.degree q.degree ≤ (p + q).degree

Tactic:
rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]

Premises used: max_eq_right_of_lt, Polynomial.degree_add_eq_right_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : max p.degree q.degree > (p + q).degree
⊢ q.degree > (p + q).degree

Tactic:
rw [HEq, max_self] at hlt

Premises used: max_self
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
rw : (p + q).coeff q.natDegree = 0
⊢ p.leadingCoeff + q.leadingCoeff = 0

Tactic:
rw [leadingCoeff, leadingCoeff, natDegree_eq_of_degree_eq HEq, ← coeff_add]

Premises used: Polynomial.leadingCoeff, Polynomial.coeff_add, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ (p + q).coeff q.natDegree = 0

Tactic:
coeff_natDegree_eq_zero_of_degree_lt hlt

Premises used: Polynomial.coeff_natDegree_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ (p + q).coeff q.natDegree = 0

Tactic:
exact coeff_natDegree_eq_zero_of_degree_lt hlt

Premises used: Polynomial.coeff_natDegree_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : q.degree < p.degree
rw : max p.degree q.degree ≤ p.degree
rw₁ rw₂ : p.degree ≤ p.degree
⊢ max p.degree q.degree ≤ (p + q).degree

Tactic:
rw [degree_add_eq_left_of_degree_lt hlt, max_eq_left_of_lt hlt]

Premises used: Polynomial.degree_add_eq_left_of_degree_lt, max_eq_left_of_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
by_contra : ∀ (h : ¬p.natDegree = q.natDegree), False
⊢ p.natDegree = q.natDegree

Tactic:
by_contra h
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h_1 : ¬p.natDegree = q.natDegree
h : p.natDegree < q.natDegree
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (H : q.natDegree < p.natDegree) (h : ¬p.natDegree = q.natDegree) (h : p.natDegree < q.natDegree),
    q.natDegree < p.natDegree
⊢ q.natDegree < p.natDegree

Tactic:
rwa [natDegree_add_eq_right_of_natDegree_lt h] at H

Premises used: Polynomial.natDegree_add_eq_right_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h_1 : ¬p.natDegree = q.natDegree
h : p.natDegree < q.natDegree
⊢ False

Tactic:
exact lt_asymm h (by rwa [natDegree_add_eq_right_of_natDegree_lt h] at H)

Premises used: lt_asymm
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h_1 : ¬p.natDegree = q.natDegree
h : q.natDegree < p.natDegree
⊢ p.natDegree < p.natDegree

Tactic:
rw [natDegree_add_eq_left_of_natDegree_lt h] at H

Premises used: Polynomial.natDegree_add_eq_left_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h_1 : ¬p.natDegree = q.natDegree
h : q.natDegree < p.natDegree
H₁ : p.natDegree < p.natDegree
⊢ ¬p.natDegree = q.natDegree

Tactic:
rw [natDegree_add_eq_left_of_natDegree_lt h] at H

Premises used: Polynomial.natDegree_add_eq_left_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h_1 : ¬p.natDegree = q.natDegree
h : q.natDegree < p.natDegree
H₁ : p.natDegree < p.natDegree
h₁ : ¬p.natDegree = q.natDegree
⊢ q.natDegree < p.natDegree

Tactic:
rw [natDegree_add_eq_left_of_natDegree_lt h] at H

Premises used: Polynomial.natDegree_add_eq_left_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : p.natDegree < p.natDegree
h_1 : ¬p.natDegree = q.natDegree
h : q.natDegree < p.natDegree
⊢ False

Tactic:
LT.lt.false H

Premises used: LT.lt.false
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : p.natDegree < p.natDegree
h_1 : ¬p.natDegree = q.natDegree
h : q.natDegree < p.natDegree
⊢ False

Tactic:
exact LT.lt.false H

Premises used: LT.lt.false
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < p.natDegree
h : ¬p.natDegree = q.natDegree
⊢ p.natDegree < q.natDegree ∨ q.natDegree < p.natDegree

Tactic:
cases Nat.lt_or_lt_of_ne h with
  | inl h => exact lt_asymm h (by rwa [natDegree_add_eq_right_of_natDegree_lt h] at H)
  | inr h =>
    rw [natDegree_add_eq_left_of_natDegree_lt h] at H
    exact LT.lt.false H

Premises used: Nat.lt_or_lt_of_ne, lt_asymm, LT.lt.false
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree < q.natDegree
⊢ p.natDegree = q.natDegree

Tactic:
(natDegree_eq_of_natDegree_add_lt_left q p (add_comm p q ▸ H)).symm

Premises used: Polynomial.natDegree_eq_of_natDegree_add_lt_left, Eq.rec, add_comm, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
pos : ∀ (h₁ : p.natDegree = 0), p.natDegree = q.natDegree
neg : ∀ (h₁ : ¬p.natDegree = 0), p.natDegree = q.natDegree
⊢ p.natDegree = q.natDegree

Tactic:
by_cases h₁ : natDegree p = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
pos : ∀ (h₂ : q.natDegree = 0), p.natDegree = q.natDegree
neg : ∀ (h₂ : ¬q.natDegree = 0), p.natDegree = q.natDegree
⊢ p.natDegree = q.natDegree

Tactic:
by_cases h₂ : natDegree q = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
pos : ∀ (h₂ : q.natDegree = 0), p.natDegree = q.natDegree
neg : ∀ (h₂ : ¬q.natDegree = 0), p.natDegree = q.natDegree
⊢ p.natDegree = q.natDegree

Tactic:
on_goal 1 => by_cases h₂ : natDegree q = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
h₁.trans h₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
exact h₁.trans h₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
neg : (p + q).natDegree < q.natDegree
⊢ p.natDegree = q.natDegree

Tactic:
apply natDegree_eq_of_natDegree_add_lt_right

Premises used: Polynomial.natDegree_eq_of_natDegree_add_lt_right
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
neg : 0 < q.natDegree
neg₁ neg₂ neg₃ neg₄ : q.natDegree ≠ 0
⊢ (p + q).natDegree < q.natDegree

Tactic:
rwa [H, Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
neg : (p + q).natDegree < p.natDegree
⊢ p.natDegree = q.natDegree

Tactic:
apply natDegree_eq_of_natDegree_add_lt_left

Premises used: Polynomial.natDegree_eq_of_natDegree_add_lt_left
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
neg : 0 < p.natDegree
neg₁ neg₂ neg₃ neg₄ : p.natDegree ≠ 0
⊢ (p + q).natDegree < p.natDegree

Tactic:
rwa [H, Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
⊢ Nontrivial R

Tactic:
nontriviality
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
h : Nontrivial R
⊢ p.leadingCoeff = 1

Tactic:
(congr_arg _ <| natDegree_eq_of_le_of_coeff_ne_zero pn ?_).trans p1

Premises used: Polynomial.leadingCoeff, congr_arg, Polynomial.natDegree_eq_of_le_of_coeff_ne_zero, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
h : Nontrivial R
refine : p.coeff n ≠ 0
⊢ p.leadingCoeff = 1

Tactic:
refine (congr_arg _ <| natDegree_eq_of_le_of_coeff_ne_zero pn ?_).trans p1

Premises used: congr_arg, Polynomial.natDegree_eq_of_le_of_coeff_ne_zero, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
h : Nontrivial R
⊢ p.coeff n ≠ 0

Tactic:
ne_of_eq_of_ne p1 one_ne_zero

Premises used: ne_of_eq_of_ne, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
h : Nontrivial R
⊢ p.coeff n ≠ 0

Tactic:
exact ne_of_eq_of_ne p1 one_ne_zero

Premises used: ne_of_eq_of_ne, one_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
pn : p.degree ≤ (↑n : WithBot ℕ)
p1 : p.coeff n = 1
⊢ p.Monic

Tactic:
monic_of_natDegree_le_of_coeff_eq_one n (natDegree_le_of_degree_le pn) p1

Premises used: Polynomial.monic_of_natDegree_le_of_coeff_eq_one, Polynomial.natDegree_le_of_degree_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree < q.degree
⊢ p.coeff q.natDegree = 0

Tactic:
have : coeff p (natDegree q) = 0 := coeff_natDegree_eq_zero_of_degree_lt h
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree < q.degree
this : p.coeff q.natDegree = 0
⊢ (p + q).leadingCoeff = q.leadingCoeff

Tactic:
simp only [leadingCoeff, natDegree_eq_of_degree_eq (degree_add_eq_right_of_degree_lt h), this,
    coeff_add, zero_add]

Premises used: Polynomial.degree_add_eq_right_of_degree_lt, Polynomial.leadingCoeff, Polynomial.coeff_add, zero_add, Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : q.degree < p.degree
rw : (q + p).leadingCoeff = p.leadingCoeff
⊢ (p + q).leadingCoeff = p.leadingCoeff

Tactic:
rw [add_comm]

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

Tactic:
leadingCoeff_add_of_degree_lt h

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

Tactic:
exact leadingCoeff_add_of_degree_lt h

Premises used: Polynomial.leadingCoeff_add_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
h₁ : (p + q).degree = p.degree
⊢ (p + q).natDegree = p.natDegree

Tactic:
apply natDegree_eq_of_degree_eq

Premises used: Polynomial.natDegree_eq_of_degree_eq
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
h₁ : max p.degree q.degree = p.degree
h₂ : max q.degree q.degree = q.degree
h₃ h₄ : q.degree = q.degree
⊢ (p + q).degree = p.degree

Tactic:
rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]

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

Tactic:
have : natDegree (p + q) = natDegree p := by
    apply natDegree_eq_of_degree_eq
    rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
this : (p + q).natDegree = p.natDegree
⊢ (p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff

Tactic:
simp only [leadingCoeff, this, natDegree_eq_of_degree_eq h, coeff_add]

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

Tactic:
Finset.sum_eq_single (natDegree p, natDegree q) ?_ ?_

Premises used: Prod.mk, Finset.sum_eq_single, WithBot.recBotCoe, Polynomial.natDegree, WithBot.unbotD
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
refine_1 :
  ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree),
    b ≠ (p.natDegree, q.natDegree) → p.coeff b.1 * q.coeff b.2 = 0
refine_2 :
  (p.natDegree, q.natDegree) ∉ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree) →
    p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree), p.coeff x.1 * q.coeff x.2 =
    p.coeff p.natDegree * q.coeff q.natDegree

Tactic:
refine Finset.sum_eq_single (natDegree p, natDegree q) ?_ ?_

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

Tactic:
rw [mem_antidiagonal] at h₁

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

Tactic:
rw [mem_antidiagonal] at h₁

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
pos : ∀ (H : p.natDegree < i), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
neg : ∀ (H : ¬p.natDegree < 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 H : natDegree p < i

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree < i
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_degree_lt
              (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 H)),
            zero_mul]

Premises used: Iff.mpr, lt_of_le_of_lt, MulZeroClass.zero_mul, Polynomial.degree_le_natDegree, WithBot.coe_lt_coe, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : ¬p.natDegree < i
⊢ p.natDegree = i ∨ i < p.natDegree

Tactic:
rw [not_lt_iff_eq_or_lt] at H

Premises used: not_lt_iff_eq_or_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i ∨ i < p.natDegree
neg : ∀ (H : p.natDegree = i), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
neg₁ : ∀ (H : i < p.natDegree), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rcases H with H | H
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
this : q.natDegree < j
rw : p.coeff (i, j).1 * 0 = 0
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                mul_zero]

Premises used: Iff.mpr, lt_of_le_of_lt, Polynomial.degree_le_natDegree, MulZeroClass.mul_zero, WithBot.coe_lt_coe, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
neg : q.natDegree < j
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
suffices natDegree q < j by
              rw [coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                mul_zero]
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
neg : ∀ (H' : j ≤ q.natDegree), False
⊢ q.natDegree < j

Tactic:
by_contra! H'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
H' : j ≤ q.natDegree
⊢ False

Tactic:
ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
                h₁

Premises used: ne_of_lt, Nat.lt_of_lt_of_le, Nat.add_le_add_left, Nat.add_lt_add_right
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
H' : j ≤ q.natDegree
⊢ False

Tactic:
exact
              ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
                h₁

Premises used: ne_of_lt, Nat.lt_of_lt_of_le, Nat.add_le_add_left, Nat.add_lt_add_right
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)
refine_2 : False
⊢ p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0

Tactic:
exfalso
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)
refine_2 : (p.natDegree, q.natDegree) ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)
⊢ False

Tactic:
apply H
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)
refine_2 refine_2₁ : (p.natDegree, q.natDegree).1 + (p.natDegree, q.natDegree).2 = p.natDegree + q.natDegree
⊢ (p.natDegree, q.natDegree) ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)

Tactic:
rw [mem_antidiagonal]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p ≠ 0

Tactic:
mt ?_ h

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

Tactic:
refine mt ?_ h

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

Tactic:
rw [hp, leadingCoeff_zero, zero_mul]

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

Tactic:
exact fun hp => by rw [hp, leadingCoeff_zero, zero_mul]
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
⊢ q ≠ 0

Tactic:
mt ?_ h

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

Tactic:
refine mt ?_ h

Premises used: mt