case pos
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : card (support f) ≤ 1
⊢ natDegree (eraseLead f) < natDegree f ∨ eraseLead f = 0

case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : ¬card (support f) ≤ 1
⊢ natDegree (eraseLead f) < natDegree f ∨ eraseLead f = 0
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ natDegree (eraseLead f) < natDegree f ∨ eraseLead f = 0
by_cases h : f.support.card ≤ 1
case pos.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : card (support f) ≤ 1
⊢ eraseLead f = 0
case pos
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : card (support f) ≤ 1
⊢ natDegree (eraseLead f) < natDegree f ∨ eraseLead f = 0
right
case pos.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : card (support f) ≤ 1
⊢ eraseLead (↑C (leadingCoeff f) * X ^ natDegree f) = 0
case pos.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : card (support f) ≤ 1
⊢ eraseLead f = 0
rw [← C_mul_X_pow_eq_self h]
no goals
case pos.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : card (support f) ≤ 1
⊢ eraseLead (↑C (leadingCoeff f) * X ^ natDegree f) = 0
simp
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : ¬card (support f) ≤ 1
⊢ natDegree (eraseLead f) < natDegree f
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : ¬card (support f) ≤ 1
⊢ natDegree (eraseLead f) < natDegree f ∨ eraseLead f = 0
left
no goals
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
h : ¬card (support f) ≤ 1
⊢ natDegree (eraseLead f) < natDegree f
apply eraseLead_natDegree_lt (lt_of_not_ge h)