case inl
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : n ≤ d
⊢ ↑(coeff R d) (X ^ n * p) = ↑(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) (X ^ n * p) = 0
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ↑(coeff R d) (X ^ n * p) = if n ≤ d then ↑(coeff R (d - n)) p else 0
split_ifs with h
case inl
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : n ≤ d
⊢ ↑(coeff R (d - n)) p = ↑(coeff R (d - n + n - n)) p
case inl
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : n ≤ d
⊢ ↑(coeff R d) (X ^ n * p) = ↑(coeff R (d - n)) p
rw [← tsub_add_cancel_of_le h, coeff_X_pow_mul]
no goals
case inl
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : n ≤ d
⊢ ↑(coeff R (d - n)) p = ↑(coeff R (d - n + n - n)) p
simp
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) (X ^ n) * ↑(coeff R x.snd) p = 0
case inr
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
h : ¬n ≤ d
⊢ ↑(coeff R d) (X ^ n * p) = 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.fst = 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) (X ^ n) * ↑(coeff R x.snd) p = 0
rw [coeff_X_pow, if_neg, MulZeroClass.zero_mul]
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
this : x.fst + x.snd = d
⊢ ¬x.fst = n
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.fst = n
have := Finset.Nat.mem_antidiagonal.mp 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
this : x.snd + x.fst = d
⊢ ¬x.fst = n
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
this : x.fst + x.snd = d
⊢ ¬x.fst = n
rw [add_comm] at this
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
this : x.snd + x.fst = d
⊢ ¬x.fst = n
exact ((le_of_add_le_right this.le).trans_lt <| not_le.mp h).ne