R : Type ?u.1293662
S : Type ?u.1293665
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.a * ↑φ P.a * (x - y) * (x - z) * (y - z) * (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
R : Type ?u.1293662
S : Type ?u.1293665
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 ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
rw [← _root_.map_ne_zero φ, disc_eq_prod_three_roots ha h3, pow_two]
no goals
R : Type ?u.1293662
S : Type ?u.1293665
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.a * ↑φ P.a * (x - y) * (x - z) * (y - z) * (↑φ P.a * ↑φ P.a * (x - y) * (x - z) * (y - z)) ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha,
  and_assoc]