R : Type ?u.935152
S : Type ?u.935155
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) =
    toPoly
      { a := ↑φ P.a, b := ↑φ P.a * -(x + y + z), c := ↑φ P.a * (x * y + x * z + y * z), d := ↑φ P.a * -(x * y * z) }

case inj
R : Type ?u.935152
S : Type ?u.935155
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}
⊢ Function.Injective toPoly
R : Type ?u.935152
S : Type ?u.935155
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}
⊢ map φ P =
    { a := ↑φ P.a, b := ↑φ P.a * -(x + y + z), c := ↑φ P.a * (x * y + x * z + y * z), d := ↑φ P.a * -(x * y * z) }
apply_fun @toPoly _ _
no goals
R : Type ?u.935152
S : Type ?u.935155
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) =
    toPoly
      { a := ↑φ P.a, b := ↑φ P.a * -(x + y + z), c := ↑φ P.a * (x * y + x * z + y * z), d := ↑φ P.a * -(x * y * z) }
rw [eq_prod_three_roots ha h3, C_mul_prod_X_sub_C_eq]
no goals
case inj
R : Type ?u.935152
S : Type ?u.935155
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}
⊢ Function.Injective toPoly
exact fun P Q ↦ (toPoly_injective P Q).mp