no goals
R : Type u_1
inst✝ : CommRing R
n : ℕ
P : Ideal R
q : R[X]
c : (R ⧸ P)[X]
hq : map (mk P) q = c * X ^ n
hn0 : 0 < n
⊢ eval 0 q ∈ P
rw [← coeff_zero_eq_eval_zero, ← eq_zero_iff_mem, ← coeff_map, hq,
coeff_zero_eq_eval_zero, coeff_zero_eq_eval_zero,
  eval_mul, eval_pow, eval_X, zero_pow hn0, MulZeroClass.mul_zero]