case inl.inl
R : Type u
S : Type v
ι : Type w
a b : R
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ natDegree p
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (natDegree p + natDegree q) = coeff p (natDegree p) * coeff q (natDegree q)

case inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
n : ℕ
inst✝ : Semiring R
p q r : R[X]
qn : natDegree q ≤ n
pm : natDegree p ≤ natDegree p
hn : natDegree q < n
⊢ coeff (p * q) (natDegree p + n) = coeff p (natDegree p) * coeff q n

case inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
hm : natDegree p < m
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (m + natDegree q) = coeff p m * coeff q (natDegree q)

case inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
hm : natDegree p < m
hn : natDegree q < n
⊢ coeff (p * q) (m + n) = coeff p m * coeff q n
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
⊢ coeff (p * q) (m + n) = coeff p m * coeff q n
rcases eq_or_lt_of_le pm with (rfl | hm) <;> rcases eq_or_lt_of_le qn with (rfl | hn)
no goals
case inl.inl
R : Type u
S : Type v
ι : Type w
a b : R
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ natDegree p
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (natDegree p + natDegree q) = coeff p (natDegree p) * coeff q (natDegree q)
exact natDegree_add_coeff_mul _ _
case inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
n : ℕ
inst✝ : Semiring R
p q r : R[X]
qn : natDegree q ≤ n
pm : natDegree p ≤ natDegree p
hn : natDegree q < n
⊢ coeff (p * q) (natDegree p + n) = 0
case inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
n : ℕ
inst✝ : Semiring R
p q r : R[X]
qn : natDegree q ≤ n
pm : natDegree p ≤ natDegree p
hn : natDegree q < n
⊢ coeff (p * q) (natDegree p + n) = coeff p (natDegree p) * coeff q n
rw [coeff_eq_zero_of_natDegree_lt hn, mul_zero]
no goals
case inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
n : ℕ
inst✝ : Semiring R
p q r : R[X]
qn : natDegree q ≤ n
pm : natDegree p ≤ natDegree p
hn : natDegree q < n
⊢ coeff (p * q) (natDegree p + n) = 0
exact natDegree_lt_coeff_mul (add_lt_add_left hn _)
case inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
hm : natDegree p < m
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (m + natDegree q) = 0
case inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
hm : natDegree p < m
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (m + natDegree q) = coeff p m * coeff q (natDegree q)
rw [coeff_eq_zero_of_natDegree_lt hm, zero_mul]
no goals
case inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
hm : natDegree p < m
qn : natDegree q ≤ natDegree q
⊢ coeff (p * q) (m + natDegree q) = 0
exact natDegree_lt_coeff_mul (add_lt_add_right hm _)
case inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
hm : natDegree p < m
hn : natDegree q < n
⊢ coeff (p * q) (m + n) = 0
case inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
hm : natDegree p < m
hn : natDegree q < n
⊢ coeff (p * q) (m + n) = coeff p m * coeff q n
rw [coeff_eq_zero_of_natDegree_lt hn, mul_zero]
no goals
case inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
pm : natDegree p ≤ m
qn : natDegree q ≤ n
hm : natDegree p < m
hn : natDegree q < n
⊢ coeff (p * q) (m + n) = 0
exact natDegree_lt_coeff_mul (add_lt_add hm hn)