case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
r : R
hr : r = 0
⊢ eraseLead (↑(monomial i) r) = 0

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
r : R
hr : ¬r = 0
⊢ eraseLead (↑(monomial i) r) = 0
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
r : R
⊢ eraseLead (↑(monomial i) r) = 0
by_cases hr : r = 0
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ eraseLead (↑(monomial i) 0) = 0
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
r : R
hr : r = 0
⊢ eraseLead (↑(monomial i) r) = 0
subst r
no goals
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ eraseLead (↑(monomial i) 0) = 0
simp only [monomial_zero_right, eraseLead_zero]
no goals
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
r : R
hr : ¬r = 0
⊢ eraseLead (↑(monomial i) r) = 0
rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]