awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (p * HPow.hPow (α := R[X]) X n).leadingCoeff = p.leadingCoeff

Tactic:
leadingCoeff_mul_monic (monic_X_pow n)

Premises used: Polynomial.monic_X_pow, Polynomial.leadingCoeff_mul_monic
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (p * X).leadingCoeff = p.leadingCoeff

Tactic:
leadingCoeff_mul_monic monic_X

Premises used: Polynomial.leadingCoeff_mul_monic, Polynomial.monic_X
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (HPow.hPow (β := ℕ) p 0).coeff (0 * p.natDegree) = HPow.hPow (β := ℕ) p.leadingCoeff 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
succ : (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
⊢ (p ^ (i + 1)).coeff ((i + 1) * p.natDegree) = p.leadingCoeff ^ (i + 1)

Tactic:
rw [pow_succ, pow_succ, Nat.succ_mul]

Premises used: pow_succ, Nat.succ_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
pos :
  ∀ (hp1 : p.leadingCoeff ^ i = 0),
    (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
neg :
  ∀ (hp1 : ¬p.leadingCoeff ^ i = 0),
    (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
by_cases hp1 : p.leadingCoeff ^ i = 0

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
pos : (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
rw [hp1, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
pos : ∀ (hp2 : p ^ i = 0), (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
neg : ∀ (hp2 : ¬p ^ i = 0), (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
by_cases hp2 : p ^ i = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : p ^ i = 0
pos : (0 * p).coeff (i * p.natDegree + p.natDegree) = 0
pos₁ : Eq.{u + 1} (α := R) (coeff 0 (i * p.natDegree + p.natDegree)) 0
pos₂ pos₃ : Eq.{u + 1} (α := R) 0 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
rw [hp2, zero_mul, coeff_zero]

Premises used: MulZeroClass.zero_mul, Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
neg : (p ^ i * p).natDegree < i * p.natDegree + p.natDegree
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i).natDegree < i * p.natDegree

Tactic:
lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_

Premises used: Polynomial.natDegree_pow_le, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
refine : ∀ (h : (p ^ i).natDegree = i * p.natDegree), p ^ i = 0
⊢ (p ^ i).natDegree < i * p.natDegree

Tactic:
refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_

Premises used: Polynomial.natDegree_pow_le, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ (p ^ i).coeff (p ^ i).natDegree = 0

Tactic:
rw [← h, hp1] at hi
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
hi₁ : (p ^ i).coeff (p ^ i).natDegree = 0
⊢ p.leadingCoeff ^ i = 0

Tactic:
rw [← h, hp1] at hi
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
hi₁ : (p ^ i).coeff (p ^ i).natDegree = 0
hp1₁ : p.leadingCoeff ^ i = 0
⊢ ¬p ^ i = 0

Tactic:
rw [← h, hp1] at hi
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
hi₁ : (p ^ i).coeff (p ^ i).natDegree = 0
hp1₁ : p.leadingCoeff ^ i = 0
hp2₁ : ¬p ^ i = 0
⊢ (p ^ i).natDegree = i * p.natDegree

Tactic:
rw [← h, hp1] at hi
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (p ^ i).natDegree = 0
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0

Tactic:
leadingCoeff_eq_zero.mp hi

Premises used: Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (p ^ i).natDegree = 0
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0

Tactic:
exact leadingCoeff_eq_zero.mp hi

Premises used: Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i).natDegree < i * p.natDegree

Tactic:
have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h1 : (p ^ i).natDegree < i * p.natDegree
⊢ (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree

Tactic:
natDegree_mul_le

Premises used: Polynomial.natDegree_mul_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h1 : (p ^ i).natDegree < i * p.natDegree
⊢ (p ^ i).natDegree + p.natDegree < i * p.natDegree + p.natDegree

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h1 : (p ^ i).natDegree < i * p.natDegree
i₁ : (p ^ i).natDegree + p.natDegree < i * p.natDegree + p.natDegree
⊢ (p ^ i * p).natDegree < i * p.natDegree + p.natDegree

Tactic:
calc
          (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
          _ < i * p.natDegree + p.natDegree := by gcongr

Premises used: HMul.hMul, HPow.hPow, Polynomial.natDegree_mul_le, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
neg : (p ^ i * p).coeff ((p ^ i).natDegree + p.natDegree) = (p ^ i).leadingCoeff * p.leadingCoeff
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]

Premises used: Polynomial.leadingCoeff_pow', Polynomial.natDegree_pow'
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff ((p ^ i).natDegree + p.natDegree) = (p ^ i).leadingCoeff * p.leadingCoeff

Tactic:
coeff_mul_degree_add_degree _ _

Premises used: Polynomial.coeff_mul_degree_add_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff ((p ^ i).natDegree + p.natDegree) = (p ^ i).leadingCoeff * p.leadingCoeff

Tactic:
exact coeff_mul_degree_add_degree _ _

Premises used: Polynomial.coeff_mul_degree_add_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).coeff (0 * p.natDegree) = HPow.hPow (β := ℕ) p.leadingCoeff 0
succ :
  ∀ (i : ℕ) (hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i),
    (p ^ (i + 1)).coeff ((i + 1) * p.natDegree) = p.leadingCoeff ^ (i + 1)
⊢ (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n

Tactic:
induction n with
  | zero => simp
  | succ i hi =>
    rw [pow_succ, pow_succ, Nat.succ_mul]
    by_cases hp1 : p.leadingCoeff ^ i = 0
    · rw [hp1, zero_mul]
      by_cases hp2 : p ^ i = 0
      · rw [hp2, zero_mul, coeff_zero]
      · apply coeff_eq_zero_of_natDegree_lt
        have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi
        calc
          (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
          _ < i * p.natDegree + p.natDegree := by gcongr
    · rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]
      exact coeff_mul_degree_add_degree _ _

Premises used: pow_succ, MulZeroClass.zero_mul, Polynomial.leadingCoeff, Nat.succ_mul, Polynomial.coeff_eq_zero_of_natDegree_lt, Polynomial.coeff_zero, Polynomial.natDegree_mul_le, Polynomial.natDegree, Polynomial.coeff_mul_degree_add_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
h : (df, dg) ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
h₀ : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg), b ≠ (df, dg) → f.coeff b.1 * g.coeff b.2 = 0
⊢ (f * g).coeff (df + dg) = f.coeff df * g.coeff dg

Tactic:
rw [coeff_mul, Finset.sum_eq_single_of_mem (df, dg)]

Premises used: Finset.sum_eq_single_of_mem, Polynomial.coeff_mul, Prod.mk
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
h h₁ : (df, dg).1 + (df, dg).2 = df + dg
⊢ (df, dg) ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)

Tactic:
rw [mem_antidiagonal]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
h₀ : ∀ (h : df < df'), f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
h₁ : ∀ (hdf' : df' ≤ df), f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

Tactic:
obtain h | hdf' := lt_or_ge df df'

Premises used: lt_or_ge
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
h : df < df'
h₀ : 0 * g.coeff (df', dg').2 = 0
h₁ h₂ : Eq.{u + 1} (α := R) 0 0
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt (hdf.trans_lt h), zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.coeff_eq_zero_of_natDegree_lt, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
h₀ : ∀ (h : dg < dg'), f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
h₁ : ∀ (hdg' : dg' ≤ dg), f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

Tactic:
obtain h | hdg' := lt_or_ge dg dg'

Premises used: lt_or_ge
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
h : dg < dg'
h₀ : f.coeff (df', dg').1 * 0 = 0
h₁ h₂ : Eq.{u + 1} (α := R) 0 0
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt (hdg.trans_lt h), mul_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.coeff_eq_zero_of_natDegree_lt, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
⊢ f.natDegree ≤ df'

Tactic:
obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)

Premises used: add_eq_add_iff_eq_and_eq, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
hdf₁ : f.natDegree ≤ df'
⊢ df' ≤ df'

Tactic:
obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)

Premises used: add_eq_add_iff_eq_and_eq, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
hdf₁ : f.natDegree ≤ df'
hdf'₁ : df' ≤ df'
⊢ g.natDegree ≤ dg'

Tactic:
obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)

Premises used: add_eq_add_iff_eq_and_eq, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
hdf₁ : f.natDegree ≤ df'
hdf'₁ : df' ≤ df'
hdg₁ : g.natDegree ≤ dg'
⊢ dg' ≤ dg'

Tactic:
obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)

Premises used: add_eq_add_iff_eq_and_eq, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
hdf₁ : f.natDegree ≤ df'
hdf'₁ : df' ≤ df'
hdg₁ : g.natDegree ≤ dg'
hdg'₁ : dg' ≤ dg'
⊢ (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df' + dg')

Tactic:
obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)

Premises used: add_eq_add_iff_eq_and_eq, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
hdf₁ : f.natDegree ≤ df'
hdf'₁ : df' ≤ df'
hdg₁ : g.natDegree ≤ dg'
hdg'₁ : dg' ≤ dg'
hmem₁ : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df' + dg')
⊢ (df', dg') ≠ (df', dg')

Tactic:
obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)

Premises used: add_eq_add_iff_eq_and_eq, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
f g : R[X]
df' dg' : ℕ
hdf : f.natDegree ≤ df'
hdf' : df' ≤ df'
hdg : g.natDegree ≤ dg'
hdg' : dg' ≤ dg'
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df' + dg')
hne : (df', dg') ≠ (df', dg')
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

Tactic:
(hne rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
f g : R[X]
df' dg' : ℕ
hdf : f.natDegree ≤ df'
hdf' : df' ≤ df'
hdg : g.natDegree ≤ dg'
hdg' : dg' ≤ dg'
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df' + dg')
hne : (df', dg') ≠ (df', dg')
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

Tactic:
exact (hne rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
S : Type u_2
inst_1 : SMulZeroClass S R
a : S
p : R[X]
⊢ (a • p).degree ≤ p.degree

Tactic:
(degree_le_iff_coeff_zero _ _).2 fun m hm => ?_

Premises used: Iff.mpr, Polynomial.degree_le_iff_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
S : Type u_2
inst_1 : SMulZeroClass S R
a : S
p : R[X]
refine : ∀ (m : ℕ) (hm : p.degree < (↑m : WithBot ℕ)), (a • p).coeff m = 0
⊢ (a • p).degree ≤ p.degree

Tactic:
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_

Premises used: Iff.mpr, Polynomial.degree_le_iff_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
S : Type u_2
inst_1 : SMulZeroClass S R
a : S
p : R[X]
m : ℕ
hm : p.degree < (↑m : WithBot ℕ)
⊢ ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0

Tactic:
rw [degree_lt_iff_coeff_zero] at hm

Premises used: Polynomial.degree_lt_iff_coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
S : Type u_2
inst_1 : SMulZeroClass S R
a : S
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (a • p).coeff m = 0

Tactic:
simp [hm m le_rfl]

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
S : Type u_2
inst_1 : SMulZeroClass S R
a : S
p : R[X]
⊢ (a • p).natDegree ≤ p.natDegree

Tactic:
natDegree_le_natDegree (degree_smul_le a p)

Premises used: Polynomial.natDegree_le_natDegree, Polynomial.degree_smul_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ (a • p).degree = p.degree

Tactic:
le_antisymm (degree_smul_le a p) <| degree_le_degree ?_

Premises used: Polynomial.degree_le_degree, le_antisymm, Polynomial.degree_smul_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
refine : (a • p).coeff p.natDegree ≠ 0
⊢ (a • p).degree = p.degree

Tactic:
refine le_antisymm (degree_smul_le a p) <| degree_le_degree ?_

Premises used: Polynomial.degree_le_degree, le_antisymm, Polynomial.degree_smul_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
rw : ¬a * p.leadingCoeff = 0
⊢ (a • p).coeff p.natDegree ≠ 0

Tactic:
rw [coeff_smul, coeff_natDegree, smul_eq_mul, ne_eq]

Premises used: Polynomial.coeff_natDegree, ne_eq, Polynomial.coeff_smul, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ ¬a * p.leadingCoeff = 0

Tactic:
hp.mul_right_eq_zero_iff.ne.mpr ha

Premises used: Iff.mpr, IsRightRegular.mul_right_eq_zero_iff, Iff.ne
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ ¬a * p.leadingCoeff = 0

Tactic:
exact hp.mul_right_eq_zero_iff.ne.mpr ha

Premises used: Iff.mpr, IsRightRegular.mul_right_eq_zero_iff, Iff.ne
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ Nontrivial R

Tactic:
haveI := Nontrivial.of_polynomial_ne hp
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
this : Nontrivial R
⊢ p.leadingCoeff * leadingCoeff X ≠ 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
this : Nontrivial R
⊢ p.leadingCoeff * leadingCoeff X ≠ 0

Tactic:
have : leadingCoeff p * leadingCoeff X ≠ 0 := by simpa
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
this_1 : Nontrivial R
this : p.leadingCoeff * leadingCoeff X ≠ 0
rw : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(p.natDegree + 1) : WithBot ℕ)
⊢ p.degree < (p * X).degree

Tactic:
rw [degree_mul' this, degree_eq_natDegree hp, degree_X, ← Nat.cast_one, ← Nat.cast_add]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.degree_mul', Nat.cast_add, Polynomial.degree_X, Nat.cast_one
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
this_1 : Nontrivial R
this : p.leadingCoeff * leadingCoeff X ≠ 0
norm_cast : p.natDegree < p.natDegree + 1
⊢ LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(p.natDegree + 1) : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
this_1 : Nontrivial R
this : p.leadingCoeff * leadingCoeff X ≠ 0
⊢ p.natDegree < p.natDegree + 1

Tactic:
Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
this_1 : Nontrivial R
this : p.leadingCoeff * leadingCoeff X ≠ 0
⊢ p.natDegree < p.natDegree + 1

Tactic:
exact Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.natDegree ≤ 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
eq_C_of_degree_le_zero <| degree_le_of_natDegree_le h

Premises used: Polynomial.degree_le_of_natDegree_le, Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.natDegree = 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
eq_C_of_natDegree_le_zero h.le

Premises used: Polynomial.eq_C_of_natDegree_le_zero, Eq.le
-- Module: Mathlib.Algebra.Polynomial.Degree.Operations
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (∃ (x : R), (C : (a : R) → R[X]) x = p) → p.natDegree = 0

Tactic:
aesop