R : Type u_1
S : Type ?u.553084
F : Type ?u.553087
K : Type ?u.553090
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h0 : toPoly P = 0
⊢ P.a = 0 ∧ P.b = 0 ∧ P.c = 0 ∧ P.d = 0
R : Type u_1
S : Type ?u.553084
F : Type ?u.553087
K : Type ?u.553090
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h0 : P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0
⊢ toPoly P ≠ 0
contrapose! h0
R : Type u_1
S : Type ?u.553084
F : Type ?u.553087
K : Type ?u.553090
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h0 : toPoly P = 0
⊢ 0.a = 0 ∧ 0.b = 0 ∧ 0.c = 0 ∧ 0.d = 0
R : Type u_1
S : Type ?u.553084
F : Type ?u.553087
K : Type ?u.553090
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h0 : toPoly P = 0
⊢ P.a = 0 ∧ P.b = 0 ∧ P.c = 0 ∧ P.d = 0
rw [(toPoly_eq_zero_iff P).mp h0]
no goals
R : Type u_1
S : Type ?u.553084
F : Type ?u.553087
K : Type ?u.553090
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h0 : toPoly P = 0
⊢ 0.a = 0 ∧ 0.b = 0 ∧ 0.c = 0 ∧ 0.d = 0
exact ⟨rfl, rfl, rfl, rfl⟩