R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : n ∈ support (p * q)
⊢ trailingDegree p + trailingDegree q ≤ ↑n
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ trailingDegree p + trailingDegree q ≤ trailingDegree (p * q)
refine' Finset.le_min fun n hn => _
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
⊢ trailingDegree p + trailingDegree q ≤ ↑n
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : n ∈ support (p * q)
⊢ trailingDegree p + trailingDegree q ≤ ↑n
rw [mem_support_iff, coeff_mul] at hn
case intro.mk.intro
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
i j : ℕ
hij : (i, j) ∈ Nat.antidiagonal n
hpq : coeff p (i, j).fst * coeff q (i, j).snd ≠ 0
⊢ trailingDegree p + trailingDegree q ≤ ↑n
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
⊢ trailingDegree p + trailingDegree q ≤ ↑n
obtain ⟨⟨i, j⟩, hij, hpq⟩ := exists_ne_zero_of_sum_ne_zero hn
case intro.mk.intro
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
i j : ℕ
hij : (i, j) ∈ Nat.antidiagonal n
hpq : coeff p (i, j).fst * coeff q (i, j).snd ≠ 0
⊢ ↑(i, j).fst + ↑(i, j).snd = ↑n
case intro.mk.intro
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
i j : ℕ
hij : (i, j) ∈ Nat.antidiagonal n
hpq : coeff p (i, j).fst * coeff q (i, j).snd ≠ 0
⊢ trailingDegree p + trailingDegree q ≤ ↑n
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
    (le_of_eq _)
no goals
case intro.mk.intro
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
i j : ℕ
hij : (i, j) ∈ Nat.antidiagonal n
hpq : coeff p (i, j).fst * coeff q (i, j).snd ≠ 0
⊢ ↑(i, j).fst + ↑(i, j).snd = ↑n
rwa [← WithTop.coe_add, WithTop.coe_eq_coe, ← Nat.mem_antidiagonal]