case h₀
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ∀ (b : ℕ × ℕ), b ∈ Finset.Nat.antidiagonal (d + n) → b ≠ (n, d) → ↑(coeff R b.fst) (X ^ n) * ↑(coeff R b.snd) p = 0

case h₁
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ¬(n, d) ∈ Finset.Nat.antidiagonal (d + n) → ↑(coeff R (n, d).fst) (X ^ n) * ↑(coeff R (n, d).snd) p = 0
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ↑(coeff R (d + n)) (X ^ n * p) = ↑(coeff R d) p
rw [coeff_mul, Finset.sum_eq_single (n, d), coeff_X_pow, if_pos rfl, one_mul]
case h₀.mk
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d i j : ℕ
h1 : (i, j) ∈ Finset.Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ ↑(coeff R (i, j).fst) (X ^ n) * ↑(coeff R (i, j).snd) p = 0
case h₀
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ∀ (b : ℕ × ℕ), b ∈ Finset.Nat.antidiagonal (d + n) → b ≠ (n, d) → ↑(coeff R b.fst) (X ^ n) * ↑(coeff R b.snd) p = 0
rintro ⟨i, j⟩ h1 h2
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d i j : ℕ
h1 : (i, j) ∈ Finset.Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ ¬(i, j).fst = n
case h₀.mk
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d i j : ℕ
h1 : (i, j) ∈ Finset.Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ ↑(coeff R (i, j).fst) (X ^ n) * ↑(coeff R (i, j).snd) p = 0
rw [coeff_X_pow, if_neg, MulZeroClass.zero_mul]
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
d i j : ℕ
h1 : (i, j) ∈ Finset.Nat.antidiagonal (d + (i, j).fst)
h2 : (i, j) ≠ ((i, j).fst, d)
⊢ False
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d i j : ℕ
h1 : (i, j) ∈ Finset.Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ ¬(i, j).fst = n
rintro rfl
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
d i j : ℕ
h1 : (i, j) ∈ Finset.Nat.antidiagonal (d + (i, j).fst)
h2 : (i, j) ≠ ((i, j).fst, d)
⊢ (i, j) = ((i, j).fst, d)
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
d i j : ℕ
h1 : (i, j) ∈ Finset.Nat.antidiagonal (d + (i, j).fst)
h2 : (i, j) ≠ ((i, j).fst, d)
⊢ False
apply h2
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
d i j : ℕ
h1 : (i, j).snd = d
h2 : (i, j) ≠ ((i, j).fst, d)
⊢ (i, j) = ((i, j).fst, d)
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
d i j : ℕ
h1 : (i, j) ∈ Finset.Nat.antidiagonal (d + (i, j).fst)
h2 : (i, j) ≠ ((i, j).fst, d)
⊢ (i, j) = ((i, j).fst, d)
rw [Finset.Nat.mem_antidiagonal, add_comm, add_right_cancel_iff] at h1
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
i j : ℕ
h2 : (i, j) ≠ ((i, j).fst, (i, j).snd)
⊢ (i, j) = ((i, j).fst, (i, j).snd)
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
d i j : ℕ
h1 : (i, j).snd = d
h2 : (i, j) ≠ ((i, j).fst, d)
⊢ (i, j) = ((i, j).fst, d)
subst h1
no goals
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
i j : ℕ
h2 : (i, j) ≠ ((i, j).fst, (i, j).snd)
⊢ (i, j) = ((i, j).fst, (i, j).snd)
rfl
case h₁
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ¬(n, d) ∈ Finset.Nat.antidiagonal (n + d) → ↑(coeff R (n, d).fst) (X ^ n) * ↑(coeff R (n, d).snd) p = 0
case h₁
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ¬(n, d) ∈ Finset.Nat.antidiagonal (d + n) → ↑(coeff R (n, d).fst) (X ^ n) * ↑(coeff R (n, d).snd) p = 0
rw [add_comm]
no goals
case h₁
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ¬(n, d) ∈ Finset.Nat.antidiagonal (n + d) → ↑(coeff R (n, d).fst) (X ^ n) * ↑(coeff R (n, d).snd) p = 0
exact fun h1 => (h1 (Finset.Nat.mem_antidiagonal.2 rfl)).elim