no goals
R : Type u
S : Type ?u.136653
inst✝¹ : CommSemiring R
inst✝ : Semiring S
I : Ideal R[X]
x : R
x✝ : ∃ p, p ∈ I ∧ degree p ≤ ↑0 ∧ Polynomial.leadingCoeff p = x
p : R[X]
hpI : p ∈ I
hpdeg : degree p ≤ ↑0
hpx : Polynomial.leadingCoeff p = x
⊢ ↑C x ∈ I
rwa [← hpx, Polynomial.leadingCoeff,
  Nat.eq_zero_of_le_zero (natDegree_le_of_degree_le hpdeg), ← eq_C_of_degree_le_zero hpdeg]