case inl
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : n ≤ d
⊢ ↑(coeff R d) (p * X ^ n) = ↑(coeff R (d - n)) p

case inr
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : ¬n ≤ d
⊢ ↑(coeff R d) (p * X ^ n) = 0
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ↑(coeff R d) (p * X ^ n) = if n ≤ d then ↑(coeff R (d - n)) p else 0
split_ifs with h
no goals
case inl
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : n ≤ d
⊢ ↑(coeff R d) (p * X ^ n) = ↑(coeff R (d - n)) p
rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
case inr
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Finset.Nat.antidiagonal d
⊢ ↑(coeff R x.fst) p * ↑(coeff R x.snd) (X ^ n) = 0
case inr
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : ¬n ≤ d
⊢ ↑(coeff R d) (p * X ^ n) = 0
refine' (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => _)
case inr.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Finset.Nat.antidiagonal d
⊢ ¬x.snd = n
case inr
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Finset.Nat.antidiagonal d
⊢ ↑(coeff R x.fst) p * ↑(coeff R x.snd) (X ^ n) = 0
rw [coeff_X_pow, if_neg, MulZeroClass.mul_zero]
no goals
case inr.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Finset.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