no goals
R✝ : Type u
S : Type ?u.71352
inst✝¹ : Ring R✝
R : Type u
inst✝ : CommRing R
p : R[X]
n : ℕ
⊢ coeff (map (algebraMap { x // x ∈ Subring.closure ↑(frange p) } R) (restriction p)) n = coeff p n
rw [coeff_map, Algebra.algebraMap_ofSubring_apply, coeff_restriction]