R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ∑ x in Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q), coeff p x.fst * coeff q x.snd =
    trailingCoeff p * trailingCoeff q
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ coeff (p * q) (natTrailingDegree p + natTrailingDegree q) = trailingCoeff p * trailingCoeff q
rw [coeff_mul]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ∀ (b : ℕ × ℕ),
    b ∈ Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q) →
      b ≠ (natTrailingDegree p, natTrailingDegree q) → coeff p b.fst * coeff q b.snd = 0
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ∑ x in Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q), coeff p x.fst * coeff q x.snd =
    trailingCoeff p * trailingCoeff q
refine'
  Finset.sum_eq_single (p.natTrailingDegree, q.natTrailingDegree) _ fun h =>
    (h (Nat.mem_antidiagonal.mpr rfl)).elim
case mk
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j) ∈ Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q)
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ∀ (b : ℕ × ℕ),
    b ∈ Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q) →
      b ≠ (natTrailingDegree p, natTrailingDegree q) → coeff p b.fst * coeff q b.snd = 0
rintro ⟨i, j⟩ h₁ h₂
case mk
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
case mk
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j) ∈ Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q)
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
rw [Nat.mem_antidiagonal] at h₁
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : i < natTrailingDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0

case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
case mk
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
by_cases hi : i < p.natTrailingDegree
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
hj : j < natTrailingDegree q
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0

case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
hj : ¬j < natTrailingDegree q
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
by_cases hj : j < q.natTrailingDegree
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : natTrailingDegree p ≤ i
hj : natTrailingDegree q ≤ j
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
hj : ¬j < natTrailingDegree q
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
rw [not_lt] at hi hj
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : natTrailingDegree p ≤ i
hj : natTrailingDegree q ≤ j
⊢ (natTrailingDegree p, natTrailingDegree q).fst = (i, j).fst ∧
    (natTrailingDegree p, natTrailingDegree q).snd = (i, j).snd
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : natTrailingDegree p ≤ i
hj : natTrailingDegree q ≤ j
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
refine' (h₂ (Prod.ext_iff.mpr _).symm).elim
no goals
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : natTrailingDegree p ≤ i
hj : natTrailingDegree q ≤ j
⊢ (natTrailingDegree p, natTrailingDegree q).fst = (i, j).fst ∧
    (natTrailingDegree p, natTrailingDegree q).snd = (i, j).snd
exact (add_eq_add_iff_eq_and_eq hi hj).mp h₁.symm
no goals
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : i < natTrailingDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
rw [coeff_eq_zero_of_lt_natTrailingDegree hi, zero_mul]
no goals
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
hj : j < natTrailingDegree q
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
rw [coeff_eq_zero_of_lt_natTrailingDegree hj, mul_zero]