no goals
R : Type ?u.180963
S : Type u_1
F : Type ?u.180969
K : Type ?u.180972
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝¹ : Semiring R
inst✝ : CommRing S
x y z : S
⊢ (X - ↑C x) * (X - ↑C y) * (X - ↑C z) =
    toPoly { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }
rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]