case a
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
⊢ coeff (eraseLead (p + q)) n = coeff (eraseLead p + q) n
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
⊢ eraseLead (p + q) = eraseLead p + q
ext n
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : n = natDegree p
⊢ coeff (eraseLead (p + q)) n = coeff (eraseLead p + q) n

case neg
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : ¬n = natDegree p
⊢ coeff (eraseLead (p + q)) n = coeff (eraseLead p + q) n
case a
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
⊢ coeff (eraseLead (p + q)) n = coeff (eraseLead p + q) n
by_cases nd : n = p.natDegree
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : n = natDegree p
⊢ 0 = coeff (eraseLead p + q) (natDegree p)
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : n = natDegree p
⊢ coeff (eraseLead (p + q)) n = coeff (eraseLead p + q) n
rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_left_of_natDegree_lt pq).symm]
no goals
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : n = natDegree p
⊢ 0 = coeff (eraseLead p + q) (natDegree p)
simpa using (coeff_eq_zero_of_natDegree_lt pq).symm
case neg.hnc
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : ¬n = natDegree p
⊢ ¬n = natDegree (p + q)
case neg
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : ¬n = natDegree p
⊢ coeff (eraseLead (p + q)) n = coeff (eraseLead p + q) n
rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]
case neg.hnc
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
nd : ¬natDegree (p + q) = natDegree p
⊢ False
case neg.hnc
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
n : ℕ
nd : ¬n = natDegree p
⊢ ¬n = natDegree (p + q)
rintro rfl
no goals
case neg.hnc
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree q < natDegree p
nd : ¬natDegree (p + q) = natDegree p
⊢ False
exact nd (natDegree_add_eq_left_of_natDegree_lt pq)