case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q

case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
by_cases hp : p = 0
case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q

case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
by_cases hq : q = 0
no goals
case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
rw [hp, MulZeroClass.zero_mul, trailingDegree_zero, top_add]
no goals
case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
rw [hq, MulZeroClass.mul_zero, trailingDegree_zero, add_top]
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(natTrailingDegree p + natTrailingDegree q) = ↑(natTrailingDegree p) + ↑(natTrailingDegree q)
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq,
trailingDegree_eq_natTrailingDegree (mul_ne_zero hp hq), natTrailingDegree_mul hp hq]
no goals
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(natTrailingDegree p + natTrailingDegree q) = ↑(natTrailingDegree p) + ↑(natTrailingDegree q)
apply WithTop.coe_add