case refine'_1
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
⊢ ∀ (b : ℕ × ℕ),
    b ∈ Nat.antidiagonal (natDegree p + natDegree q) →
      b ≠ (natDegree p, natDegree q) → coeff p b.fst * coeff q b.snd = 0

case refine'_2
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
⊢ ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q) →
    coeff p (natDegree p, natDegree q).fst * coeff q (natDegree p, natDegree q).snd = 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
⊢ ∑ x in Nat.antidiagonal (natDegree p + natDegree q), coeff p x.fst * coeff q x.snd =
    coeff p (natDegree p) * coeff q (natDegree q)
refine' Finset.sum_eq_single (natDegree p, natDegree q) _ _
case refine'_1.mk
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ Nat.antidiagonal (natDegree p + natDegree q)
h₂ : (i, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
case refine'_1
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
⊢ ∀ (b : ℕ × ℕ),
    b ∈ Nat.antidiagonal (natDegree p + natDegree q) →
      b ≠ (natDegree p, natDegree q) → coeff p b.fst * coeff q b.snd = 0
rintro ⟨i, j⟩ h₁ h₂
case refine'_1.mk
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
case refine'_1.mk
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ Nat.antidiagonal (natDegree p + natDegree q)
h₂ : (i, j) ≠ (natDegree p, natDegree 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 c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : natDegree p < i
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0

case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : ¬natDegree p < i
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
case refine'_1.mk
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
by_cases H : natDegree p < i
no goals
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : natDegree p < i
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
rw [coeff_eq_zero_of_degree_lt
    (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 H)),
  zero_mul]
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : natDegree p = i ∨ i < natDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : ¬natDegree p < i
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
rw [not_lt_iff_eq_or_lt] at H
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : natDegree p = i
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0

case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : natDegree p = i ∨ i < natDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
cases' H with H H
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
j : ℕ
h₁ : (natDegree p, j).fst + (natDegree p, j).snd = natDegree p + natDegree q
h₂ : (natDegree p, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, j).fst * coeff q (natDegree p, j).snd = 0
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : natDegree p = i
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
subst H
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
j : ℕ
h₁ : (natDegree p, j).snd = natDegree q
h₂ : (natDegree p, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, j).fst * coeff q (natDegree p, j).snd = 0
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
j : ℕ
h₁ : (natDegree p, j).fst + (natDegree p, j).snd = natDegree p + natDegree q
h₂ : (natDegree p, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, j).fst * coeff q (natDegree p, j).snd = 0
rw [add_left_cancel_iff] at h₁
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
j : ℕ
h₁ : j = natDegree q
h₂ : (natDegree p, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, j).fst * coeff q (natDegree p, j).snd = 0
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
j : ℕ
h₁ : (natDegree p, j).snd = natDegree q
h₂ : (natDegree p, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, j).fst * coeff q (natDegree p, j).snd = 0
dsimp at h₁
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
h₂ : (natDegree p, natDegree q) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, natDegree q).fst * coeff q (natDegree p, natDegree q).snd = 0
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
j : ℕ
h₁ : j = natDegree q
h₂ : (natDegree p, j) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, j).fst * coeff q (natDegree p, j).snd = 0
subst h₁
case neg.inl.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
h₂ : (natDegree p, natDegree q) ≠ (natDegree p, natDegree q)
⊢ False
case neg.inl
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
h₂ : (natDegree p, natDegree q) ≠ (natDegree p, natDegree q)
⊢ coeff p (natDegree p, natDegree q).fst * coeff q (natDegree p, natDegree q).snd = 0
exfalso
no goals
case neg.inl.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
h₂ : (natDegree p, natDegree q) ≠ (natDegree p, natDegree q)
⊢ False
exact h₂ rfl
case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
⊢ natDegree q < j
case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
suffices natDegree q < j by
  rw [coeff_eq_zero_of_degree_lt
      (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
    mul_zero]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
this : natDegree q < j
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
rw [coeff_eq_zero_of_degree_lt
    (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
  mul_zero]
case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
H' : ¬natDegree q < j
⊢ False
case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
⊢ natDegree q < j
by_contra H'
case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
H' : j ≤ natDegree q
⊢ False
case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
H' : ¬natDegree q < j
⊢ False
rw [not_lt] at H'
no goals
case neg.inr
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natDegree p + natDegree q
h₂ : (i, j) ≠ (natDegree p, natDegree q)
H : i < natDegree p
H' : j ≤ natDegree q
⊢ False
exact
  ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
    h₁
case refine'_2
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
H : ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
⊢ coeff p (natDegree p, natDegree q).fst * coeff q (natDegree p, natDegree q).snd = 0
case refine'_2
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
⊢ ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q) →
    coeff p (natDegree p, natDegree q).fst * coeff q (natDegree p, natDegree q).snd = 0
intro H
case refine'_2.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
H : ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
⊢ False
case refine'_2
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
H : ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
⊢ coeff p (natDegree p, natDegree q).fst * coeff q (natDegree p, natDegree q).snd = 0
exfalso
case refine'_2.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
H : ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
⊢ (natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
case refine'_2.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
H : ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
⊢ False
apply H
no goals
case refine'_2.h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.653636
p q : R[X]
H : ¬(natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
⊢ (natDegree p, natDegree q) ∈ Nat.antidiagonal (natDegree p + natDegree q)
rw [Nat.mem_antidiagonal]