R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.567630
p q : R[X]
⊢ degree (∑ x in support p, sum q fun j a => ↑(monomial (x + j)) (coeff p x * a)) ≤
    sup (support p) fun i => degree (sum q fun j a => ↑(monomial (i + j)) (coeff p i * a))
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.567630
p q : R[X]
⊢ degree (p * q) ≤ sup (support p) fun i => degree (sum q fun j a => ↑C (coeff p i * a) * X ^ (i + j))
simp only [← C_mul_X_pow_eq_monomial.symm, mul_eq_sum_sum (p := p) (q := q)]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.567630
p q : R[X]
⊢ degree (∑ x in support p, sum q fun j a => ↑(monomial (x + j)) (coeff p x * a)) ≤
    sup (support p) fun i => degree (sum q fun j a => ↑(monomial (i + j)) (coeff p i * a))
exact degree_sum_le _ _
R : Type u
S : Type v
a✝ b✝ c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.567630
p q : R[X]
a : ℕ
ha : a ∈ support p
b : ℕ
hb : b ∈ support q
⊢ ↑(a + b) ≤ degree p + degree q
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.567630
p q : R[X]
⊢ (sup (support p) fun i => sup (support q) fun j => degree (↑C (coeff p i * coeff q j) * X ^ (i + j))) ≤
    degree p + degree q
refine'
  Finset.sup_le fun a ha => Finset.sup_le fun b hb => le_trans (degree_C_mul_X_pow_le _ _) _
R : Type u
S : Type v
a✝ b✝ c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.567630
p q : R[X]
a : ℕ
ha : a ∈ support p
b : ℕ
hb : b ∈ support q
⊢ ↑a + ↑b ≤ degree p + degree q
R : Type u
S : Type v
a✝ b✝ c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.567630
p q : R[X]
a : ℕ
ha : a ∈ support p
b : ℕ
hb : b ∈ support q
⊢ ↑(a + b) ≤ degree p + degree q
rw [Nat.cast_withBot, WithBot.coe_add]
R : Type u
S : Type v
a✝ b✝ c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.567630
p q : R[X]
a : ℕ
ha : coeff p a ≠ 0
b : ℕ
hb : coeff q b ≠ 0
⊢ ↑a + ↑b ≤ degree p + degree q
R : Type u
S : Type v
a✝ b✝ c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.567630
p q : R[X]
a : ℕ
ha : a ∈ support p
b : ℕ
hb : b ∈ support q
⊢ ↑a + ↑b ≤ degree p + degree q
rw [mem_support_iff] at ha hb
no goals
R : Type u
S : Type v
a✝ b✝ c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.567630
p q : R[X]
a : ℕ
ha : coeff p a ≠ 0
b : ℕ
hb : coeff q b ≠ 0
⊢ ↑a + ↑b ≤ degree p + degree q
exact add_le_add (le_degree_of_ne_zero ha) (le_degree_of_ne_zero hb)