rw [hp]
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative ((C (p.coeff 0)).scaleRoots r) = (derivative (C (p.coeff 0))).scaleRoots r