R : Type ?u.715676
S : Type ?u.715679
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑C (↑φ P.a) * prod (Multiset.map (fun a => X - ↑C a) {x, y, z}) = ↑C (↑φ P.a) * (X - ↑C x) * (X - ↑C y) * (X - ↑C z)
R : Type ?u.715676
S : Type ?u.715679
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ toPoly (map φ P) = ↑C (↑φ P.a) * (X - ↑C x) * (X - ↑C y) * (X - ↑C z)
rw [map_toPoly,
  eq_prod_roots_of_splits <|
    (splits_iff_roots_eq_three ha).mpr <| Exists.intro x <| Exists.intro y <| Exists.intro z h3,
  leadingCoeff_of_a_ne_zero ha, ← map_roots, h3]
R : Type ?u.715676
S : Type ?u.715679
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑C (↑φ P.a) * prod ((X - ↑C x) ::ₘ (X - ↑C y) ::ₘ {X - ↑C z}) = ↑C (↑φ P.a) * (X - ↑C x) * (X - ↑C y) * (X - ↑C z)
R : Type ?u.715676
S : Type ?u.715679
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑C (↑φ P.a) * prod (Multiset.map (fun a => X - ↑C a) {x, y, z}) = ↑C (↑φ P.a) * (X - ↑C x) * (X - ↑C y) * (X - ↑C z)
change C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = _
no goals
R : Type ?u.715676
S : Type ?u.715679
F : Type u_1
K : Type u_2
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
⊢ ↑C (↑φ P.a) * prod ((X - ↑C x) ::ₘ (X - ↑C y) ::ₘ {X - ↑C z}) = ↑C (↑φ P.a) * (X - ↑C x) * (X - ↑C y) * (X - ↑C z)
rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc]