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

case neg
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
nd : ¬n = natDegree q
⊢ coeff (eraseLead (p + q)) n = coeff (p + eraseLead q) n
case a
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
⊢ coeff (eraseLead (p + q)) n = coeff (p + eraseLead q) n
by_cases nd : n = q.natDegree
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
nd : n = natDegree q
⊢ 0 = coeff (p + eraseLead q) (natDegree q)
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
nd : n = natDegree q
⊢ coeff (eraseLead (p + q)) n = coeff (p + eraseLead q) n
rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_right_of_natDegree_lt pq).symm]
no goals
case pos
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
nd : n = natDegree q
⊢ 0 = coeff (p + eraseLead q) (natDegree q)
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 p < natDegree q
n : ℕ
nd : ¬n = natDegree q
⊢ ¬n = natDegree (p + q)
case neg
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
nd : ¬n = natDegree q
⊢ coeff (eraseLead (p + q)) n = coeff (p + eraseLead 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 p < natDegree q
nd : ¬natDegree (p + q) = natDegree q
⊢ False
case neg.hnc
R : Type u_1
inst✝ : Semiring R
f p q : R[X]
pq : natDegree p < natDegree q
n : ℕ
nd : ¬n = natDegree q
⊢ ¬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 p < natDegree q
nd : ¬natDegree (p + q) = natDegree q
⊢ False
exact nd (natDegree_add_eq_right_of_natDegree_lt pq)