-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem coeff_mul_degree_add_degree (p q : R[X]) :
    coeff (p * q) (natDegree p + natDegree q) = leadingCoeff p * leadingCoeff q :=
  calc
    coeff (p * q) (natDegree p + natDegree q) =
        ∑ x ∈ antidiagonal (natDegree p + natDegree q), coeff p x.1 * coeff q x.2 :=
      coeff_mul _ _ _
    _ = coeff p (natDegree p) * coeff q (natDegree q)

Proof state:
case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree)
⊢ (p.natDegree, q.natDegree) ∈ antidiagonal (p.natDegree + q.natDegree)

Tactic:
rw [mem_antidiagonal]

Result:
no goals

Proof state:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
h₂ : (p.natDegree, q.natDegree) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0

Tactic:
exact (h₂ rfl).elim

Result:
no goals

Proof state:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
j : ℕ
h₁ : (p.natDegree, j).1 + (p.natDegree, j).2 = p.natDegree + q.natDegree
h₂ : (p.natDegree, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (p.natDegree, j).1 * q.coeff (p.natDegree, j).2 = 0

Tactic:
rw [add_left_cancel_iff] at h₁

Result:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
j : ℕ
h₁ : (p.natDegree, j).2 = q.natDegree
h₂ : (p.natDegree, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (p.natDegree, j).1 * q.coeff (p.natDegree, j).2 = 0

Proof state:
case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree) →
    p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0

Tactic:
intro H

Result:
case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree)
⊢ p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i ∨ i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rcases H with H | H

Result:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Proof state:
case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree)
⊢ False

Tactic:
apply H

Result:
case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree)
⊢ (p.natDegree, q.natDegree) ∈ antidiagonal (p.natDegree + q.natDegree)

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : ¬p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [not_lt_iff_eq_or_lt] at H

Result:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i ∨ i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Proof state:
case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ q.natDegree < j

Tactic:
by_contra! H'

Result:
case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
H' : j ≤ q.natDegree
⊢ False

Proof state:
case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
H' : j ≤ q.natDegree
⊢ False

Tactic:
exact
  ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
    h₁

Result:
no goals

Proof state:
case refine_1.mk
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
by_cases H : natDegree p < i

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : ¬p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Proof state:
case refine_1.mk
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ antidiagonal (p.natDegree + q.natDegree)
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [mem_antidiagonal] at h₁

Result:
case refine_1.mk
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Proof state:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
j : ℕ
h₁ : j = q.natDegree
h₂ : (p.natDegree, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (p.natDegree, j).1 * q.coeff (p.natDegree, j).2 = 0

Tactic:
subst h₁

Result:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
h₂ : (p.natDegree, q.natDegree) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0

Proof state:
case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
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]

Result:
case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ q.natDegree < j

Proof state:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
subst H

Result:
case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
j : ℕ
h₁ : (p.natDegree, j).1 + (p.natDegree, j).2 = p.natDegree + q.natDegree
h₂ : (p.natDegree, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (p.natDegree, j).1 * q.coeff (p.natDegree, j).2 = 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
this : q.natDegree < j
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
rw [coeff_eq_zero_of_degree_lt
    (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
  mul_zero]

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree)
⊢ p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0

Tactic:
exfalso

Result:
case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree)
⊢ False