no goals
A : Type ?u.22612
K : Type ?u.22615
R : Type u_1
S : Type ?u.22621
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
⊢ coeff (scaleRoots p s) (natDegree p) = leadingCoeff p
rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]