no goals
R✝ : Type ?u.16691
inst✝¹ : Semiring R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ f - ↑C (leadingCoeff f) * X ^ natDegree f = eraseLead f
rw [C_mul_X_pow_eq_monomial, self_sub_monomial_natDegree_leadingCoeff]