R : Type ?u.1160753
S : Type ?u.1160756
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}
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
R : Type ?u.1160753
S : Type ?u.1160756
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}
⊢ ↑φ (disc P) = (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
simp only [disc, RingHom.map_add, RingHom.map_sub, RingHom.map_mul, map_pow]
R : Type ?u.1160753
S : Type ?u.1160756
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}
f4 : ↑φ 4 = 4
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
R : Type ?u.1160753
S : Type ?u.1160756
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}
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
have f4 : φ 4 = 4 := map_natCast φ 4
R : Type ?u.1160753
S : Type ?u.1160756
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}
f4 : ↑φ 4 = 4
f18 : ↑φ 18 = 18
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
R : Type ?u.1160753
S : Type ?u.1160756
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}
f4 : ↑φ 4 = 4
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
have f18 : φ 18 = 18 := map_natCast φ 18
R : Type ?u.1160753
S : Type ?u.1160756
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}
f4 : ↑φ 4 = 4
f18 : ↑φ 18 = 18
f27 : ↑φ 27 = 27
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
R : Type ?u.1160753
S : Type ?u.1160756
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}
f4 : ↑φ 4 = 4
f18 : ↑φ 18 = 18
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
have f27 : φ 27 = 27 := map_natCast φ 27
R : Type ?u.1160753
S : Type ?u.1160756
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}
f4 : ↑φ 4 = 4
f18 : ↑φ 18 = 18
f27 : ↑φ 27 = 27
⊢ (↑φ P.a * -(x + y + z)) ^ 2 * (↑φ P.a * (x * y + x * z + y * z)) ^ 2 -
            4 * ↑φ P.a * (↑φ P.a * (x * y + x * z + y * z)) ^ 3 -
          4 * (↑φ P.a * -(x + y + z)) ^ 3 * (↑φ P.a * -(x * y * z)) -
        27 * ↑φ P.a ^ 2 * (↑φ P.a * -(x * y * z)) ^ 2 +
      18 * ↑φ P.a * (↑φ P.a * -(x + y + z)) * (↑φ P.a * (x * y + x * z + y * z)) * (↑φ P.a * -(x * y * z)) =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
R : Type ?u.1160753
S : Type ?u.1160756
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}
f4 : ↑φ 4 = 4
f18 : ↑φ 18 = 18
f27 : ↑φ 27 = 27
⊢ ↑φ P.b ^ 2 * ↑φ P.c ^ 2 - ↑φ 4 * ↑φ P.a * ↑φ P.c ^ 3 - ↑φ 4 * ↑φ P.b ^ 3 * ↑φ P.d - ↑φ 27 * ↑φ P.a ^ 2 * ↑φ P.d ^ 2 +
      ↑φ 18 * ↑φ P.a * ↑φ P.b * ↑φ P.c * ↑φ P.d =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
rw [f4, f18, f27, b_eq_three_roots ha h3, c_eq_three_roots ha h3, d_eq_three_roots ha h3]
no goals
R : Type ?u.1160753
S : Type ?u.1160756
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}
f4 : ↑φ 4 = 4
f18 : ↑φ 18 = 18
f27 : ↑φ 27 = 27
⊢ (↑φ P.a * -(x + y + z)) ^ 2 * (↑φ P.a * (x * y + x * z + y * z)) ^ 2 -
            4 * ↑φ P.a * (↑φ P.a * (x * y + x * z + y * z)) ^ 3 -
          4 * (↑φ P.a * -(x + y + z)) ^ 3 * (↑φ P.a * -(x * y * z)) -
        27 * ↑φ P.a ^ 2 * (↑φ P.a * -(x * y * z)) ^ 2 +
      18 * ↑φ P.a * (↑φ P.a * -(x + y + z)) * (↑φ P.a * (x * y + x * z + y * z)) * (↑φ P.a * -(x * y * z)) =
    (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
ring1