no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
p : R[X]
hp : Monic p
⊢ ↑normalize p = p
simp only [Polynomial.coe_normUnit, normalize_apply, hp.leadingCoeff, normUnit_one,
  Units.val_one, Polynomial.C.map_one, mul_one]