case inl
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : n ≤ d
⊢ coeff (p * X ^ n) d = coeff p (d - n)

case inr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ coeff (p * X ^ n) d = 0
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ coeff (p * X ^ n) d = if n ≤ d then coeff p (d - n) else 0
split_ifs with h
no goals
case inl
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : n ≤ d
⊢ coeff (p * X ^ n) d = coeff p (d - n)
rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
case inr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Nat.antidiagonal d
⊢ coeff p x.fst * coeff (X ^ n) x.snd = 0
case inr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ coeff (p * X ^ n) d = 0
refine' (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => _)
case inr.hnc
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Nat.antidiagonal d
⊢ ¬x.snd = n
case inr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Nat.antidiagonal d
⊢ coeff p x.fst * coeff (X ^ n) x.snd = 0
rw [coeff_X_pow, if_neg, mul_zero]
no goals
case inr.hnc
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Nat.antidiagonal d
⊢ ¬x.snd = n
exact ((le_of_add_le_right (Finset.Nat.mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne