R : Type u_1
S : Type ?u.686853
F : Type ?u.686856
K : Type ?u.686859
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ ↑card (Polynomial.roots (toPoly P)) ≤ 3
R : Type u_1
S : Type ?u.686853
F : Type ?u.686856
K : Type ?u.686859
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ Finset.card (toFinset (roots P)) ≤ 3
apply (toFinset_card_le P.toPoly.roots).trans
case pos
R : Type u_1
S : Type ?u.686853
F : Type ?u.686856
K : Type ?u.686859
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : toPoly P = 0
⊢ ↑card (Polynomial.roots (toPoly P)) ≤ 3

case neg
R : Type u_1
S : Type ?u.686853
F : Type ?u.686856
K : Type ?u.686859
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : ¬toPoly P = 0
⊢ ↑card (Polynomial.roots (toPoly P)) ≤ 3
R : Type u_1
S : Type ?u.686853
F : Type ?u.686856
K : Type ?u.686859
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
⊢ ↑card (Polynomial.roots (toPoly P)) ≤ 3
by_cases hP : P.toPoly = 0
no goals
case pos
R : Type u_1
S : Type ?u.686853
F : Type ?u.686856
K : Type ?u.686859
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : toPoly P = 0
⊢ ↑card (Polynomial.roots (toPoly P)) ≤ 3
exact (card_roots' P.toPoly).trans (by rw [hP, natDegree_zero]; exact zero_le 3)
R : Type u_1
S : Type ?u.686853
F : Type ?u.686856
K : Type ?u.686859
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : toPoly P = 0
⊢ 0 ≤ 3
R : Type u_1
S : Type ?u.686853
F : Type ?u.686856
K : Type ?u.686859
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : toPoly P = 0
⊢ natDegree (toPoly P) ≤ 3
rw [hP, natDegree_zero]
no goals
R : Type u_1
S : Type ?u.686853
F : Type ?u.686856
K : Type ?u.686859
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : toPoly P = 0
⊢ 0 ≤ 3
exact zero_le 3
no goals
case neg
R : Type u_1
S : Type ?u.686853
F : Type ?u.686856
K : Type ?u.686859
P : Cubic R
inst✝³ : CommRing R
inst✝² : CommRing S
φ : R →+* S
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
hP : ¬toPoly P = 0
⊢ ↑card (Polynomial.roots (toPoly P)) ≤ 3
exact WithBot.coe_le_coe.1 ((card_roots hP).trans degree_cubic_le)