case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ ∀ (b : ℕ × ℕ), b ∈ Nat.antidiagonal (d + n) → b ≠ (d, n) → coeff p b.fst * coeff (X ^ n) b.snd = 0

case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ ¬(d, n) ∈ Nat.antidiagonal (d + n) → coeff p (d, n).fst * coeff (X ^ n) (d, n).snd = 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 + n) = coeff p d
rw [coeff_mul, sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
case h₀.mk
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ coeff p (i, j).fst * coeff (X ^ n) (i, j).snd = 0
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ ∀ (b : ℕ × ℕ), b ∈ Nat.antidiagonal (d + n) → b ≠ (d, n) → coeff p b.fst * coeff (X ^ n) b.snd = 0
rintro ⟨i, j⟩ h1 h2
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).snd = n
case h₀.mk
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ coeff p (i, j).fst * coeff (X ^ n) (i, j).snd = 0
rw [coeff_X_pow, if_neg, mul_zero]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + (i, j).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ False
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).snd = n
rintro rfl
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
d i j : ℕ
h1 : (i, j) ∈ 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
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + (i, j).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ False
apply h2
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
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
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + (i, j).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ (i, j) = (d, (i, j).snd)
rw [Nat.mem_antidiagonal, add_right_cancel_iff] at h1
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
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
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
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
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
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
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ ¬(d, n) ∈ Nat.antidiagonal (d + n) → coeff p (d, n).fst * coeff (X ^ n) (d, n).snd = 0
exact fun h1 => (h1 (Nat.mem_antidiagonal.2 rfl)).elim