simp only [coeff_smul, coeff_scaleRoots, ge_iff_le, smul_eq_mul, coeff_derivative,
  mul_comm (r ^ (natDegree p - _)), mul_assoc, ← pow_add]
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ (derivative (p.scaleRoots r)).coeff i =
    (r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r).coeff i
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ p.coeff (i + 1) * ((↑i + 1) * r ^ (p.natDegree - (i + 1))) =
    p.coeff (i + 1) * ((↑i + 1) * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))))