no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
n : ℕ
inst✝ : Nat.AtLeastTwo n
⊢ map f ↑n = ↑n
rw [Polynomial.map_nat_cast]