R : Type ?u.1296918
S : Type ?u.1296921
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}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ Nodup {x, y, z}
R : Type ?u.1296918
S : Type ?u.1296921
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 ↔ Nodup (roots (map φ P))
rw [disc_ne_zero_iff_roots_ne ha h3, h3]
R : Type ?u.1296918
S : Type ?u.1296921
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}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ Nodup (x ::ₘ y ::ₘ {z})
R : Type ?u.1296918
S : Type ?u.1296921
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}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ Nodup {x, y, z}
change _ ↔ (x ::ₘ y ::ₘ {z}).Nodup
R : Type ?u.1296918
S : Type ?u.1296921
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}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ Nodup {z}
R : Type ?u.1296918
S : Type ?u.1296921
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}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ Nodup (x ::ₘ y ::ₘ {z})
rw [nodup_cons, nodup_cons, mem_cons, mem_singleton, mem_singleton]
R : Type ?u.1296918
S : Type ?u.1296921
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}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
R : Type ?u.1296918
S : Type ?u.1296921
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}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ Nodup {z}
simp only [nodup_singleton]
no goals
R : Type ?u.1296918
S : Type ?u.1296921
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}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
tauto