case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : card (support f) = c
f0 : f = 0
⊢ card (support (eraseLead f)) = c - 1

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : card (support f) = c
f0 : ¬f = 0
⊢ card (support (eraseLead f)) = c - 1
R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : card (support f) = c
⊢ card (support (eraseLead f)) = c - 1
by_cases f0 : f = 0
no goals
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : card (support f) = c
f0 : f = 0
⊢ card (support (eraseLead f)) = c - 1
rw [← fc, f0, eraseLead_zero, support_zero, card_empty]
no goals
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
c : ℕ
fc : card (support f) = c
f0 : ¬f = 0
⊢ card (support (eraseLead f)) = c - 1
rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero f0), fc]