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

case h₁
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ¬(d, n) ∈ Finset.Nat.antidiagonal (d + n) → ↑(coeff R (d, n).fst) p * ↑(coeff R (d, n).snd) (X ^ n) = 0
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ↑(coeff R (d + n)) (p * X ^ n) = ↑(coeff R d) p
rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
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) ≠ (d, n)
⊢ ↑(coeff R (i, j).fst) p * ↑(coeff R (i, j).snd) (X ^ n) = 0
case h₀
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ∀ (b : ℕ × ℕ), b ∈ Finset.Nat.antidiagonal (d + n) → b ≠ (d, n) → ↑(coeff R b.fst) p * ↑(coeff R b.snd) (X ^ n) = 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) ≠ (d, n)
⊢ ¬(i, j).snd = 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) ≠ (d, n)
⊢ ↑(coeff R (i, j).fst) p * ↑(coeff R (i, j).snd) (X ^ n) = 0
rw [coeff_X_pow, if_neg, MulZeroClass.mul_zero]
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).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ 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) ≠ (d, n)
⊢ ¬(i, j).snd = 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).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ (i, j) = (d, (i, j).snd)
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).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ False
apply h2
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
d i j : ℕ
h1 : (i, j).fst = d
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ (i, j) = (d, (i, j).snd)
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).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ (i, j) = (d, (i, j).snd)
rw [Finset.Nat.mem_antidiagonal, 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).fst = d
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ (i, j) = (d, (i, j).snd)
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
no goals
case h₁
R : Type u_1
inst✝ : Semiring R
p : PowerSeries R
n d : ℕ
⊢ ¬(d, n) ∈ Finset.Nat.antidiagonal (d + n) → ↑(coeff R (d, n).fst) p * ↑(coeff R (d, n).snd) (X ^ n) = 0
exact fun h1 => (h1 (Finset.Nat.mem_antidiagonal.2 rfl)).elim