R : Type ?u.90291
S : Type u_1
F : Type ?u.90297
K : Type ?u.90300
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝¹ : Semiring R
inst✝ : CommRing S
w x y z : S
⊢ ↑C w * (X - ↑C x) * (X - ↑C y) * (X - ↑C z) =
    ↑C w * X ^ 3 + ↑C w * -(↑C x + ↑C y + ↑C z) * X ^ 2 + ↑C w * (↑C x * ↑C y + ↑C x * ↑C z + ↑C y * ↑C z) * X +
      ↑C w * -(↑C x * ↑C y * ↑C z)
R : Type ?u.90291
S : Type u_1
F : Type ?u.90297
K : Type ?u.90300
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝¹ : Semiring R
inst✝ : CommRing S
w x y z : S
⊢ ↑C w * (X - ↑C x) * (X - ↑C y) * (X - ↑C z) =
    toPoly { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }
simp only [toPoly, C_neg, C_add, C_mul]
no goals
R : Type ?u.90291
S : Type u_1
F : Type ?u.90297
K : Type ?u.90300
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝¹ : Semiring R
inst✝ : CommRing S
w x y z : S
⊢ ↑C w * (X - ↑C x) * (X - ↑C y) * (X - ↑C z) =
    ↑C w * X ^ 3 + ↑C w * -(↑C x + ↑C y + ↑C z) * X ^ 2 + ↑C w * (↑C x * ↑C y + ↑C x * ↑C z + ↑C y * ↑C z) * X +
      ↑C w * -(↑C x * ↑C y * ↑C z)
ring1