R : Type ?u.1301913
S : Type ?u.1301916
F : Type u_2
K : Type u_1
P : Cubic F
inst✝² : Field F
inst✝¹ : Field K
φ : F →+* K
x y z : K
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
hd : disc P ≠ 0
⊢ ∃ x y z, roots (map φ P) = {x, y, z}
R : Type ?u.1301913
S : Type ?u.1301916
F : Type u_2
K : Type u_1
P : Cubic F
inst✝² : Field F
inst✝¹ : Field K
φ : F →+* K
x y z : K
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
hd : disc P ≠ 0
⊢ Finset.card (toFinset (roots (map φ P))) = 3
rw [toFinset_card_of_nodup <| (disc_ne_zero_iff_roots_nodup ha h3).mp hd,
  ← splits_iff_card_roots ha, splits_iff_roots_eq_three ha]
no goals
R : Type ?u.1301913
S : Type ?u.1301916
F : Type u_2
K : Type u_1
P : Cubic F
inst✝² : Field F
inst✝¹ : Field K
φ : F →+* K
x y z : K
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : roots (map φ P) = {x, y, z}
hd : disc P ≠ 0
⊢ ∃ x y z, roots (map φ P) = {x, y, z}
exact ⟨x, ⟨y, ⟨z, h3⟩⟩⟩